Area of Application
SAVE is developed to specify operational requirements of distributed modile real-time systems with a process algebra, called d-Calculus, and to verify the secure requirements of the systems with a logic, called GTS logic. SAVE provides users with a suite of visual tools for both the specification and the verificaiton: ITL and ITS Modellers, EM(Execution Model) Generator, Simulator and Analyzer.
Abstract
SAVE is a final output of the project to develop a suite of tools to visualize an engineering process to model distributed modile real-time systems. The process consists of specification of both operational and secure requirements of the systems using d-Calculus and GTS Logic, generation of all the possible executions of the operational requirements based on its execution model, simulation of every and each execution, and verification of the secure requirements from the results of the simulation. SAVE provides a suite of visual tools for each steps of the process: ITL ans ITS Modelers for the specification of the operational srererequirements, EM Generator for the generation of the execution model, Simulator for the simulation of every and each execution case, and Analyzer for the specification and verification of the secure requirements. SAVE has been developed on ADOxx meta-modeling platform.
Approach
SAVE consists of the following components:
- 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:
- Operational requirements: These requirements are visually specified with a process algebra, called δ-Calculus. The calculus is designed to specify DMRTS, including IoT.
- 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.
- 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:
- Execution model: A visual execution model is generated for the operational specification. It contains all the possible cases of execution.
- 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.
- 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:
- PBC: http://moon.jbnu.ac.kr/index.php?mid=SAVE&document_srl=96258
- CryptoLocker: http://moon.jbnu.ac.kr/index.php?mid=SAVE&document_srl=96322
- EMS A (Simple Version): http://moon.jbnu.ac.kr/index.php?mid=SAVE&document_srl=96338
- 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).
Publications
Here is the list of publications related to SAVE:
- S. Lee, Y. Choe, M. Lee, A Dual Method to Model IoT Systems, International Journal of Mathematical Models and Methods in Applied Sciences, Vol. 10, pp. 201-219, May 2016.
- Y. Choe, M. Lee, A Process Algebra Construct Method for Reduction of States in Reachability Graph: Conjenctive and Complement Choices, Journal of KIISE, Vol. 43, No. 5, pp. 541-552, May 2016.
- Y. Choe, M. Lee, A Process Algebra for Modeling Secure Movements of Distrbuted Mobile Processes, Journal of KIISE, Vol. 43, No. 3, pp. 314-326, March 2016.
- Y. Choe, M. Lee, et. Al., A Tool for Visual Specification and Verification for Secure Process Movements, eChallenge 2015, Nov. 2015, Vilnius, Lithuania. The Best Paper.
- W. Choi, Y. Choe, M. Lee, A Reduction Method for Process and System Complexity with Conjunctive and Complement Choices in a Process Algebra, Proceedings of 23rd IEEE COMPSAC/MVDA, July 2015.
- Y. Choe, M. Lee, δ-Calculus: Process Algebra to Model Secure Movements of Distributed Mobile Processes in Real-Time Business Application, Proceedings of 23rd European Conference on Information Systems, May 2015.
- M. Lee, J. Choi, A Calculus for Transportation Systems, Proceedings of The 38th IEEE COMPSAC/MVDA, July 2014.
You can donwload the papers from: http://moon.jbnu.ac.kr/index.php?mid=SAVE&document_srl=96281