SIMVA-SoS

Background

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.

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.

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.

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.

 

Tool Overview

(1) User Interface: 대표 화면 스크린샷

 

(2) Tool Features: 리스트 형식으로 도구의 functionality를 리스팅

 A. SoS Modeling & Specifications

  • SIMVA-SoS imports input models and specifications from user’s local device.
    • Input models: SoS system models, SoS environment model
    • Input specifications: Verification properties, Policy specifications, Simulation scenario specification
  • SIMVA-SoS contains predefined skeleton classes to represent input models as Java classes.
  • Based on predefined classes, SIMVA-SoS checks correctness and completeness of input models for Java code generation.
  • SIMVA-SoS reads, interprets, and transforms input models.
    • XML parser reads and interprets input XML files.
    • Java code generator transforms input models into simulatable Java code using predefined classes in SIMVA-SoS.
  • SIMVA-SoS displays information of imported input files.
  • SIMVA-SoS supports re-importation of input files.
  • SIMVA-SoS shows runtime status of model objects during simulation.

B. Simulation

  • SIMVA-SoS simulates the input SoS model by discrete time simulation.
    • Discrete time simulation executes simulation model based on a discrete time unit.
    • Status of models are changed by time flow.
    • Simulation result is log of each time unit.
  • SIMVA-SoS performs multi-agent simulation.
    • CSs of the SoS model is regarded as an autonomous and independent agents.
    • The behavior of each CS is determined by their decision making algorithm.
    • It supports to simulate collaborative behavior or interactions between the multiple agents.

C. Verification

  • SIMVA-SoS verifies the input models by adopting SPRT algorithm.
    • A SPRT algorithm is the fastest statistical model checking algorithm.
    • In SPRT algorithm, SIMVA-SoS simulates the input models several times to each probability (from 0.01 to 1.00) for checking whether each probability is true or false.
  • SIMVA-SoS can apply a specific verification property as a verifiable goal of SoS.
    • There are 22 verification properties that we found from other existing research (listed in Appendix A).
  • SIMVA-SoS shows the raw and analyzed result to the user.
    • The raw result of the verification is the number of samples, number of true samples, the true/false tag selected by the SPRT algorithm.
    • SIMVA-SoS provides the analyzed result to the user by the form of the graph for each probability and its specific value.
  • SIMVA-SoS can save the results of verification as a file.

D. Slicing

  • Slicing module increases the efficiency of simulation and verification by slicing user interested parts of SoS simulation and goal models.

 

Opensource Repository

GitHub link: https://github.com/SESoS/SIMVA-SoS

 

Installation Guide

https://github.com/SESoS/SIMVA-SoS/wiki

 

User Manual

 

See <Background> for screenshots

 

SIMVA-SoS menus

  1. Simulation-based analysis tab
  • Verification Progress: graphical representation of verification process
  • Verification Information: details of the verification input including scenario and verification configurations
  • Verification Progress & Results: details of verification progress and results
  • Analysis: textual representation of verification results
  • Statistical Verification: graphical representation of verification results
  1. Single simulation tab
  • Simulation Progress: graphical representation of simulation process
  • Simulation Information: details of the simulation input including SoS scenario, policy and configurations
  • Model Information: details of simulation models
  • Simulation Progress & Results: details of simulation progress and results
  • Simulation Log: textual representation of simulation results
  • Single Simulation: graphical representation of simulation results