Verification of real time UML specifications through a specialized inference mechanism based on a token player algorithm and the sequent calculus of linear logic

The objective of this article is to present an approach based on UML dynamic diagrams, on time Petri Nets and Linear Logic for scenario verification of Real Time Systems. The main idea consists of translating the sequence diagrams which express the initial specifications of the system to a unique p-time Petri Net model which represents the global behaviour of the entire system. For the Petri Net fragments involved in conflict situations, symbolic production and consumption dates assigned to tokens are calculated using a non-conventional (max;+) algebra based on the sequent calculus of Linear Logic. These dates are then used to solve conflict situations within a token player algorithm used for scenario verification of Real Time specifications and which can be seen as a simulation tool for UML interaction diagrams. The approach is illustrated through an example of Real Time System used at the global coordination level of a Batch System.