Abstract
"How does reactive behaviour decompose? What can be done to encourage stepwise refinement of the behavioural aspects of a system? How can one cope with the intricacy, that the behaviour of a complex reactive system presents??" These questions, posed in [HP85] and informally discussed there in the setting of statecharts, are taken up in this paper using a particular class of Petri-Nets as models for open reactive systems. It presents an assumption/commitment style temporal logic [Pn85] for specifying the behaviour of such systems, an automatic proof method for verifying the correctness of an implementation of such a specification in terms of the considered class of Petri-Nets based on modelchecking of MCTL formula (discussed in a companion paper [Jo89]), and presents a proof-method for infering the behaviour of a compound reactive system from the behaviour of its constituents.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
H.Barringer, R.Kuiper: A Temporal Logic Specification Method Supporting Hierarchical Development, University of Manchester, 1983
H.Barringer, R.Kuiper, A.Pnueli: Now You May Compose Temporal Logic Specifications, Proc. 16th ACM Symposium on Theory of Computing, 1984, 51–63
E.M. Clarke, E.A. Emerson, A.P. Sistla: Automatic verification of finite-state concurrent systems using temporal logic specifications: a practical approach. Tenth ACM Symposium on principles of Programming Languages (1983)
W. Damm, G. Döhmen: Specifying Distributed Computer Architectures in AADL, Parallel Computing, Vol 9, 1988, 193–211
W.Damm, G.Döhmen: AADL: a Net-Based Specification Method for Computer Architecture Design, in: Languages for Parallel Architectures: Design, Semantics, and Implementation Models", edt. J.de Bakker, Wiley & Sons, 1989
W.Damm, G.Döhmen, V.Gerstner, J.Helbig, B.Josko, F.Korf, T.Peikenkamp: AADL Language Document, University of Oldenburg, FRG, 1989
P.Degano, R.Gorrieri, S.Machetti: An excercise in concurrency: a CSP process as a Condition/Event system, Advances on Petri-Nets 1988, edt G.Rozenberg, Lecture Notes in Computer science 340, Springer Verlag, 1988, 83–105
E.A. Emerson, E.M. Clarke: Using branching time temporal logic to synthesisze synchronization skeletons, Science of Computer Programming, Vol 2, 1982, 241–266
E.A. Emerson, J.Y. Halpern: Sometimes and not never revisited: On branching time versus linear time. 10th ACM Symposium on Principles of programming Languages. 1983
E.A. Emerson, J.Y. Halpern: Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Science 30 (1985), pp. 1–24
B. Hailpern, S. Owicki: Modular Verification of Computer Communication Protocols, IEEE Trans. on Communication, Vol COM-31, 1983,56–68
D.Harel, A.Pnueli: On the Development of Reactive Systems, Nato ASI Series, Vol. F13, Logics and Models of Concurrent Systems, edt. K.Apt, Springer Verlag, 1985
M.Jazayeri, C.Ghezzi, D.Hoffman,. D.Middleton, M.Smotherman: Design and Implementation of a Language for Communicating Sequential Processes, IEEE Proc. 9th Int.Conf. on Parallel Processes, Harbor Spring, Michigan, USA, 1980
B. Josko: Modelchecking of CTL formulae under liveness assumptions. Proceedings ICALP 87. Lecture Notes in Computer Science 267 (1987), 280–289
B. Josko: Verifying the correctness of AADL-modules using model checking. Proceedings REX-Workshop on Stepwise refinement of Distributed systems: models, formalisms, correctness
F. Korf: M-CSP — eine modulare Sprache mit Prozeßkommunikation und ihre Implemntierung, Master Thesis, RWTH Aachen, 1987
J. Misra, K.M. Chandy: Proofs of Networks of Processes, IEEE Trans. Software Enginering. 7, 1981, 417–426
Z. Manna,P. Wolper: Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Toplas 6, 1984, 68–93
V.Nguyen, D.Gries, S.Owicki: A Model and Temporal Proof System for Network of Proceses, 12 POPL, 1985, 121–131
OCCAM Programming Manual, INMOS Ltd, Whitefriars, Lewins Mead, Bristol, England
A.Pnueli: In transition from Global to Modular Temporal Reasoning about Programs, in: Logics and Models of Concurrent Systems, edt. K.R.Apt, Springer Verlag, 1985, 123–144
A. Pnueli, Applications of Temporal Logic to the Specification and Verification of Reactive Systems: a Survey of Current Trends, in: Current Trends in Concurrency, edts. J.W.de Bakker, W.-P. de Roever, G.Rozenberg, Lecture Notes in Computer Science 224, Springer Verlag, 1986, 510–584
W. Reisig: Partial Order Semantics versus Interleaving Semantics of CSP-like languages and its Impact on Fairness, Lecture Notes in Computer Science 172, Springer Verlag, 1984, 403–413
S.P. Wolper: Specification and Synthesis of Communicating Processes using an extended Temporal Logic, POPL 82, 1982, 20–33
P.Wolper: Expressing INteresting Properties of Programs in Propositional Temporal Logic, 13th POPL, 1986, 184–193
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Damm, W., Döhmen, G., Gerstner, V., Josko, B. (1990). Modular verification of Petri Nets. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness. REX 1989. Lecture Notes in Computer Science, vol 430. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52559-9_65
Download citation
DOI: https://doi.org/10.1007/3-540-52559-9_65
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52559-2
Online ISBN: 978-3-540-47035-9
eBook Packages: Springer Book Archive