SoS Simulation Model Slicing

Background

In order to verify a large-scale complex SoS efficiently, statistical model checking (SMC) techniques can be applied to measure the probability of goal achievement by the SoS. SMC is a simulation-based model verification technique that statistically analyzes the probability of how likely it is that the given verification properties will be satisfied by sampling the simulation results from the model. While the size and the complexity of SoSs are barriers to applying traditional model checking approaches, a simulation-based statistical verification method may be a good solution for bypassing the state explosion problem and for verifying high-level system properties.

Even though we can perform statistical verification of an SoS, it may not be easy to deal with the dynamic characteristics of the SoS during the verification process. In particular, when there is a need to respond instantly to changes in an SoS during its operation, it may be neither efficient nor feasible to verify the entire SoS model. When the size of an SoS model is reduced by using the slicing method, the memory consumption and execution time needed for the verification will also be reduced. In addition, it will not be necessary to perform duplicate verifications of verification properties that are irrelevant to the current change. It will be necessary to verify the change-related parts of the SoS model, thereby reducing the verification cost.

In this study, we propose SoS GaP slicer, a verification method for an SoS designed to enable handling of the dynamic characteristics of the SoS. To deal with the dynamic characteristics of the SoS, we define the changes that can occur during the SoS operation, and we introduce a mechanism that responds to these changes. By reducing the range of the models and the properties to be verified through use of SoS GaP slicer, we could considerably improve the efficiency of the verification. The experimental results show that SoS GaP slicer can effectively shorten the time needed to verify an SoS model by 7.4 times.

Overall Approach/Method

Figure: Overall approach

The slicing technique based on the SoS-level goals is applied to the SoS PRISM models and SoS-Java programs. The slicing criterion for SoS PRISM models and SoS Java programs is a goal related to the SoS changes. Goals are examples of the goals related to the current change. Each goal has its subject CSs, and the subject CSs are sliced from the entire SoS PRISM model and Java program. To Slice the subject CSs from the SoS PRISM model and Java program is to slice the corresponding modules. For an example, if we set the target SoS goal as ‘SaveOver40%SEAPatients’, which is one of the change related goals, SoS Simulation Model slicer slices the subject CSs, the helicopter modules, the hospital modules, and the environment modules from the entire MCI response SoS PRISM model. when slicing the helicopters, hospitals and environment modules, statements which have the same label with other statements in non-sliced modules should be discarded as well due to the synchronization characteristic of the PRISM model.

The Verification results for the changed SoS-PRISM model and SoS-Java programs are the output. PRISM engine receives a sliced SoS PRISM model from the PRISM model slicing module and change-related SoS goals which becomes the verification properties. SIMVA-SoS receives a sliced SoS-Java program and verify the sliced model based on the verification properties. With the given two inputs, verification engine verifies the SoS PRISM models and SoS Java programs using statistical model checking techniques.

Results

When the SoS-level goals related to the change are sliced, slicing technique based on the SoS-level goals is applied to SoS PRISM model. In order to slice the SoS PRISM model, we need to generate PRISM model dependency graph (PMDG) and to extract variables included in the sliced SoS-level goals. Below Figure describes the part of PMDG of the MCI-responsive SoS described.

Figure: Slicing result

The name of each CS is identified by the module name represented at the root of each module: Hospital A, Helicopter 1, Ambulance 1 in the Figure. When PRISM conducts SMC, it randomly executes one of the executable predicates in each module for every simulation step. We represent the relation of non-deterministic execution in an arrow with a sector form. The PMDG has control and data dependency graph as well as other model dependency graphs. The control dependency graph is drawn with a black unidirectional solid arrow, and an arrow is drawn according to the execution precedence of the statement. The data dependency graph is drawn with a black unidirectional dotted arrow, and an arrow is drawn from read-predicate to write-predicate on the same variable.

Unlike other existing dependency graphs, the PMDG has an additional synchronization dependency. Interactions and synchronization between CSs are significant for an SoS to be dynamically reconfigured or to achieve SoS-level goals. For instance, ‘patient SEA++’ predicate of the helicopter module and ‘patient1 SEA=0’ predicate of the hospital module in the Figure are synchronized by the label [Heli1 arrives].

These predicates indicate that the number of patients in the helicopter become zero and the number of hospital patients increases at the same time as the patients are transferred. The synchronization dependency graph is drawn with a black bidirectional dotted arrow. The data dependency graph indicates the read/write relationship of data. The SoS Simulation Model slicer slices the predicate recursively on the predicate that it may have written to the last variable. The synchronization dependency graph of PRISM models is a graph showing that the predicates are executed simultaneously in different modules. When a predicate with a certain label A in one module is executed, the predicates of other modules with the same label should be executed together. Thus, if one predicate is sliced, the other predicates in the synchronization dependency relationship are also sliced. For example, if the ‘patient SEA++’ predicate in the helicopter module in Figure 5 is sliced, the ‘patient1 SEA=0’ statement of the hospital module in the synchronization dependency relationship must be sliced together.

 

Related Publications

  • Song, Jiyoung, et al. “SoS GaP Slicer: Slicing SoS Goal and PRISM Models for Change-Responsive Verification of SoS.” 2017 24th Asia-Pacific Software Engineering Conference (APSEC). IEEE, 2017.

 

Related Tools