Advertisement

Abstract

An assertional proof system is proposed for a shared variable language extended with real-time constructs and synchronization, and a layering operator. The proof system is used to check real-time side conditions for an extended Communication Closed Layers rule. Reversely, this rule extends the scope of applicability of the proof system. The resulting system combines algebraic and assertional reasoning. A number of small examples are discussed.

Keywords

Proof System Delay Statement Mutual Exclusion Sequential Composition Parallel Composition 
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. [AL92]
    M. Abadi and L. Lamport. An old-fashioned recipe for real time. In de Bakker, Huizing, de Roever, and Rozenberg, editors, Real-Time: Theory in Practice, LNCS 600, pages 1–27. Springer-Verlag, 1992.Google Scholar
  2. [BG86]
    G. Berry and G. Gontier. The synchronous programming language esterel, design, semantics, implementation. Science of Computer Programming, 1986.Google Scholar
  3. [BHG87]
    P.A. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987.Google Scholar
  4. [CASD85]
    F. Cristian, H. Aghili, R. Strong, and D. Dolev. Atomic broadcast: From simple message diffusion to byzantine agreement. In Proceedings 15th International Symposium on Fault-Tolerant Computing, 1985.Google Scholar
  5. [Fid93]
    C. Fidge. A constraint-oriented real-time process calculus. In M. Diaz and R. Groz, editors, Formal Description Techniques, pages 363–378. Elsevier Science Publishers, 1993.Google Scholar
  6. [Hoo91]
    J. Hooman. Specification and Compositional Verification of Real-Time Systems. Springer-Verlag Lecture Notes in Computer Science 558, 1991.Google Scholar
  7. [Jan94]
    W. Janssen. Layered Design of Parallel Systems. PhD thesis, University of Twente, 1994. (to appear).Google Scholar
  8. [JPZ91]
    W. Janssen, M. Poel, and J. Zwiers. Action systems and action refinement in the development of parallel systems. In Proceedings of CONCUR '91, LNCS 527, pages 298–316. Springer-Verlag, 1991.Google Scholar
  9. [JZ92a]
    W. Janssen and J. Zwiers. From sequential layers to distributed processes, deriving a distributed minimum weight spanning tree algorithm, (extended abstract). In Proceedings 11th ACM Symposium on Principles of Distributed Computing, pages 215–227. ACM, 1992.Google Scholar
  10. [JZ92b]
    W. Janssen and J. Zwiers. Protocol design by layered decomposition, a compositional approach. In J. Vytopil, editor, Proceedings Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 571, pages 307–326. Springer-Verlag, 1992.Google Scholar
  11. [MK93]
    Y. Moses and O. Kislev. Knowledge-oriented programming, (extended abstract). In Proceedings 12th ACM Symposium on Principles of Distributed Computing, pages 261–270. ACM, 1993.Google Scholar
  12. [OG76]
    S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319–340, 1976.Google Scholar
  13. [PZ92]
    M. Poel and J. Zwiers. Layering techniques for development of parallel systems. In G. v. Bochmann and D. Probst, editors, Proceedings Computer Aided Verification, LNCS 663, pages 16–29. Springer-Verlag, 1992.Google Scholar
  14. [PZ93]
    M. Poel and J. Zwiers. Closed layers in the presence of conspiracy and cascading. Preliminary report, 1993.Google Scholar
  15. [RH92]
    F. Rocheteau and N. Halbwachs. Implementing reactive programs on circuits: A hardware implementation of lustre. In de Bakker, de Roever, and Rozenberg, editors, Real-Time: Theory in Practice, LNCS 600, pages 195–208. Springer-Verlag, 1992.Google Scholar
  16. [SBM92]
    F. Schneider, B. Bloom, and K. Marzullo. Putting time into proof outlines. In de Bakker, de Roever, and Rozenberg, editors, Real-Time: Theory in Practice, LNCS 600, pages 618–639. Springer-Verlag, 1992.Google Scholar
  17. [Zho93]
    P. Zhou. Clocks, Communications, and Correctness. PhD thesis, University of Eindhoven, 1993.Google Scholar
  18. [ZJ94]
    J. Zwiers and W. Janssen. Partial order based design of concurrent systems. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX School/Symposium “A Decade of Concurreny”, Noordwijkerhout, 1993, LNCS 803, pages 622–684. Springer-Verlag, 1994.Google Scholar
  19. [Zwi91]
    J. Zwiers. Layering and action refinement for timed systems. In de Bakker, Huizing, de Roever, and Rozenberg, editors, Real-Time: Theory in Practice, LNCS 600, pages 687–723. Springer-Verlag, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Wil Janssen
    • 1
  • Mannes Poel
    • 1
  • Job Zwiers
    • 1
  • Qiwen Xu
    • 2
  1. 1.Department of Computer ScienceUniversity of TwenteAE EnschedeThe Netherlands
  2. 2.Department of Computer Scienceåbo AkademiTurkuFinland

Personalised recommendations