Abstract
We discuss in this paper the consistency of time Petri net semantics when assuming a monoserver hypothesis. This hypothesis assumes that for a given marking of the net, only one instance of an enabled transition should be considered. We show that for unsafe nets, the standard semantics is not sound and may induce false behaviors in presence of conflicting transitions. To fix this problem, we propose a new semantics that removes these incoherences by managing accurately after each firing the status of enabled transitions. We prove that our semantics is sound when assuming a monoserver hypothesis.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berthomieu, B., Diaz, M.: Modeling and verification of time dependant systems using Time Petri Nets. IEEE Transactions on Software Engineering 17(3), 259–273 (1991)
Berthomieu, B.: La méthode des classes d’états pour l’analyse des réseaux temporels. In: Modélisation des Systèmes Réactifs (MSR 2001), Toulouse, France (October 2001), pp. 275–290 (2001) Hermes
Boucheneb, H., Rakkay, H.: A More Efficient Time Petri Net State Space Abstraction Useful to Model Checking Timed Linear Properties. Fundam. Inform. 88(4), 469–495 (2008)
Merlin, P.: A study of the recoverability of computer system. PHD Thesis Dep. Computer. Science, Univ. California, Irvine (1974)
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: When are Timed Automata weakly timed bisimilar to Time Petri Nets? Theor. Comput. Sci. 403(2-3), 202–220 (2008)
Vicario, E.: Static Analysis and Dynamic Steering of Time-Dependent Systems. IEEE Trans. Software Eng. 27(8), 728–748 (2001)
TINA Tool, http://www.laas.fr/tina/
ROMEO TOOL, http://romeo.rts-software.org
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abdelli, A. (2009). Towards a Consistent Semantics for Unsafe Time Petri Nets. In: Ślęzak, D., Kim, Th., Kiumi, A., Jiang, T., Verner, J., Abrahão, S. (eds) Advances in Software Engineering. ASEA 2009. Communications in Computer and Information Science, vol 59. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10619-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-10619-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10618-7
Online ISBN: 978-3-642-10619-4
eBook Packages: Computer ScienceComputer Science (R0)