{"id":351,"date":"2018-11-06T00:57:02","date_gmt":"2018-11-06T00:57:02","guid":{"rendered":"http:\/\/se.kaist.ac.kr\/starlab\/?page_id=351"},"modified":"2018-12-12T15:16:04","modified_gmt":"2018-12-12T15:16:04","slug":"simva-sos","status":"publish","type":"page","link":"https:\/\/se.kaist.ac.kr\/starlab\/tools-and-artifacts\/opensource-tools\/simva-sos\/","title":{"rendered":"SIMVA-SoS"},"content":{"rendered":"

Background<\/strong><\/h4>\n

A System-of-Systems (SoS) is a collection of systems, which consists of autonomous and independent constituent systems to achieve higher-level goals. As an SoS changes constantly due to external and internal factors, dynamic reconfiguration and evolutionary development must be performed effectively. To manage an SoS that has these characteristics, SoS managers and engineers need to model and verify an SoS that accommodates changes. SIMVA-SoS is a tool to support modeling, simulation and statistical verification of the SoS. In addition, it supports slicing technique for efficient verification of large-scale SoS models.<\/p>\n

For the simulation and verification, a simulation model should be generated. In SIMVA-SoS, the simulation model is generated in the form of the source code, which contains the information of a target SoS and its environment. The information of the models is first specified in several input models, and it contains specific SoS-level entities, CS-level entities, and environmental entities. A user of SIMVA-SoS will import model files and it will be converted into the simulation model as JAVA source code. Also, a simulation scenario needs to be optionally imported to run specific simulation.<\/p>\n

A key aspect of SoS is that how can we achieve whole SoS-level goals by orchestrating the interconnection between otherwise independent CSs. Thus, naturally, it is necessary to study approaches to verify whether the SoS-level goals are achieved or not. To do this, we consider a simulation-based statistical verification, or Statistical Model Checking (SMC), for SoS. While SMC only provides probabilistic guarantees about the correctness of the answer, it overcomes the critical state explosion problem caused by the scalability of the SoS.<\/p>\n

Since the size and complexity of SoSs are too great to apply existing verification techniques, an efficient verification method for dynamically changing SoSs is required. If we can detect the change-related goals of an SoS and the corresponding change-affected parts in an SoS model, we can slice the SoS model in our area of concern and verify the SoS model efficiently. The slicing module could save the cost of verifying the whole of an SoS model by an efficient statistical model checking for SoSs.<\/p>\n

 <\/p>\n

Tool Overview<\/strong><\/h4>\n

(1) User Interface: \ub300\ud45c \ud654\uba74 \uc2a4\ud06c\ub9b0\uc0f7<\/p>\n

\"\"<\/a><\/p>\n

\"\"<\/a><\/p>\n

 <\/p>\n

(2) Tool Features: \ub9ac\uc2a4\ud2b8 \ud615\uc2dd\uc73c\ub85c \ub3c4\uad6c\uc758 functionality\ub97c \ub9ac\uc2a4\ud305<\/p>\n

\u00a0A. SoS Modeling & Specifications<\/strong><\/p>\n