{"id":450,"date":"2018-11-06T20:08:38","date_gmt":"2018-11-06T20:08:38","guid":{"rendered":"http:\/\/se.kaist.ac.kr\/starlab\/?page_id=450"},"modified":"2018-12-12T10:40:19","modified_gmt":"2018-12-12T10:40:19","slug":"sos-simulation-model-slicing","status":"publish","type":"page","link":"https:\/\/se.kaist.ac.kr\/starlab\/sos-simulation-model-slicing\/","title":{"rendered":"SoS Simulation Model Slicing"},"content":{"rendered":"
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.<\/p>\n
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.<\/p>\n
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.<\/p>\n
Figure: Overall approach<\/em><\/p>\n <\/p>\n 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 \u2018SaveOver40%SEAPatients\u2019, 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.<\/p>\n 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.<\/p>\n 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.<\/p>\nResults<\/strong><\/h4>\n