Formal Specification Of Asynchronous Distributed Real-time Systems By APTL

We propose a language, Asynchronous Propositional Temporal Logic (APTL), for the specification and verification of asynchronous hard-real-time systems. APTL extends the logic TPTL [1] by explicitly introducing local clocks whose numerical readings cannot be arithmetically compared to determine temporal precedence. To interprete timing inequalities involving different local clocks, we introduce an asynchronous distributed system model which interpretes timing inequalities in terms of the temporal precedence of local clock readings. With this model, we give the formal semantic definition of APTL formulas. APTL is especially useful for specifying and reasoning about properties inherent in asynchronous environments such as the bounded drift rates of local clocks. Two versions of a railroad crossing example are used to illustrate the expressiveness of APTL.