Formal specification of asynchronous distributed real-time systems by APTL

1 January 1992

conference paper
Published by Association for Computing Machinery (ACM)

p. 188-198
https://doi.org/10.1145/143062.143113

Abstract

In this paper, 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 interpret timing inequalities involving different local clocks, we introduce an asynchronous distributed system model which interpreted 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 reasonil. ~ 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.

Keywords

This publication has 0 references indexed in Scilit: