Search

A formal method is proposed for the specification and verification of embedded real-time systems. We consider distributed systems in which parallel processes communicate by sending messages along synchronous or asynchronous channels. To verify that a program satisfies a specification, a compositional proof system is given. Compositionality enables verification during the process of top-down program design. This is illustrated by an example of a rail road crossing. Starting from an assertional specification, we design a program that controls lamps and barriers using information from sensors that signal the passage of trains at a certain distance from the crossing.

Formal methods to specify and verify concurrent programs with synchronous message passing are discussed. We stress the development towards compositional methods, i.e. methods in which the specification of a compound program can be inferred from specifications of its constituents without reference to the internal structure of those parts. Compositionality enables verification during the process of (top-down) design — the derivation of correct programs — instead of the more familiar a-posteriori verification based on already completed program codes. We sketch the transition from non-compositional towards compositional methods for concurrent programs, indicating the main principles behind compositionality. Having achieved a compositional framework based on classical Hoare triples, we discuss extensions to achieve a convenient formalism to specify and verify reactive systems that have an intensive interaction with their environment. Next this Hoare-style framework is adapted to specify and verify real-time properties, and a compositional proof method is formulated for real-time distributed computing. Compositional reasoning during top-down development of a real-time program is illustrated by an example concerning a watchdog timer.