Abstract
We describe an algebraic technique for performing timing analysis on a restricted class of Petri nets with interval time delays specified on the places of the net. The timing analysis we perform determines the extreme separation in time between specified occurrences of pairs of transitions for all possible timed executions of the system. We present the details of the timing analysis algorithm and demonstrate polynomial running time on a non-trivial parameterized example. Petri nets with 3000 nodes and 1016 reachable states have been analyzed using these techniques.
This work is supported by an NSF YI Award (MIP-9257987) and by the DARPA/CSTO Microsystems Program under an ONR monitored contract (N00014-91-J-4041).
Chapter PDF
References
R. Alur and D. L. Dill. The theory of timed automata. In J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rosenberg, editors, Real-Time: Theory in Practice, LNCS #600, pages 28–73. Springer-Verlag, 1991.
F. Baccelli, G. Cohen, G. J. Olsder, and J.-P. Quadrat. Synchronization and Linearity. John Wiley and Sons, 1992.
B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, 17(3):259–273, 1991.
E. Best and J. Desel. Partial order behavior and structure of Petri nets. Formal Aspects of Computing, 2:123–138, 1990.
E. Best and Raymond Devillers. Interleaving and partial orders in concurrency: A formal comparison. In M. Wirsing, editor, Formal Description of Programming Concepts-III, pages 299–323, 1986.
J. R. Burch. Trace Algebra for Automatic Verification of Real-Time Concurrent Systems. Ph.D. thesis, Carnegie Mellon, August 1992.
C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-time systems. Formal Methods in System Design, 1:385–415, 1992.
D. L. Dill, editor. Computer-Aided Verification '94.
P. Godefroid. Using partial orders to improve automatic verification methods. In E. M. Clarke and R. P. Kurshan, editors, Computer-Aided Verification '90, pages 321–340.
H. Hulgaard and S. M. Burns. Bounded delay timing analysis of a class of CSP programs with choice. In International Symposium on Advanced Research in Asynchronous Circuits and Systems, November 1994.
H. Hulgaard, S. M. Burns, T. Amon, and G. Borriello. Practical applications of an efficient time separation of events algorithm. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 146–151, November 1993.
H. Hulgaard, S. M. Burns, T. Amon, and G. Borriello. An algorithm for exact bounds on the time separation of events in concurrent systems. To appear in IEEE Transactions on Computers. Available as University of Washington CS&E Technical Report #94-02-02. (anonymous ftp: cs.washington.edu:tr/1994/02/UW-CSE-94-02-02.PS.Z)
K. L. McMillan and D. L. Dill. Algorithms for interface timing verification. In 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, October 1992.
J. L. Peterson. Petri Net Theory and The Modeling of Systems. Prentice-Hall, 1981.
C. V. Ramamoorthy and G. S. Ho. Performance evaluation of asynchronous concurrent systems using Petri nets. IEEE Transactions on Software Engineering, SE-6(5):440–448, September 1980.
T. G. Rokicki. Representing and Modeling Digital Circuits. Ph.D. thesis, Stanford University, 1993.
T. G. Rokicki and C. J. Myers. Automatic verification of timed circuits. In D. L. Dill, editor, Computer-Aided Verification '94, pages 468–480.
W. Vogler. Modular Construction and Partial Order Semantics of Petri Nets. LNCS #625. Springer-Verlag, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hulgaard, H., Burns, S.M. (1995). Efficient timing analysis of a class of Petri nets. In: Wolper, P. (eds) Computer Aided Verification. CAV 1995. Lecture Notes in Computer Science, vol 939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60045-0_67
Download citation
DOI: https://doi.org/10.1007/3-540-60045-0_67
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60045-9
Online ISBN: 978-3-540-49413-3
eBook Packages: Springer Book Archive