×

zbMATH — the first resource for mathematics

Model checking of time Petri nets using the state class timed automaton. (English) Zbl 1113.68068
Summary: In this paper, we propose a method for building the state class graph of a bounded Time Petri Net (TPN) as a Timed Automaton (TA), which we call the state class timed automaton. We consider bounded TPN, whose underlying net is not necessarily bounded. We prove that our translation preserves the behavioral semantics of the TPN (the initial TPN and the obtained TA are proved timed-bisimilar). It allows us to check real-time properties on TPN by using the state class TA. This can be done efficiently thanks to a reduction of the number of clocks. We have implemented the method, and give some experimental results illustrating the efficiency of the translation algorithm in terms of number of clocks. Using the state class TA, we also give a framework for expressing and efficiently verifying TCTL properties on the initial TPN.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
93C65 Discrete event control/observation systems
93A30 Mathematical modelling of systems (MSC2010)
Software:
Kronos; SENAC; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla PA, Nylén A (2001). Timed petri nets and bqos. In 22nd International Conference on Application and Theory of Petri Nets (ICATPN’01), Newcastle upon Tyne, United Kingdom, Vol. 2075 of Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, pp 53–72. · Zbl 0986.68092
[2] Alur R, Courcoubetis C, Dill DL (1993). Model-checking in dense real-time, Information and Computation, 104(1): 2–34. · Zbl 0783.68076 · doi:10.1006/inco.1993.1024
[3] Arnold A (1994). Finite Transition System. Prentice Hall.
[4] Berthomieu B (2001). La méthode des classes d’états pour l’analyse des réseaux temporels. In 3e congrès Modélisation des Systèmes Réactifs (MSR’2001) Hermes France: Toulouse, pp. 275–290.
[5] Berthomieu B, Diaz M (1991). Modeling and verification of time dependent systems using time petri nets, IEEE Transactions on Software Engineering, 17(3): 259–273. · Zbl 05113493 · doi:10.1109/32.75415
[6] Berthomieu B, Vernadat F (2003). State class constructions for branching analysis of time Petri nets. In 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’2003) Springer, Berlin Heidelberg New York, pp. 442–457. · Zbl 1031.68082
[7] Bornot S, Sifakis J, Tripakis S (1998). Modeling urgency in timed systems, Lecture Notes in Computer Science, 1536: 103–129. · doi:10.1007/3-540-49213-5_5
[8] Bowden F DJ (1996). Modelling time in petri nets. In 2nd Australia–Japan Workshop on Stochastic Models in Engineering, Technology and Management. Australia: Gold Coast.
[9] Dantzig GB (1963). Linear programming and extensions. IEICE Transactions on Information and Systems. · Zbl 0108.33103
[10] Daws C, Yovine S (1996). Reducing the number of clock variables of timed automata. In 1996 IEEE Real-Time Systems Symposium (RTSS’96). Washington, District of Columbia: IEEE Computer Society, pp 73–81.
[11] de Frutos Escrig D, Valero Rui, V, Marroquín Alonso O (2000). Decidability of properties of timedarc petri nets. In 21st International Conference on Application and Theory of Petri Nets (ICATPN’00),Aarhus, Denmark, Vol. 1825 of Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York, pp. 187–206. · Zbl 0986.68077
[12] Delfieu D, Molinaro P, Roux OH (2000). Analyzing temporal constraints with binary decision diagrams. In 25th IFAC Workshop on Real-Time Programming (WRTP’00). Palma, Spain, pp. 131–136.
[13] Diaz M, Senac P (1994). Time stream Petri nets: a model for timed multimedia information, Lecture Notes in Computer Science, 815: 219–238.
[14] Gardey G, Roux OH, Roux OF (2006). State space computation and analysis of time Petri nets. Theory and Practice of Logic Programming (TPLP). Special Issue on Specification Analysis and Verification of Reactive Systems, (to appear).
[15] Henzinger TA, Nicollin X, Sifakis J, Yovine S (1994). Symbolic model checking for real-time systems, Information and Computation, 111(2): 193–244. · Zbl 0806.68080 · doi:10.1006/inco.1994.1045
[16] Khansa W, Denat J-P, Collart-Dutilleul S (1996). P-Time Petri Nets for manufacturing systems. In International Workshop on Discrete Event Systems, WODES’96. UK: Edinburgh, pp 94–102.
[17] Larsen KG, Pettersson P, Yi W (1995). Model-checking for real-time systems. In Fundamentals of Computation Theory, pp 62–88.
[18] Larsen KG, Pettersson P, Yi W (1997). UPPAAL in a nutshell, International Journal on Software Tools for Technology Transfer, 1(1–2): 134–152. · Zbl 1060.68577 · doi:10.1007/s100090050010
[19] Lilius J (1999). Efficient state space search for time petri nets. In MFCS Workshop on Concurrency ’98. Vol. 18 of ENTCS. Elsevier.
[20] Lime D, Roux OH (2004). http://romeo.rts-software.org.
[21] Menasche M (1982) Analyse des réseaux de Petri temporisés et application aux systèmes distribués. PhD thesis. Université Paul Sabatier. France: Toulouse
[22] Merlin PM (1974). A study of the recoverability of computing systems, PhD thesis, Department of Information and Computer Science, University of California, Irvine, California.
[23] Penczek W, Polrola A (2004). Specification and model checking of temporal properties in time Petri nets and timed automata. In The 25th International Conference on Application and Theory of Petri Nets, (ICATPN 2004). Vol. 3099 of Lecture Notes in Computer Science, Italy, Bologna. Springer, Berlin Heidelberg New York. · Zbl 1094.68067
[24] Pezze M, Toung M (1999). Time Petri nets: a primer introduction. Tutorial presented at the Multi-Workshop on Formal Methods in Performance Evaluation and Applications, Zaragoza, Spain.
[25] Popova L (1991). On time petri nets, Journal Information Processing and Cybernetics, EIK, 27(4): 227–244. · Zbl 0731.68082
[26] Ramchandani C (1974). Analysis of asynchronous concurrent systems by timed Petri nets. PhD thesis. Massachusetts Institute of Technology. Cambridge, Massachusetts. Project MAC Report MAC-TR-120.
[27] Roux O H, Déplanche A-M (2002). A t-time petri net extension for real time-task scheduling modeling, European Journal of Automation (JESA).
[28] Sava AT (2001). Sur la synthèse de la commande des systèmes à évènements discrets temporisés, PhD thesis, Institut National polytechnique de Grenoble, Grenoble, France.
[29] Sifakis J, Yovine S (1996). Compositional specification of timed systems (extended abstract). In 13th Syposium on Theoretical Aspects of Computer Science, France: Grenoble, Springer, Berlin Heidelberg New York, pp 347–359. · Zbl 1379.68240
[30] Toussaint J, Simonot-Lion F, Thomesse Jean-Pierre (1997). Time constraint verifications methods based time petri nets. In 6th Workshop on Future Trends in Distributed Computing Systems (FTDCS’97). Tunisia: Tunis, pp 262–267.
[31] Vicario E (2001). Static analysis and dynamic steering of time-dependent systems, IEEE Transactions on Software Engineering, 27(8): 728–748. · Zbl 05114174 · doi:10.1109/32.940727
[32] Yoneda T, Ryuba H (1998). CTL model checking of time petri nets using geometric regions, IEICE Transactions on Information and Systems, E99-D(3): 297–396.
[33] Yovine S (1997). Kronos: a verification tool for real-time systems, International Journal of Software Tools for Technology Transfer, 1(1–2): 123–133. · Zbl 1060.68606 · doi:10.1007/s100090050009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.