Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Alternating Simulation and IOCO

Margus Veanes and Nikolaj Bjorner

Abstract

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.

Details

Publication typeInproceedings
Published inICTSS'10
Pages47–62
Volume6435
SeriesLNCS
PublisherSpringer Verlag

Previous versions

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

> Publications > Alternating Simulation and IOCO