Model synthesis and stochastic automated verification of systems-of-systems dynamic architectures

Software intensive Systems-of-Systems (SoS) are complex alliances of autonomous Constituent Systems (CSs) formed at a large scale to achieve a common objective. As such the CSs are operationally and managerially independent and geographically dispersed which generate emergent behaviors to achieve SoS missions through collective dynamics. Therefore, architectural modeling and analysis of a resulting SoS is pivotal to avoid stochastic architectural arrangements that can lead to undesired behaviors, systems outages, losses and non-conformance of core Quality Attributes (QAs) such as performance and reliability. In this research, we propose a formally founded approach for stochastic synthesis and automated verification of SoS architectural models to predict the impact of dynamic architectural changes on QAs at runtime. At first, we provide Hybrid Stochastic Formalism (HSF) based on Process Algebras (PAs) to model the stochastic SoS software architecture. At the architectural level, non-determinism is dealt with by treating HSF as Markov Decision Process (MDP). The SoS modeled with MDP is then verified against certain system properties using model checking through Probabilistic Computation Tree Logic (PCTL) operators. The effectiveness of our approach is evaluated through a fire monitoring and emergency response SoS to predict the impact of dynamic reconfiguration on QAs. The experimental results show that our method helps to assess different architectural configurations that support design choices to achieve missions without compromising quality.