Object Petri nets marking using UML Online publication date: Wed, 05-Jun-2013
by Thouraya Bouabana-Tebibel; Lila Méziani
International Journal of Computer Applications in Technology (IJCAT), Vol. 47, No. 2/3, 2013
Abstract: UML semantics formalisation has aroused much interest these two last decades. Among the numerous proposed works many undertake the formalisation by translation into state-transition languages. The verification is afterwards performed by model-checking. However, one important issue raised by model checking is the state space explosion. The purpose of this paper will mainly address this issue. It is threefold. We first propose an approach to mark the derived formalisms starting from any time of the system lifecycle. The marking is drawn from the object and sequence diagrams. We secondly exploit the association ends modelled on the object diagram to retrieve the first action of each object behaviour. This contribution ensures a strong consistency when handling the object and sequence diagrams. We finally propose a method based on the association end formalisation in order to deal with the models validation. The whole of the solution is analysed by model checking.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Computer Applications in Technology (IJCAT):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com
Our Blog 
Follow us on Twitter 
Visit us on Facebook