| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
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.
Cited literature [22 references]
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
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