Formal Verification of 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

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.  

Downloads

Published

2021-09-15

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

I assign to Informatica, An International Journal of Computing and Informatics ("Journal") the copyright in the manuscript identified above and any additional material (figures, tables, illustrations, software or other information intended for publication) submitted as part of or as a supplement to the manuscript ("Paper") in all forms and media throughout the world, in all languages, for the full term of copyright, effective when and if the article is accepted for publication. This transfer includes the right to reproduce and/or to distribute the Paper to other journals or digital libraries in electronic and online forms and systems.

I understand that I retain the rights to use the pre-prints, off-prints, accepted manuscript and published journal Paper for personal use, scholarly purposes and internal institutional use.

In certain cases, I can ask for retaining the publishing rights of the Paper. The Journal can permit or deny the request for publishing rights, to which I fully agree.

I declare that the submitted Paper is original, has been written by the stated authors and has not been published elsewhere nor is currently being considered for publication by any other journal and will not be submitted for such review while under review by this Journal.  The Paper contains no material that violates proprietary rights of any other person or entity. I have obtained written permission from copyright owners for any excerpts from copyrighted works that are included and have credited the sources in my article. I have informed the co-author(s) of the terms of this publishing agreement.


Copyright ©  Slovenian Society Informatika