|
 
|
[LBJ15] Temporal Properties Veri cation of Real-Time Systems Using UML/MARTE/OCL-RT;
Revue Internationale avec comité de lecture : Journal Advances in Intelligence Systems and Computing, Springer Verlag., vol. 346, pp. 133-147, 2015, (doi:2194-5357)Mots clés: UML , OCL , verification, Real-Time , TPN , TCTL
Résumé:
Dependability is a key feature of critical Real-Time Systems (RTS). In fact, errors may lead to disastrous consequences on life beings and economy. To ensure the absence or avoidance of such errors, it is important to focus on RTS verification as early as possible. As MARTE UML profile is the standard de facto for modelling RTS, we suggest to extend UML diagrams by a formal verification stage. More precisely, in the first part we propose a transformation approach of Interaction Overview Diagrams and Timing Diagram merged with UML-MARTE annotations into Time Petri Nets (TPN) models Then, in the second part, we show how we can derive Timed Computational Tree Logic formulae from Ob- ject Constraint Language-Real Time (OCL-RT) constraints. This formal verification is performed by the Romeo model-checker. Finally, we illus- trate our approach through a case study derived from a RT asynchronous system (Integrated Modular Avionics/based airborne system).
Commentaires:
download pdf : http://link.springer.com/chapter/10.1007%2F978-3-319-16577-6_6
Equipe:
sys
BibTeX
| @article { | |||
| LBJ15, | |||
| title | = | "{Temporal Properties Veri cation of Real-Time Systems Using UML/MARTE/OCL-RT; }", | |
| author | = | "A. Louati and K. Barkaoui and C. Jerad", | |
| journal | = | "Advances in Intelligence Systems and Computing, Springer Verlag.", | |
| year | = | 2015, | |
| volume | = | 346, | |
| pages | = | "133-147", | |
| note | = | "{download pdf : http://link.springer.com/chapter/10.1007%2F978-3-319-16577-6_6}", | |
| doi | = | "2194-5357", | |
| } | |||
