Predicting logical and temporal properties of real-time systems using Synchronized Elementary Nets
SENS (Synchronised Elementary Net Systems) are derived from low level Petri nets “Condition/events systems” by adding temporal notions. They are used to describe and analyse real-time systems as a set of cooperating sub-systems. Each sub-system, also called a region, has its own logical clock used to specify temporal constraints in the region. Due to these characteristics, SENS can easily be implemented as synchronous programs written with the ESTEREL language.
We present in this paper an approach for building the reachability graph of SENS. Each node of this graph is a set of states equivalent from a logical and temporal points of view and arcs represent occurrences of atomic actions (events) inside an specific interval of time. The reachability graph can be used not only for checking logical properties like deadlocks, liveness, home states but also to predict the minimum and maximum bounds of any sequence of actions, including cyclic sequences.
Keywordstime Petri net reachability graph performance analysis
Unable to display preview. Download preview PDF.
- [ACH92]R.Alur„ N.Halbwachs: “Minimization of timed transition systems”, CONCUR'92, LNCS 630.Google Scholar
- [AlD90]R.Alur, D.Dill: “Automata for modelling real-time systems”, ICALP'90, LNCS 443.Google Scholar
- [AlD94]R. Alur, D. Dill: “A theory of timed automata”, Theoritical Computer Sciences 126 1994, 183–235.Google Scholar
- [And89]C.André “Synchronized Elmentary Net Systems”. Advances in Petri Nets 1989, Grzegorz Rozenberg editor, LNCS 424, Springer-Verlag.Google Scholar
- [BeG88]G.Berry, G.Gonthier “The synchroneous Programming Language ESTEREL: Design, Semantic, Implementation”. INRIA report 842, 1988.Google Scholar
- [BeM83]B. Berthomieu, M. Menasche “An enumerative approach for analyzing time Petri nets”. IFIP Congress 1983, Paris, North-Holland.Google Scholar
- [BeD91]B.Berthomieu, M. Diaz “Modeling and verification of time dependent systems using time Petri nets”, IEEE Transactions on Software Engineering vol 17, Nℴ3, March 91.Google Scholar
- [CoY91]C.Courcoubetis, M.Yannakakis: “Minimum and Maximum Delay problems in Real-time systems”. CAV'91,LNCS 575.Google Scholar
- [Fan90]L.Fancelli “Méthode de conception mixte asynchrone/synchrone pour la réalisation de systèmes de commande de processus discontinus”, Thèse de docteur en sciences, université de Nice-Sophia-Antipolis, Juillet 90.Google Scholar
- [HNSY92]T.A.Henzinger, X.Nicollin, J.Sifakis, S.Yovine: “Symbolic Model Checking for Real-Time Systems”. In Procedings of the Seventh iEEE Symposium on Logic in Computer Science, 1992.Google Scholar
- [MeF76]P.Merlin, D.J.Farber, “Recovability of communication protocols”. IEEE Trans. on Communications, 24 (1976).Google Scholar
- [Pop91]L. Popova. “On Time Petri Nets”, J. Inform. Process. Cybern., EIK 27 (1991) 4.Google Scholar
- [Pop93]L. Popova. “Petri Nets with Time Restrictions”, SAMS, 1993, Vol. 13, pp. 13–20.Google Scholar