A process - oriented verification and validation for real time embedded systems

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 processoriented 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 counterexamples 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)