Formal Verification of UML2 Timing Diagrams based on Time Petri Nets

Formal Verification of UML2 Timing Diagrams based on Time Petri Nets

Aymen Louati (LR-SITI, Ecole Nationale d'Ingénieurs de Tunis, Université de Tunis El ManarTunisie, Tunis, Tunisia & Laboratoire Cedric, CNAM, Paris, France) and Kamel Barkaoui (Laboratoire Cedric, CNAM, Paris, France)
DOI: 10.4018/IJISSS.2016040107
OnDemand PDF Download:
$30.00
List Price: $37.50

Abstract

Unified Modeling Language (UML) is using in the design notation in industry and academia projects. Interesting by the critical Real-Time System verification, it is important to ensure its dependability in order to avoid eventual errors. In this paper, the authors aim to extend the UML diagrams by adding a formal verification stage. They tackle with the UML2 timing diagram (TD), as interaction diagram in order to describe the system's behavior in temporal way. For that, the authors give a formal description for TD using Time Petri Nets (TPN). Then, they propose a formal verification by means of Romeo Model Checker. In particular, they show how to formulate quantitative properties using TCTL (timed computation tree logic). In addition, the authors show how they can derive the TCTL formulae from Object Constraint Language-Real Time (OCLRT) constraints. Finally, they illustrate the proposed approach through a real case study.
Article Preview

2. Outline Tools

In this section, we introduce the basic concepts used in this work which are: TD, TPN, OCLRT and TCTL.

2.1. UML2 TD

Timing Diagram (TD) (OMG, 2012) is used to express state change of a value of one or more elements over time. Actually, it is used to further study the model in terms of time and duration constraints and the merge of the different elements such as lifeline, state, message, time constraint and duration constraint (see Figure 1).

Figure 1.

Timing Diagram example [Source: www.sparxsystems.com]

The TD life line shows the change of an item's state over time, while the state represents the set of the attributes values of an object. The duration constraint expresses the maintain time of the object state and the time constraint represents the time where each state transition can be released. Finally, a message represents a communication link between two life lines.

In this work, we propose a formal definition of UML2 TD which is inspired from the work proposed in (Joochim, 2010). So, the TD will be described using a model MTD as follows:

MTD = (Lf, Pt, Msg, State, Dc and Tc) where:

  • Lf = {lf1, .., lfk} represents a final set of life lines.

  • Pt = {pt1, .., ptk} represents a final set of interaction points relying all life lines to asynchronous messages.

  • Msg = {m1, .., mk} represents a final set of asynchronous messages exchanged between objects.

  • State = {st1, .., stk} represents a final set of objects states.

  • Dc = {dc1, .., dck} represents a final set of duration constraints.

  • Tc = {tc1, .., tck} represents a final set of time constraints.

Complete Article List

Search this Journal:
Reset
Open Access Articles: Forthcoming
Volume 10: 4 Issues (2018): 1 Released, 3 Forthcoming
Volume 9: 4 Issues (2017)
Volume 8: 4 Issues (2016)
Volume 7: 4 Issues (2015)
Volume 6: 4 Issues (2014)
Volume 5: 4 Issues (2013)
Volume 4: 4 Issues (2012)
Volume 3: 4 Issues (2011)
Volume 2: 4 Issues (2010)
Volume 1: 4 Issues (2009)
View Complete Journal Contents Listing