Blending Timed Formal Models with Clock Transition Systems

• Autorzy: Jard C. , Lime D. , Roux O.H.

Identyfikatory

DOI

10.3233/FI-2014-962

• Języki publikacji: EN

Abstrakty

EN

Networks of Timed Automata (NTA) and Time Petri Nets (TPNs) are well-established formalisms used to model, analyze and control industrial real-time systems. The underlying theories are usually developed in different scientific communities and both formalisms have distinct strong points: for instance, conciseness for TPNs and a more flexible notion of urgency for NTA. The objective of the paper is to introduce a new model allowing the joint use of both TPNs and NTA for the modeling of timed systems. We call it Clock Transition System (CTS). This new model incorporates the advantages of the structure of Petri nets, while introducing explicitly the concept of clocks. Transitions in the network can be guarded by an expression on the clocks and reset a subset of them as in timed automata. The urgency is introduced by a separate description of invariants. We show that CTS allow to express TPNs (even when unbounded) and NTA. For those two classical models, we identify subclasses of CTSs equivalent by isomorphism of their operational semantics and provide (syntactic) translations. The classical state-space computation developed for NTA and then adapted to TPNs can easily be defined for general CTSs. Armed with these merits, the CTS model seems a good candidate to serve as an intermediate theoretical and practical model to factor out the upcoming developments in the TPNs and the NTA scientific communities.

Słowa kluczowe

EN

real-time systems; timed models; Timed Automata; time Petri nets

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 129, nr 1/2
• Strony: 85--100
• Opis fizyczny: Bibliogr. 20 poz.

Twórcy

autor

Jard C.

• Université de Nantes, LINA, Nantes, France

autor

Lime D.

• École Centrale de Nantes, IRCCyN, Nantes, France

autor

Roux O.H.

• École Centrale de Nantes, IRCCyN, Nantes, France

Bibliografia

• [1] Alur, R., Dill, D. L.: A theory of timed automata, Theoretical Computer Science, 126(2), 1994, 183–235.
• [2] Alur, R., Henzinger, T. A.: Real-time system = discrete system + clock variables, Theories and Experiences for Real-Time System Development, AMAST Series in Computing, 2, 1994.
• [3] Alur, R., Henzinger, T. A.: Real-time system = discrete system + clock variables, Software Tools for Technology Transfer, 1, 1997, 86–109.
• [4] Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O. H.: The Expressive Power of Time Petri Nets, Theoretical Computer Science, 474, 2013, 1–20.
• [5] Berthomieu, B., Diaz, M.: Modeling and Verification of Time Dependent Systems Using Time Petri Nets, IEEE trans. on Soft. Eng., 17(3), 1991, 259–273.
• [6] Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA – Construction of Abstract State Spaces for Petri Nets and Time Petri Nets, International Journal of Production Research, 42(4), July 2004.
• [7] Boucheneb, H., Gardey, G., Roux, O. H.: TCTL model checking of Time Petri Nets, Journal of Logic and Computation, 19(6), December 2009, 1509–1540.
• [8] Gardey, G., Roux, O. F., Roux, O. H.: Safety Control Synthesis for Time Petri Nets., 8th International Workshop on Discrete Event Systems (WODES’06), IEEE Comp. Soc. Press, Ann Arbor, USA, July 2006.
• [9] Grabiec, B., Traonouez, L.-M., Jard, C., Lime, D., Roux, O. H.: Diagnosis using Unfoldings of Parametric Time Petri Nets, Proceedings of FORMATS’10, 6246, Springer, Austria, September 2010.
• [10] Henzinger, T. A., Kopke, P. W., Wong-Toi, H.: The expressive power of clocks, Proceedings of the 22ndInternational Colloquium on Automata, Languages, and Programming (ICALP), 944, 1995.
• [11] Henzinger, T. A., Manna, Z., Pnueli, A.: Temporal Proof Methodologies for Timed Transitions Systems, Information and Computation, 112(2), 1994, 273–337.
• [12] Jard, C., Lime, D., Roux, O. H., Traonouez, L.-M.: Symbolic Unfolding of Parametric Stopwatch Petri Nets, Formal Methods in System Design, 2013, To appear.
• [13] Karp, R.M.,Miller, R. E.: Parallel program schemata, Journal of Computer and System Sciences, 3(2), 1969,147 – 195, ISSN 0022-0000.
• [14] Kesten, Y., Manna, Z., Pnueli, A.: Verifying Clocked Transition Systems, Hybrid Systems, 1066, 1996.
• [15] Larsen, K. G., Pettersson, P., Yi, W.: Model-Checking for Real-Time Systems, Proceedings of the 10thInternational Conference on Fundamentals of Computation Theory, LNCS 965, Dresden, Germany, 1995.
• [16] Larsen, K. G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell, International Journal on Software Tools for Technology Transfer, 1(1–2), Oct 1997, 134–152, Http://www.uppaal.com/.
• [17] Lime, D., Roux, O. H., Jard, C.: Clock Transition Systems, Technical report, Institut de Recherche enCommunications et Cybern´etique de Nantes (IRCCyN), 2012, Available on HAL as hal-00725792.
• [18] Lime, D., Roux, O. H., Seidner, C., Traonouez, L.-M.: Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches, 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), 5505, Springer, York, United Kingdom, March 2009.
• [19] Merlin, P. M.: A study of the recoverability of computing systems, Ph.D. Thesis, Dep. of Information and Computer Science, University of California, Irvine, CA, 1974.
• [20] Srba, J.: Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets, Proceedings of FORMATS’08, 5215, Springer, 2008.