Alternating Simulation and IOCO - Testing Software and Systems Access content directly
Conference Papers Year : 2010

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.
Fichier principal
Vignette du fichier
ictss.pdf (208 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01055244 , version 1 (12-08-2014)

Licence

Attribution

Identifiers

Cite

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⟩
84 View
153 Download

Altmetric

Share

Gmail Facebook X LinkedIn More