SMC: An Approach for the Statistical Model Checking of Systems-of-Systems Dynamic Architectures with MS4Me and PLASMA
-
Contemporary society increasingly relies on software-intensive systems, a dependency driven by the growing complexity of demands. Isolated systems, unable to meet these multifaceted requirements, have given rise to Systems-of-Systems (SoS). SoS emerge as a solution, capitalizing on the interoperability of independent systems to deliver complex solutions that individual systems cannot achieve in isolation. The inherent dynamism of SoS architecture, with constituents joining and departing as needed, results in an ever-evolving structure.
SoS often underpin critical domains, where failures can have severe human, environmental, social, or financial consequences. Thus, SoS engineers bear the responsibility of ensuring that specific properties within the software architecture persist throughout operations, ensuring reliability and faultless performance. However, due to the non-deterministic nature stemming from dynamic architecture of SoS, formal verification of such properties necessitates the combined use of simulation and a statistical verifier.
Recognizing the substantial costs and risks associated with implementing an SoS without rigorous architectural verification, this article's principal contribution lies in presenting the outcomes of developing and evaluating an infrastructure tailored to enable statistical and formal verification of properties within SoS software architectures. To achieve this, an interprocess communication framework was devised, facilitating seamless interaction between the MS4ME simulator and the PLASMA statistical verifier.
This statistical verification capability empowers the early verification of SoS properties during architectural design, proactively addressing potential challenges and vulnerabilities. The results obtained are expected to not only advance the state of the art in SoS Software Engineering but also contribute significantly to a broader research initiative dedicated to SoS architectural design. The conducted experiment conclusively demonstrates that our infrastructure excels at conducting statistical verification for SoS dynamic architectures, achieving a high confidence interval while effectively managing computational costs at an admirably sustainable level.
-
-
-
-
|