Advertisement

Time Petri Nets with Dynamic Firing Dates: Semantics and Applications

  • Bernard Berthomieu
  • Silvano Dal Zilio
  • Łukasz Fronc
  • François Vernadat
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8711)

Abstract

We define an extension of time Petri nets such that the time at which a transition can fire, also called its firing date, may be dynamically updated. Our extension provides two mechanisms for updating the timing constraints of a net. First, we propose to change the static time interval of a transition each time it is newly enabled; in this case the new time interval is given as a function of the current marking. Next, we allow to update the firing date of a transition when it is persistent, that is when a concurrent transition fires. We show how to carry the widely used state class abstraction to this new kind of time Petri nets and define a class of nets for which the abstraction is exact. We show the usefulness of our approach with two applications: first for scheduling preemptive task, as a poor man’s substitute for stopwatch, then to model hybrid systems with non trivial continuous behavior.

Keywords

Global Error Static Time Interval Time Automaton Time Automaton Reachable Marking 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Berthomieu, B., Vernadat, F.: State class constructions for branching analysis of time petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 442–457. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time petri nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 211–225. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  3. 3.
    Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. on Software Engineering 17(3), 259–273 (1991)CrossRefMathSciNetGoogle Scholar
  4. 4.
    Berthomieu, B., Lime, D., Roux, O.H., Vernadat, F.: Reachability problems and abstract state spaces for time Petri nets with stopwatches. Journal of Discrete Event Dynamic Systems 17, 133–158 (2007)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Berthomieu, B., Menasche, M.: A state enumeration approach for analyzing time Petri nets. In: Proc. of ATPN, Applications and Theory of Petri Nets (1982)Google Scholar
  6. 6.
    Berthomieu, B., Peres, F., Vernadat, F.: Bridging the gap between timed automata and bounded time petri nets. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 82–97. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    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(14), 2741–2756Google Scholar
  8. 8.
    Boniol, F., Wiels, V.: The landing gear system case study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. CCIS, vol. 433, pp. 1–18. Springer, Heidelberg (2014)Google Scholar
  9. 9.
    Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theoretical Computer Science 321(23), 291–345 (2004)CrossRefzbMATHMathSciNetGoogle Scholar
  10. 10.
    Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Timed state space analysis of real-time preemptive systems. IEEE Transactions on Software Engineering 30(2) (2004)Google Scholar
  11. 11.
    Cellier, F.-E., Kofman, E.: Continuous System Simulation. Springer (2006)Google Scholar
  12. 12.
    Cellier, F.-E., Kofman, E., Migoni, G., Bortolotto, M.: Quantized state system simulation. In: Proc. GCMS 2008, Grand Challenges in Modeling and Simulation (2008)Google Scholar
  13. 13.
    Daws, C., Yovine, S.: Two examples of verification of multirate timed automata with kronos. In: Proc. of RTSS, IEEE Real-Time Systems Symposium (1995)Google Scholar
  14. 14.
    Foures, D., Albert, V., Nketsa, A.: Formal compatibility of experimental frame concept and FD-DEVS model. In: Proc. of MOSIM, International Conference on Modeling, Optimization and Simulation (2012)Google Scholar
  15. 15.
    Gardey, G., Lime, D., Magnin, M., Roux, O(H.): Romeo: A tool for analyzing time petri nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Merlin, P.M.: A study of the recoverability of computing systems. PhD thesis, Department of Information and Computer Science, University of California (1974)Google Scholar
  17. 17.
    Nasr, O., Rached, M., Bodeveix, J.-P., Filali, M.: Spécification et vérification d’un ordonnanceur en B via les automates temporisés. L’Objet 14(4) (2008)Google Scholar
  18. 18.
    Ramalingam, G., Song, J., Joscovicz, L., Miller, R.E.: Solving difference constraints incrementally. Algorithmica 23 (1995)Google Scholar
  19. 19.
    Dal Zilio, S., Fronc, L., Berthomieu, B., Vernadat, F.: Time petri nets with dynamic firing dates: Semantics and applications. Technical Report 14148, LAAS-CNRS (2014) arXiv: 1404.7067Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Bernard Berthomieu
    • 1
    • 2
  • Silvano Dal Zilio
    • 1
    • 2
  • Łukasz Fronc
    • 1
    • 2
  • François Vernadat
    • 1
    • 3
  1. 1.CNRS, LAASToulouseFrance
  2. 2.Université de Toulouse, LAASToulouseFrance
  3. 3.Université de Toulouse, INSA, LAASToulouseFrance

Personalised recommendations