System-of-Systems (SoS) is a large-scale complex system in which several independent heterogeneous systems interact and operate in order to achieve high-level goals that cannot be achieved with individual systems. Representative examples of SoS include disaster response systems to respond to mass casualty incidents (MCIs), war simulation systems used to identify war victories and strategies, and smart farms and unmanned drones delivery systems Internet of Things (IoT). D. Seo et al. studied verification of the goal achievement of large and complex SoS using simulation based statistical model checking to solve the state explosion problem caused by SoS complexity.
SoS has characteristics of dynamic reconfiguration and evolution and can be changed by change of external environment and interaction of internal constitution systems. SoS model should be changed every time a change occurs in the SoS, and all the goals in the modified SoS model and the SoS goal model can be input to the statistical model verifier to check whether each goal is achieved. The SoS goal model is an independent model used in the SoS model verification. It is composed of the high level common goal of the SoS, the goal of each constituent system (CS) level, and the detail goal of the subsystem level constituting each CS . However, the disadvantage of statistical model validation is that it is costly because it is based on simulation. It is inefficient to repeatedly perform this statistical model verification on every goal in the SoS goal model whenever a change occurs in the SoS. Therefore, this study proposes SoS target model slicing techniques and tools that can extract change related goals for efficient verification.
The input is the name of the SoS target model in tree form and the subsystem level target directly related to the change in SoS model. The SoS goal model slicer goes through three stages and extracts only the goals related to the change.
Figure: Overall approach
1) Create Slicing Criteria
First, the slicing criterion is created by analyzing the SoS target model and the name of the change-related target input. In the disaster response SoS scenario applying this study, each goal has a validation specification of the PCTL (Probabilistic Computation Tree Logic) format, which is used in the PRISM statistical verification tool. Therefore, the slicing criterion was created by extracting variables on the PCTL specification for a given change-related target as input.
2) Slicing Starting Point Setting
After that, you should set a starting point for slicing. The slicing starting point is set as the target on the SoS target model having the same name as the change related target given as input, and the target set as the starting point is one of the leaf nodes on the SoS target model.
3) Backward Slicing progress
The reverse slicing is performed for the upper targets using the slicing starting point and the slicing criterion. In this study, we used the specification of the targets present in each goal, and in the disaster response SoS applying this study, we use the PCTL specification of each target. . When the reverse slicing is performed to the highest goal SoS target, the slicing is ended and the sliced SoS target model is output.
The following is an example of applying the SoS target model slicer described above to a disaster response SoS. First, the SoS goal model is composed of the CS level goals achieved by each CS and the tree of the detailed goals at the subsystem level constituting the CS, starting from the top level SoS level goal as shown in [Figure 2] .
Figure: Sliced SoS Goal Model
The implementation of the SoS goal model is based on the UML model, and each goal has “Target name, Target system satisfying target, Verification specification specified in PCTL format, Top goal, Sub goal, Detailed target description”. In this model, the goal of the highest level of SoS is ‘①SaveOver40% patient’, which indicates that the entire patient is more than 40% of all patients. Below these are the CS level goals, which are the goals for the number of patients rescued in the sea and land, respectively, ‘② saveOver40% LANDPatient’ and ‘③ saveOver40% SEAPatient’. Finally, subsystem level objectives are composed of ‘④ treatLANDPatient’ and ‘⑤ notViolateTranserringRule’ for goal ②, and ‘⑥ HasAEDwithPR_HELIPerformance’ and ‘⑦ treatSEAPatient’ for goal.
- Sangwon Hyun, Jiyoung Song, Eunkyoung Jee, Doo-Hwan Bae, “Goal Model Slicing for Efficient Verification of System of Systems”, KSC 2018
- See <GoalModelSlicer>