Specification and verification of timing properties of distributed real-time systems

The authors present a formalism for the specification and analysis of the timing properties of distributed real-time systems. This formalism is based on the real-time logic of F. Jahanian and A. Mok (1986) and it incorporates multiple occurrence functions to take care of the multiple unsynchronized clocks in a distributed system. This is a three-level approach to formal specification and verification of the timing properties of a system. In the first level of specification, the system is described in an event-action model. In the second level, this specification is mechanically transformed into a set of DRTL formulas for carrying out the safety analysis in the next level. DRTL is a first-order logic. The fundamental constraints that a distributed real-time system needs to satisfy for the correctness of any formal reasoning about its timing properties are investigated