A tool for visual specification and verification for secure process movements

This paper presents a tool, called SAVE, developed on the ADOxx meta-modelling platform, to implement a dual approach to specify and verify the requirements for secure movements of processes in distributed mobile real-time systems. For specification, a process algebra, called ö-Calculus, was visualized to define the movements of processes on a conceptual geographical space. For verification, a first-order logic, called GTS logic, was visualized to define the dependencies among the movements. Both visualization methods make the specification and verification of the systems more comprehensible and configurable. All the necessary visualization capabilities were fully supported by the graphical facilities of ADOxx. SAVE can be considered to be one of the unique tools for visualization of requirements and verification of the movements in the systems.