An approach based on dynamic UML diagrams and on a token player algorithm for the scenario verification of real time systems

The objective of this article is to present an approach based on UML dynamic diagrams and on p-time Petri Nets for scenario verification of Real Time Systems. The main idea consists of translating the sequence diagrams which express the initial specifications of the system in a unique p-time Petri Net model which represents the global behaviour of the entire system. A Token Player algorithm used for the scheduling problem of Real Time Systems and which can be seen as a simulation technique of a formal model is then applied to the obtained p-time Petri Net model for scenario verification. The approach is illustrated through an example of a batch system which can be seen as a particular case of a Real Time System.