Abstract
The PEP tool provides an integrated development and verification environment for parallel systems. Beginning with version 2.0 it also offers use of timed systems. This paper describes a sample session for the design and the verification by partial order based techniques of a simple real-time model for a mutual exclusion algorithm.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Abadi, M., Lamport, L.: An Old-Fashioned Recipe for Real-Time. In Real Time: Theory in Practice. Volume 600 of LNCS. Springer-Verlag (1992) 1–27
Best, E., Devillers, R., Hall, J.: The Box Calculus: a New Causal Algebra with Multi-Label Communication. In Proc. of APN’92. Volume 609 of LNCS. Springer-Verlag (1992) 21–69
Best, E., Hopkins, R.P.: B(PN)2-a Basic Petri Net Programming Notation. In Proc. of PARLE’93. Volume 694 of LNCS. Springer-Verlag (1993) 379–390
Bieber, B., Fleischhack, H.: Model Checking of Time Petri Nets Based on Partial Order Semantics. In Proc. of Concur’99. Volume 1664 of LNCS. Springer-Verlag (1999) 210–225
Esparza, J.: Model Checking Using Net Unfoldings. Science of Computer Programming 23. Elsevier (1994) 151–195
Esparza, J., Römer, S., Vogler, W.: An Improvement of McMillan’s Unfolding Algorithm. In Proc. of TACAS’96. Volume 1055 of LNCS. Springer-Verlag (1996) 87–106
Fleischhack, H., Grahlmann, B.: A Compositional Petri Net Semantics for SDL. In Proc. of ATPN’98. Volume 1420 of LNCS. Springer-Verlag (1998)
Fleischhack, H., Stehno, C.: Computing the Finite Prefix of a Time Petri Net. Submitted paper. 2001
Grahlmann, G., Moeller, M., Anhalt, U.: A New Interface for the PEP Tool—Parallel Finite Automata. In Proc. of AWPN’95, AIS 22. FB10 Universität Oldenburg (1995)
Heljanko, K.: Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets. In Proc. of TACAS’99. Volume 1579 of LNCS. Springer-Verlag (1999) 240–254
Jaeger, J.: Portable Codegenerierung für eine parallele Programmiersprache. Masters thesis. Universität Hildesheim (1997) in German
Khomenko, V., Koutny, M.: LP Deadlock Checking Using Partial Order Dependencies. In Proc. of CONCUR’2000. Volume 1877 of LNCS. Springer-Verlag (2000) 410–425
Koutny, M.: A Compositional Model of Time Petri Nets. In Proc. of Application and Theory of Petri Nets 2000. Volume 1825 of LNCS. Springer-Verlag (2000) 303–322
McMillan, K.: Symbolic model checking: An approach to the state explosion problem. Kluwer Academic Publishers (1993)
Merlin, P., Faber, D.: Recoverability of Communication Protocols—Implication of a Theoretical Study. IEEE Transactions on Software Communications 24 (1976) 1036–1043
Starke, P.: INA—Integrated Net Analyzer Version 2.2. Humboldt-Universität Berlin (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stehno, C. (2002). Real-Time Systems Design with PEP. In: Katoen, JP., Stevens, P. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2002. Lecture Notes in Computer Science, vol 2280. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46002-0_35
Download citation
DOI: https://doi.org/10.1007/3-540-46002-0_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43419-1
Online ISBN: 978-3-540-46002-2
eBook Packages: Springer Book Archive