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.
Part of this work has been supported by Finnish Akademi Project Irene.
Part of this work has been supported by Esprit/BRA Project 6021 (REACT).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
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.
G. Berry and G. Gontier. The synchronous programming language esterel, design, semantics, implementation. Science of Computer Programming, 1986.
P.A. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987.
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.
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.
J. Hooman. Specification and Compositional Verification of Real-Time Systems. Springer-Verlag Lecture Notes in Computer Science 558, 1991.
W. Janssen. Layered Design of Parallel Systems. PhD thesis, University of Twente, 1994. (to appear).
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.
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.
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.
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.
S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319–340, 1976.
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.
M. Poel and J. Zwiers. Closed layers in the presence of conspiracy and cascading. Preliminary report, 1993.
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.
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.
P. Zhou. Clocks, Communications, and Correctness. PhD thesis, University of Eindhoven, 1993.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Janssen, W., Poel, M., Zwiers, J., Xu, Q. (1994). Layering of real-time distributed processes. In: Langmaack, H., de Roever, WP., Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT ProCoS 1994 1994. Lecture Notes in Computer Science, vol 863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58468-4_175
Download citation
DOI: https://doi.org/10.1007/3-540-58468-4_175
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58468-1
Online ISBN: 978-3-540-48984-9
eBook Packages: Springer Book Archive