OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Formal Verification of Emergent Properties

Boumaza, Kamal and Tolba, Cherif and Ober, Iulian Formal Verification of Emergent Properties. (2021) Informatica, 45 (3). 463-475. ISSN 0350-5596

[img]
Preview
(Document in English)

PDF (Publisher's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
545kB

Official URL: https://doi.org/10.31449/inf.v45i3.3160

Abstract

Complex systems and systems of systems (SoS) are systems characterized by the interconnection of a large number of components or sub-systems. The complexity of such systems increases with the number of com- ponents and their manner of connectivity. The global behaviour of complex systems and SoS exhibits some properties that cannot be predicted by analysing components or sub-systems in isolation. The verification of these properties called “emergent properties" is considered a crucial issue when engineering such sys- tems. The purpose of this paper is to give an overview and verify emergent properties. In a first step, we have taken the blinker and the traffic light of the game of life as examples to verify emergence by using refinement techniques; in a second step, since the refinement is not straightforward, we have taken another example, the Boids model, and by using timed automata and UPPAAL model checking techniques, we have been able to simulate and verify emergent properties.

Item Type:Article
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Other partners > Université Badji Mokhtar - Annaba (ALGERIA)
Laboratory name:
Statistics:download
Deposited On:23 Nov 2021 10:34

Repository Staff Only: item control page