Synthèse
Volume 25, Numéro 1, Pages 72-81
2019-04-20
A Process - Oriented Verification And Validation For Real Time Embedded Systems
Authors : Chabbat Nadia . Ghanemi Salim .
Abstract
Based on formal and robust concepts, the real-time embedded systems allow meeting the requirements for the quality of the systems. Considering the UML MARTE profile as the standard by excellence, it has been the most used in the modelling and analysis of systems. In addition, for the support of time constraints, the CCSL language (Clock Constraint Specification Language) has been proposed. However, the MARTE-CCSL profile allows only formal verification, which represents only the static validation. As a complement to the analysis, it is essential to consider the dynamic validation step as well. In this paper, we suggest a hybrid process-oriented verification approach (HV&V) for MARTE-CCSL models. The HV&V approach is based on a transformation of MARTE-CCSL models to Timed CSP (Communicating Sequential Processes) models. Thus, the Timed CSP model and the generated counter-examples will be automatically used by the validation step. This last step helps to quickly generate a prototype that is functional and verifiable at low cost. The approach is tested on the elevator control system.
Keywords
Real Time Embedded Systems (RTES), Timed CSP (Communicating Sequential Processes), Clock Constraint Specification Language (CCSL), MARTE (Modeling and Analysis of Real Time Embedded Systems), V&V (Verification & Validation)
Les articles similaires
Azzaz Mohamad Salah
.
Tanougast@univ-metz.fr Camel
.
Sadoudi Said
.
Dandache Abbas
.
A. Bouridane Ahmed
.
pages 61-65.
Laredj Khaldia
.
Belarbi Mostefa
.
Arab Yassine
.
pages 41-48.
Boutekkouk Fateh
.
pages 56-60.
Benaoun Mouna
.
pages 112-123.
