{"id":911,"date":"2020-11-25T04:00:40","date_gmt":"2020-11-25T04:00:40","guid":{"rendered":"http:\/\/se.kaist.ac.kr\/starlab\/?page_id=911"},"modified":"2020-11-25T04:27:40","modified_gmt":"2020-11-25T04:27:40","slug":"interactive-simulation","status":"publish","type":"page","link":"https:\/\/se.kaist.ac.kr\/starlab\/studies\/study-2-statistical-verification-of-sos\/interactive-simulation\/","title":{"rendered":"Interactive Simulation"},"content":{"rendered":"

Architecture of SIMVA-SoS<\/h4>\n

 <\/p>\n

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

Figure shows the whole architecture of SIMVASoS.\u00a0SIMVA-SoS can be divided into two modules: SIMVASoS\u00a0simulator and SIMVA-SoS verifier. The SIMVA-SoS simulator\u00a0has three inputs: SoS model, default scenario, and stimulus.\u00a0The first two inputs must be defined before running the\u00a0simulation, and the last input can be defined before or during\u00a0the simulation. The SIMVA-SoS simulator has a user interface\u00a0for interactive simulation. Interactive simulation allows users\u00a0to modify the model or scenario through the injection of\u00a0a stimulus during the simulation. If the model or scenario\u00a0is changed through the interactive simulator, these changes\u00a0are reflected in the simulation. At the end of the simulation,\u00a0the execution results, that is, the logs of the simulation, are\u00a0saved in a storage device. After the simulation, the verification\u00a0process is executed. For the verification, a verification property\u00a0must be defined in advance. We defined abstract verification\u00a0property classes for various types of verification properties\u00a0that can be used in diverse domains. During verification, the\u00a0statistical verification algorithm runs and the verification result\u00a0is produced.<\/p>\n

Interactive Simulator for SoS<\/h4>\n

To reflect the characteristics, we implement the interactive simulator based on the structure of discrete-time and multiagent simulation. A discrete-time simulation structure is used to reflect evolutionary development in the simulator. The interactive simulator\u00a0enables users to inject new scenario events during the simulation.\u00a0The discrete-time simulation structure, which updates all\u00a0system states in all discrete times, allows the user to inject new\u00a0scenario events during the simulation. We applied discrete time\u00a0simulation to the SoS simulation, resulting in a structure\u00a0that updates the state of every CS at every tick.<\/p>\n

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

In the user\u2019s perspective in figure, the user sets up the\u00a0simulation scenario, simulation policy, and simulation configuration\u00a0before running the simulation. After running the\u00a0simulation, the user can interrupt the simulation at any time\u00a0during the simulation. When the user interrupts the simulation,\u00a0the simulation stops while maintaining the current simulation\u00a0state. Then, the user can inject a new scenario event. The
\nuser can resume the simulation after injecting scenario events.\u00a0When the simulation is resumed, the simulation continues\u00a0from the point where the simulation was stopped. The user\u00a0can observe the injected scenario event and progress of the\u00a0simulation through the GUI. After the simulation is finished,\u00a0the user can analyze the simulation results.<\/p>\n

In the simulation engine\u2019s perspective in figure, the simulation\u00a0scenario, policy, and configuration are reflected into\u00a0the simulation. When the simulation runs, scenario events that\u00a0have been defined by the user are updated in the simulation\u00a0engine. Further, scenario events that are injected by the user\u00a0during the simulation are updated in the simulation engine\u00a0when the user resumes the simulation. After updating the scenario
\nevents, the simulation engine increments the simulation\u00a0time by one tick. Here, a tick is the logical execution time of\u00a0the simulation. The simulation engine executes scenario events\u00a0that need to be executed through logic time. For example,\u00a0suppose we have a scenario event where we add one firefighter\u00a0at 30 ticks. If the logical time of the simulation increases\u00a0from 29 ticks to 30 ticks, the scenario event is triggered\u00a0at this point. In other words, one firefighter is added to\u00a0the simulation. The process of this loop repeats until the\u00a0simulation is finished. When the simulation is finished, the\u00a0simulation engine stores all scenario events applied to the\u00a0simulation. In addition, simulation logs and result reports are\u00a0generated for the simulation.<\/p>\n

 <\/p>\n

Related Publications<\/strong><\/h4>\n
    \n
  • Park, S., Shin, Y. J., Hyun, S., & Bae, D. H. (2020, June). SIMVA-SoS: Simulation-based Verification and Analysis for System-of-Systems. In\u00a02020 IEEE 15th International Conference of System of Systems Engineering (SoSE)<\/i>\u00a0(pp. 575-580). IEEE.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"

    Architecture of SIMVA-SoS   Figure shows the whole architecture of SIMVASoS.\u00a0SIMVA-SoS can be divided into two modules: SIMVASoS\u00a0simulator and SIMVA-SoS verifier. The SIMVA-SoS simulator\u00a0has three inputs: SoS model, default scenario, and stimulus.\u00a0The first two inputs must be defined before running the\u00a0simulation, and the last input can be defined before or during\u00a0the simulation. The SIMVA-SoS simulator […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":340,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/pages\/911"}],"collection":[{"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/comments?post=911"}],"version-history":[{"count":6,"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/pages\/911\/revisions"}],"predecessor-version":[{"id":937,"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/pages\/911\/revisions\/937"}],"up":[{"embeddable":true,"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/pages\/340"}],"wp:attachment":[{"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/media?parent=911"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}