Refinements for Open Automata - Inria - Institut national de recherche en sciences et technologies du numérique
[go: up one dir, main page]

Communication Dans Un Congrès Année : 2023
Refinements for Open Automata
1 LabSoC - System on Chip (Télécom Paris (Eurecom) Sophia Antipolis - France)
"> LabSoC - System on Chip
2 COMELEC - Département Communications & Electronique (19 Place Marguerite Perey 91120 PALAISEAU - France)
"> COMELEC - Département Communications & Electronique
3 CASH - Compilation et Analyse, Logiciel et Matériel (France)
"> CASH - Compilation et Analyse, Logiciel et Matériel
4 LIP - Laboratoire de l'Informatique du Parallélisme (46 Allée d'Italie 69364 LYON CEDEX 07 - France)
"> LIP - Laboratoire de l'Informatique du Parallélisme
5 KAIROS - Logical Time for Formal Embedded System Design (2004 route des Lucioles BP 93 06902 Sophia Antipolis - France) "> KAIROS - Logical Time for Formal Embedded System Design

Résumé

Establishing equivalence and refinement relations between programs is an important mean for verifying their correctness. By establishing that the behaviours of a modified program simulate those of the source one, simulation relations formalise the desired relationship between a specification and an implementation, two equivalent implementations, or a program and its optimised implementation. This article discusses a notion of simulation between open automata, which are symbolic behavioural models for communicating systems. Open automata may have holes modelling elements of their context, and can be composed by instantiation of the holes. This allows for a compositional approach for verification of their behaviour. We define a simulation between open automata that may or may not have the same holes, and show under which conditions these refinements are preserved by composition of open automata.
Fichier principal
Vignette du fichier
refinementarticleV2.pdf (435.1 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-04271300 , version 1 (06-11-2023)

Licence

Identifiants

Citer

Rabéa Ameur-Boulifa, Quentin Corradi, Ludovic Henrio, Eric Madelaine. Refinements for Open Automata. SEFM 2023 - Software Engineering and Formal Methods, Nov 2023, Eindhoven, Netherlands. pp.11-29, ⟨10.1007/978-3-031-47115-5_2⟩. ⟨hal-04271300⟩
289 Consultations
85 Téléchargements

Altmetric

Partager

More