|
 
|
[LBJ14] Time properties Verification of UML/MARTE Real-Time Systems
Conférence Internationale avec comité de lecture : Proceedings of the 15th {IEEE} International Conference on Information Reuse and Integration, {IRI} 2014, August 2014, pp.386-393, Redwood City CA, USA,Mots clés: UML/MARTE, real-time, TPN, TCTL.
Résumé:
UML and MARTE are standardized modeling languages widely used in industry for the design of real-time 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).
Commentaires:
http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7051915
BibTeX
| @inproceedings { | |||
| LBJ14, | |||
| title | = | "{Time properties Verification of UML/MARTE Real-Time Systems}", | |
| author | = | " A. Louati and K. Barkaoui and C. Jerad ", | |
| booktitle | = | "{Proceedings of the 15th {IEEE} International Conference on Information Reuse and Integration, {IRI} 2014}", | |
| year | = | 2014, | |
| edition | = | "IEEE", | |
| month | = | "August", | |
| pages | = | "386-393", | |
| address | = | "Redwood City CA, USA", | |
| note | = | "{http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7051915}", | |
| } | |||
