@inproceedings{70f940469ba344098a3e880c07f744c9,
title = "Refinements for Open Automata",
abstract = "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.",
keywords = "Composition, Labelled transition systems, Simulation",
author = "Rab{\'e}a Ameur-Boulifa and Quentin Corradi and Ludovic Henrio and Eric Madelaine",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2023.; 21st International Conference on Software Engineering and Formal Methods, SEFM 2023 ; Conference date: 06-11-2023 Through 10-11-2023",
year = "2023",
month = jan,
day = "1",
doi = "10.1007/978-3-031-47115-5\_2",
language = "English",
isbn = "9783031471148",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "11--29",
editor = "Carla Ferreira and Willemse, \{Tim A.C.\}",
booktitle = "Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Proceedings",
}