Alternating Simulation and IOCO

We propose a symbolic framework called guarded labeled assignment systems or GLASs and show how GLASs can be used as a foundation for symbolic analysis of various aspects of formal specification languages. We define a notion of i/o-refinement over GLASs as an alternating simulation relation and provide formal proofs that relate i/o-refinement to ioco. We show that non-i/o-refinement reduces to a reachability problem and provide a translation from bounded non-i/orefinement or bounded non-ioco to checking first-order assertions.

In  ICTSS'10

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details

TypeInproceedings
Pages47–62
Volume6435
SeriesLNCS

Previous Versions

Margus Veanes and Nikolaj Bjorner. Alternating Simulation and IOCO, Microsoft Research, April 2010.

> Publications > Alternating Simulation and IOCO