Advertisement

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 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.

Keywords

Decision Procedure Mixed Formalism Proof Rule Programming Construct Prototype Verification System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 2.
    C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580,583, 1969.Google Scholar
  3. 3.
    J. Hooman. Specification and Compositional Verification of Real-Time Systems. LNCS 558, Springer-Verlag, 1991.Google Scholar
  4. 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. 5.
    J. Hooman. Compositional verification of a distributed real-time arbitration protocol. Real-Time Systems, 6:173–205, 1994.Google Scholar
  6. 6.
    J. Hooman. Extending Hoare logic to real-time. Formal Aspects of Computing, To appear, 1994.Google Scholar
  7. 7.
    C. Morgan. Programming from Specifications. Prentice Hall, 1990.Google Scholar
  8. 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. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Jozef Hooman
    • 1
  1. 1.Dept. of Mathematics and Computing ScienceEindhoven University of TechnologyMB EindhovenThe Netherlands

Personalised recommendations