Correctness of real time systems by construction
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 PVS specification language, 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.
KeywordsDecision Procedure Mixed Formalism Proof Rule Programming Construct Prototype Verification System
Unable to display preview. Download preview PDF.
- 1.T. Anderson, R. de Lemos, J.S. Fitzgerald, and A. Saeed. On formal support for industrial-scale requirements analysis. In Workshop on Theory of Hybrid Systems, pages 426–451. LNCS 736, 1993.Google Scholar
- 2.C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580,583, 1969.Google Scholar
- 3.J. Hooman. Specification and Compositional Verification of Real-Time Systems. LNCS 558, Springer-Verlag, 1991.Google Scholar
- 4.J. Hooman. A compositional approach to the design of hybrid systems. In Workshop on Theory of Hybrid Systems, pages 121–148. LNCS 736, 1993.Google Scholar
- 5.J. Hooman. Compositional verification of a distributed real-time arbitration protocol. Real-Time Systems, 6:173–205, 1994.Google Scholar
- 6.J. Hooman. Extending Hoare logic to real-time. Formal Aspects of Computing, To appear, 1994.Google Scholar
- 7.C. Morgan. Programming from Specifications. Prentice Hall, 1990.Google Scholar
- 8.E. R. Olderog. Process theory: semantics, specification and verification. In ESPRIT/LPC Advanced School on Current Trends in Concurrency, pages 509–519. LNCS 194, Springer-Verlag, 1985.Google Scholar
- 9.S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In 11th Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752. Springer-Verlag, 1992.Google Scholar
- 10.J.U. SkakkebÆk and N. Shankar. Towards a duration calculus proof assistant in PVS. In Formal Techniques in Real-Time and Fault Tolerant Systems. LNCS, This Volume, Springer-Verlag, 1994.Google Scholar