On the verification of mission-related properties in software-intensive systems-of-systems architectural design

摘要

One of the prominent domains of nowadays software engineering concerns on building and maintaining the so-called system-of-systems (SoS). The activity of integrating independent, potentially heterogeneous, and distributed systems has become remarkable. Designing SoS that consists on integrating independent and behaviorally unknown systems involves several difficulties, specially due to the inner dynamism that hovers SoS. Aiming to support the development of such kind of systems, mission models allows stakeholders to set objectives and resources for SoS, complementing the traditional requirements approach. In a mission model, designers specify the missions of the system and what the system is capable of doing to achieve them. On the other hand, one of the most desired feature of any modeling language is the possibility of formally verifying described properties. Enabling the stakeholders to check the degree of compliance of a model to a given set of properties fosters quality and simplifies the development process by shifting the problem resolution to the design level. The difficulties of SoS modeling also reflect on the verification processes: traditional verification methods were shown noneffective. In this context, this work proposes a method to verify SoS models based on mission-related properties, using the mission modeling language mKAOS and the DynBLTL formalism. Our proposal can be applied to any modeling language, although we exemplify using SosADL, an architectural description language for the SoS context.