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.
Type de document :
Communication dans un congrès
Alexandre Petrenko; Adenilso Simão; José Carlos Maldonado. 22nd IFIP WG 6.1 International Conference on Testing Software and Systems (ICTSS), Nov 2010, Natal, Brazil. Springer, Lecture Notes in Computer Science, LNCS-6435, pp.47-62, 2010, Testing Software and Systems. 〈10.1007/978-3-642-16573-3_5〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01055244
Contributeur : Hal Ifip <>
Soumis le : mardi 12 août 2014 - 09:21:23
Dernière modification le : mercredi 16 août 2017 - 15:22:38
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 22:36:10

Fichier

ictss.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Margus Veanes, Nikolaj Bjørner. Alternating Simulation and IOCO. Alexandre Petrenko; Adenilso Simão; José Carlos Maldonado. 22nd IFIP WG 6.1 International Conference on Testing Software and Systems (ICTSS), Nov 2010, Natal, Brazil. Springer, Lecture Notes in Computer Science, LNCS-6435, pp.47-62, 2010, Testing Software and Systems. 〈10.1007/978-3-642-16573-3_5〉. 〈hal-01055244〉

Partager

Métriques

Consultations de la notice

138

Téléchargements de fichiers

73