Alternating Simulation and IOCO

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/o-refinement or bounded non-ioco to checking first-order assertions.
Document type :
Conference papers
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01055244
Contributor : Hal Ifip <>
Submitted on : Tuesday, August 12, 2014 - 9:21:23 AM
Last modification on : Wednesday, August 16, 2017 - 3:22:38 PM
Long-term archiving on : Wednesday, November 26, 2014 - 10:36:10 PM

File

ictss.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Margus Veanes, Nikolaj Bjørner. Alternating Simulation and IOCO. 22nd IFIP WG 6.1 International Conference on Testing Software and Systems (ICTSS), Nov 2010, Natal, Brazil. pp.47-62, ⟨10.1007/978-3-642-16573-3_5⟩. ⟨hal-01055244⟩

Share

Metrics

Record views

160

Files downloads

142