A Calculus to Reduce Spatial and Temporal Complexity for Specification and Analysis of Complex Real-Time Systems

In order to make the methods suitable to complex real-time systems (CRS), it is necessary to reduce the complexity of CRS with a large number of heavily interacting mobile agents over spatial-temporal space. To demonstrate the necessity of the reduction, this paper presents a new formal method, namely, calculus of real-time distribution, mobility, and interaction (CARDMI). In CARDMI, the spatial requirements are described in the spatial map, called Reconfigurable hyper graph (RHG), for the geographical space where agents move and interact. The space is dynamically reconfigurable through mobility. The behaviors of the agents, that is, movements and interactions, can be hierarchically represented, analyzed and verified on RHG. Consequently, the separate representation reduces the complexity dramatically and makes the development of CRS more realistic and practical for industrial applications. This paper presents TAG (timed action graph) for the graphical representation of the results of the execution. It shows the movements and interactions of agents are visually understandable over the hierarchically organized spatial domain along with the temporal dimension. For the implementation of the method, we have developed a new tool, called specification, analysis and verification environment (SAVE) to demonstrate the efficiency and effectiveness of the approach in the paper.