Formal Verification of UML2 Timing Diagrams based on Time Petri Nets

Aymen Louati and Kamel Barkaoui
Additional contact information
Aymen Louati: LR-SITI, Ecole Nationale d'Ingénieurs de Tunis, Université de Tunis El ManarTunisie, Tunis, Tunisia & Laboratoire Cedric, CNAM, Paris, France
Kamel Barkaoui: Laboratoire Cedric, CNAM, Paris, France

International Journal of Information Systems in the Service Sector (IJISSS), 2016, vol. 8, issue 2, 87-97

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.

Date: 2016
References: Add references at CitEc
Citations:

Downloads: (external link)
http://services.igi-global.com/resolvedoi/resolve. ... 18/IJISSS.2016040107 (application/pdf)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:igg:jisss0:v:8:y:2016:i:2:p:87-97

Access Statistics for this article

International Journal of Information Systems in the Service Sector (IJISSS) is currently edited by John Wang

More articles in International Journal of Information Systems in the Service Sector (IJISSS) from IGI Global
Bibliographic data for series maintained by Journal Editor ().