Europe

Approach:

SAVE consists of the following components:

1. Visual specifications: It consists of specifications of both dynamic properties, such as operational requirements, of the system and static properties, such as safety properties, of the systems. These can be summarized as follows:
   1.  Operational requirements: These requirements are visually specified with a process algebra, called δ-Calculus. The calculus is designed to specify DMRTS, including IoT.
   2. Safety requirements: These requirements are visually specified with a first order logic, called GTS (Geo-Temporal Space) Logic. The logic is designed to reason geo-temporal properties of processes and their interactions on a specific geographical space.
2. Simulation: In order to verify the safety requirements for the dynamic requirements, it is necessary to generate all the possible execution cases for simulation. It is accomplished as follows:
   1.  Execution model: A visual execution model is generated for the operational specification. It contains all the possible cases of execution.
   2. Simulation: It simulates each individual case in the execution model. It represents the results of the simulation in a GTS block diagram, which will be input to Verifier for verification of the validity.
3. Verification: It verifies visually on the GTS block diagrams for the safety requirements in GTS Logic. The results of the verification will be displayed directly and visually on the diagrams.

Overview:

Overview with PBC Example: http://moon.jbnu.ac.kr/index.php?mid=SAVE&document_srl=96255

Manual:

Manual: http://moon.jbnu.ac.kr/index.php?mid=SAVE&document_srl=96361

Examples:

Selected examples are displayed in the following pages:

1. PBC: http://moon.jbnu.ac.kr/index.php?mid=SAVE&document_srl=96258
2. CryptoLocker: http://moon.jbnu.ac.kr/index.php?mid=SAVE&document_srl=96322
3. EMS A (Simple Version): http://moon.jbnu.ac.kr/index.php?mid=SAVE&document_srl=96338
4. EMS B (Midium Version): http://moon.jbnu.ac.kr/index.php?mid=SAVE&document_srl=96352

Acknowledgements:

This project was supported by Basic Science Research Programs through The National Research Foundation of Korea (NRF), funded by the Ministry of Education (2010-0023787), and the MISP (Ministry of Science, ICT and Future Planning), Korea, under the ITRC (Information Technology Research Center) support program (IITP-2016-H85011610120001002), supervised by the IITP (Institute for Information & communications Technology Promotion), and Space Core Technology Development Program through NRF, funded by the Ministry of Science, ICT and Future Planning (NRF-2014M1A3A3A02034792), and Basic Science Research Program through NRF, funded by the Ministry of Education (NRF-2015R1D1A3A01019282).