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

Author

Mall, R. ; Patnaik, L.M.

Author_Institution

Dept. of Comput. Sci. & Autom., Indian Inst. of Sci., Bangalore, India

fYear

1990

fDate

24-27 Sep 1990

Firstpage

274

Abstract

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

Keywords

distributed processing; formal logic; formal specification; program verification; real-time systems; DRTL formulas; distributed real-time systems; event-action model; first-order logic; formal reasoning; formal specification; multiple occurrence functions; multiple unsynchronized clocks; real-time logic; safety analysis; timing properties; verification; Application software; Automatic control; Automation; Clocks; Computer aided manufacturing; Computer science; Control systems; Logic; Real time systems; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer and Communication Systems, 1990. IEEE TENCON'90., 1990 IEEE Region 10 Conference on

Print_ISBN

0-87942-556-3

Type

conf

DOI

10.1109/TENCON.1990.152615

Filename

152615