SAM-SoS: A stochastic software architecture modeling and verification approach for complex system-of-systems

Ahmad Mohsin, Naeem Khalid Janjua, Syed M.S. Islam, Muhammad Ali Babar

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)
27 Downloads (Pure)


A System-of-Systems (SoS) is a complex, dynamic system whose Constituent Systems (CSs) are not known precisely at design time, and the environment in which they operate is uncertain. SoS behavior is unpredictable due to underlying architectural characteristics such as autonomy and independence. Although the stochastic composition of CSs is vital to achieving SoS missions, their unknown behaviors and impact on system properties are unavoidable. Moreover, unknown conditions and volatility have significant effects on crucial Quality Attributes (QAs) such as performance, reliability and security. Hence, the structure and behavior of a SoS must be modeled and validated quantitatively to foresee any potential impact on the properties critical for achieving the missions. Current modeling approaches lack the essential syntax and semantics required to model and verify SoS behaviors at design time and cannot offer alternative design choices for better design decisions. Therefore, the majority of existing techniques fail to provide qualitative and quantitative verification of SoS architecture models. Consequently, we have proposed an approach to model and verify Non-Deterministic (ND) SoS in advance by extending the current algebraic notations for the formal models as a hybrid stochastic formalism to specify and reason architectural elements with the required semantics. A formal stochastic model is developed using a hybrid approach for architectural descriptions of SoS with behavioral constraints. Through a model-driven approach, stochastic models are then translated into PRISM using formal verification rules. The effectiveness of the approach has been tested with an end-to-end case study design of an emergency response SoS for dealing with a fire situation. Architectural analysis is conducted on the stochastic model, using various qualitative and quantitative measures for SoS missions. Experimental results reveal critical aspects of SoS architecture model that facilitate better achievement of missions and QAs with improved design, using the proposed approach.

Original languageEnglish
Pages (from-to)177580-177603
Number of pages24
JournalIEEE Access
Publication statusPublished - 8 Oct 2020
Externally publishedYes


  • Architecture modeling
  • Formal modeling
  • Quantitative verification
  • Statistical model checking
  • Stochastic systems
  • System properties
  • System-of-systems


Dive into the research topics of 'SAM-SoS: A stochastic software architecture modeling and verification approach for complex system-of-systems'. Together they form a unique fingerprint.

Cite this