A Process – oriented verification and validation for real time embedded systems

Numéro de la revue: Volume 25 , Numéro 1
Auteurs: Nadia Chabbat & Salim Ghanemi
 Department of Computer Sciences, Badji Mokhtar Annaba University, Po Box 12, Annaba, 23000, Algeria.


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.

Key words

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)