A Graphical Language to Integrate Process Algebra and State Machine Views for Specification and Verification of Distributed Real-Time Systems

Being very large and extremely complex, distributed real-time systems are specified by formal methods, such as state machines and process algebras, and are verified by temporal and spatial logics. However the methods have some limitations in the specification and verification, since process algebras mainly focus on the in-the-large view of the systems and, relatively, state machines mainly focus on the in-the-small view of the systems. Consequently there is a strong need for some intermediate methods to integrate these two views into one view to handle the size and complexity of the systems effectively. This paper presents such a visual formalism, namely, Onion, where processes and their transitive actions in the systems are graphically represented in one single entity, just like those of a real onion, over a geographical space. Further the temporal properties of mobility and interactions of the processes are specified in a geo-temporal space. Once these are done, the temporal and spatial requirements for the systems are graphically specified on the processes and actions using a visual logic. Finally, the specifications are visually analyzed and verified through simulation on the space for the requirements. The comparative study shows that Onion is very effective and efficient for the visualization of the systems and that it overcomes the stated limitations.