Modeling and Verification for Different Types of System of Systems using PRISM

摘要

A System of Systems (SoS) consists of complex Constituent Systems (CSs), which have managerial and operational independence. As the CSs have independence, the degree of authority to control the CSs varies depending on the different types of SoS, such as directed, acknowledged, and collaborative SoS. While many researchers have attempted to model SoSs and verify SoS-level goals, little attention has been paid to how different types of SoSs are characterized and realized during modeling and verification. Using a mass casualty incident response system as a common working example for different types of a SoS, we model the types of SoS with probabilistic models of PRISM, which can capture uncertain behaviors of an SoS in a quantitative manner and perform statistical model checking in order to verify to which extent each type of SoS achieves the SoS-level goal. Differences between the different types of SoS are demonstrated in the probabilistic models and analyzed by statistical model checking. This modeling and verification can help SoS-level managers to identify the appropriate SoS types to achieve the SoS-level goal.