Keywords: d-Calculus, GTS Logic, Specification, Verification, Visualization

Affiliation: Division of Computer Science and Engineering, Chonbuk National University, Republic of Korea

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.


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.