From UML object behavior description into petri net models towards systematic development of embedded systems

The paper describes a translation of object behavior specified by UML into semantically equivalent Petri net models. The translation focuses on object behavior with event handling implemented in UML. The resulted Petri net allows to check UML model properties not only by simulation but also in formal way. For possibly closest congruence between UML and Petri net model an event queue is defined. Each state machine assigned to an object has its own event queue which is available as long as the machine exists. It allows modeling not just a simple message passing but also cases, when state machine cannot handle an event. A higher priority of sub-machine's event queue is also considered. The presented solution is a part of wider conversion algorithm from UML model into Petri nets [12]. However, the paper is intended to describe the issue in such a detailed way and focuses on aspects crucial for embedded systems development.