Title :
Time properties verification of UML/MARTE real-time systems
Author :
Louati, Aymen ; Barkaoui, Kamei ; Jerad, Chadlia
Author_Institution :
LR-SITI, Univ. Tunis El Manor, Tunis, Tunisia
Abstract :
UML and MARTE are standardized modeling languages widely used in industry for the design of realtime systems. However, formal verification at early phases of the system lifecycle for UML/MARTE models remains an open issue mainly for dependability features. In this paper, we show how we can provide a formal verification of time properties from a UML/MARTE description. For this, we translate this latter description expressed in Interaction Overview Diagrams (IOD) and Timing Diagrams (TD) into Timed Petri Nets (TPN). This resulting formal execution semantics allows using the Romeo model-checker to check the behavior of TPN and some time properties formulated in TCTL (Timed Computation Tree Logic). We illustrate the proposed approach on a case study derived from a real-time asynchronous system (Integrated Modular Avionics (IMA)-based airborne system).
Keywords :
Unified Modeling Language; formal verification; real-time systems; IMA-based airborne system; IOD; MARTE realtime system; Romeo model checker; TCTL; TD; TPN; UML realtime system; Unified Modeling Language; dependability feature; formal verification; integrated modular avionics system; interaction overview diagram; modeling languages; realtime asynchronous system; time properties verification; time property; timed Petri nets; timed computation tree logic; timing diagram; Delays; Formal verification; Real-time systems; Receivers; Time factors; Unified modeling language; TCTL; TPN; UML/MARTE; real-time;
Conference_Titel :
Information Reuse and Integration (IRI), 2014 IEEE 15th International Conference on
DOI :
10.1109/IRI.2014.7051915
