A Formal Language for Modelling and Verifying Systems-of-Systems Software Architectures

Akram Seghiri (1) , Faiza Belala (2, 3) , Nabil Hameurlain (1)

1 LIUPPA - Laboratoire Informatique de l'Université de Pau et des Pays de l'Adour
2 Université de Constantine 2 Abdelhamid Mehri [Constantine]
3 LIRE - Laboratoire d'Informatique Répartie [Algérie]

Systems of systems (SoS) are a set of independent systems that are constantly evolving. These systems cooperate in order to achieve a common goal, known as an SoS mission. It is difficult to capture their behaviours while operating in a hierarchical, cooperative and evolutionary structure. Thus, a software architecture based approach is defined in order to model and analyze these systems, reducing their increasing complexity. It ought to describe an SoS on both structural and behavioural levels. In this paper, ArchSoS, an ADL dedicated to describe SoS software architectures, is extended with a syntax-driven formal description, based on Bigraphic Reactive Systems (BRS). SoS defined via ArchSoS have both a graphical and a textual view. For this syntax to be executable, and to verify SoS evolutions, an operational semantic for ArchSoS is defined. It is implemented in Maude language to permit ArchSoS behavioural simulations, and its formal analysis is done through Linear Temporal Logic (LTL). The proposed approach is illustrated through a Crisis Response SoS as a case study.

Domains: Computer Science [cs]

Akram Seghiri, Faiza Belala, Nabil Hameurlain. A Formal Language for Modelling and Verifying Systems-of-Systems Software Architectures. International journal of systems and service-oriented engineering (IJSSOE), 2022, 12 (1), pp.1-17. ⟨10.4018/IJSSOE.297137⟩. ⟨hal-03658631⟩