Study Of Real-time Value-passing And Real-time Mobile Systems

Real-time systems are computational systems which must respond to externally generated stimuli or inputs within specified time limits. With extensive applications in industry and defence, formal analysis of real-time systems has been an important research area in recent years.During the last two decades, considerable efforts have been devoted into extending existing process theories with real-time features. However, most of these efforts were focused on so-called basic (or pure) calculi where processes running in parallel can only synchronize on signals rather than transmit messages. As most real-time concurrent systems do involve message-passing or link-passing, there is a need to develop formal models and algorithms which can be applied to real-time message-passing and mobile systems. This is the topic of the thesis.The main work of the thesis consists of modeling and analysing real-time value-passing systems and real-time mobile systems.The first work can be divided into three parts: computation model and semantics theory, algorithms for analysing and verification, as well as a tool for computer aided verification. First, a new model, TSTG (Timed Symbolic Transition Graph) is presented along with its semantics theory. An algorithm deciding timed bisimulation is developed based upon the idea of symbolic bisimulations. Model checking algorithms has played an very important role in verifying systems. So we present an algorithm based on reachability analysis, and a more complex one which uses a stronger temporal logic (timed predicate μ, calculus) and can verify more properties. To efficiently represent and manipulate continuous time semantics, an optimization method for eliminating redundant information is developed. Based on the above research, a tool named RealM is implemented and a case analysis of a real-time protocol is presented.Another work is on real-time mobile systems. A new computation model, Timed π calculus is presented, which is a real-time extension of the standard π calculus on continuous time domain. The syntax and the semantics of the calculus are given, and properties of timed bisimulations are examined. Finally, the strong ground bisimulation and strong bisimulation over a finite subset of Timed π are completely axiomatized.