Formal Verification of Emergent Properties

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 components and their manner of connectivity.The global behavior 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 systems. The purpose of this paper is to give an overview and to 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 the 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 to verify the emergent properties.  

Authors

  • Kamal Boumaza Badji Mokhtar Annaba University, Computer science department, LISCO Laboratory.
  • Cherif Tolba Computer science department, Badji Mokhtar University, Annaba, B.P. 12, 23000, Algeria
  • Iulian Ober ISAE-Supaero, University of Toulouse, France

DOI:

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

Downloads

Published

09/15/2021

How to Cite

Boumaza, K., Tolba, C., & Ober, I. (2021). Formal Verification of Emergent Properties. Informatica, 45(3). https://doi.org/10.31449/inf.v45i3.3160

Issue

Vol. 45 No. 3 (2021)

Section

Regular papers

License

Authors retain copyright in their work. By submitting to and publishing with Informatica, authors grant the publisher (Slovene Society Informatika) the non-exclusive right to publish, reproduce, and distribute the article and to identify itself as the original publisher.

All articles are published under the Creative Commons Attribution license CC BY 3.0. Under this license, others may share and adapt the work for any purpose, provided appropriate credit is given and changes (if any) are indicated.

Authors may deposit and share the submitted version, accepted manuscript, and published version, provided the original publication in Informatica is properly cited.