Motivation
The increasing scale and complexity of systems have reached a point that imposes qualitatively new demands on the existing system technology. The emerging system is characterized by distributed, decentralized, and networked combinations of autonomous sub-systems under large-scale and complex environments. This new “system” is a general concept of “System of systems” (SoS). The term has arisen in various domains such as social infrastructures, smart grids, military services, and air traffic.
With respect to SoS, there are various types of definition from the literature that have been independently published by industry, government, and academia. One definition suggests that SoS is composed of independent sub-systems, which is called Constituent Systems (CSs), and CS has two unique properties: (1) operational independence, i.e., each system operates independently and it achieves its own goals by itself and (2) managerial independence, i.e., each system is managed in most parts for its own goals rather than the goals of SoS. These indicate that CS is operated, managed, and developed independently, and it may not focus on the whole SoS-level goals. The behavior of an SoS emerges from the interaction among its CSs.
A key aspect of SoS is that how we can achieve whole SoS-level goals by orchestrating the interconnection between otherwise independent CSs. Thus, naturally, it is necessary to study approaches to verifying whether the SoS-level goals are achieved or not. However, there is a lack of supporting tools for modeling and verifying SoS and SoS-level goal achievements.
Features
SIMVA-SoS is a software for simulating and verifying the SoS. SoS models, given by users, are converted to executable SoS models and those become the inputs of simulation engine. Another input for simulation engine is SoS scenario data which is based on a target SoS. For verification, SoS goal and its verification property are input of the verification engine. A user can verify the satisfaction of goal and verification property of an SoS supported by SIMVA-SoS.
Bellows are key features of simulation and verification.
- 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.
- 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.
- 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.
Figure: Architecture of SIMVA-SoS
Figure: User Interface of SIMVA-SoS Simulation
Related Publications
- Mingyu Jin, Donghwan Shin, and Doo-Hwan Bae, “ABC+: Extended Action-Benefit-Cost Modeling with Knowledge-based Decision-Making and Interaction Model for System of Systems Verification,” 33rd ACM/SIGAPP Symposium On Applied Computing (SAC), 2018.
- Dongwon Seo, Donghwan Shin, Young-Min Baek, Jiyoung Song, Wonkyung Yun, Junho Kim, Eunkyoung Jee, Doo-Hwan Bae, “Modeling and Verification for Different Types of System of Systems using PRISM”, ICSE 4th International Workshop on Software Engineering for Systems-of-Systems (SESoS), 2016
- 서동원, 신동환, 박지훈, 지은경, 배두환, “시스템 오브 시스템즈 목표 검증을 위한 시뮬레이션 사례 연구”, 제 18회 한국 소프트웨어공학 학술대회 [KCSE 2016], pp.203-206, 2016년 01월.
- 김준호, 신동환, 배두환, “시스템 오브 시스템즈 대상 행동–이익–비용 모델링 및 통계적 모델 체킹 기반 속성 검증 사례 연구”, 한국컴퓨터종합학술대회 논문집 [KCC 2016], pp.625-627, 2016년 07월.
- 김준호, 배두환, 신동환, “시스템 오브 시스템즈 수준의 목표 달성 검증을 위한 행동–이익–비용 모델과 통계적 모델 체킹 적용 연구”, 정보과학회 컴퓨팅의 실제 논문지, 제23권, 제4호, pp.256-261, 2017년 4월.