Correctness of Real Time Systems by Construction

Jozef Hooman

Appeared in: Proceedings Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 863, Springer-Verlag, pages 19-40, 1994.

ABSTRACT

To design distributed real-time systems in a top-down way, we present a mixed formalism in which programs and assertional specifications are combined. Specifications consist of an assumption-commitment pair, extending Hoare logic to real-time and progress properties. By defining the theory in the specification language of the tool PVS (Prototype Verification System), the interactive proof checker of PVS can be used to reason in this framework. We show how this tool can be used during the design of real-time systems to derive programs that are correct by construction.

Dump file of all PVS theories of the chemical batch processing example.