Author/Authors
chabbat, nadia badji mokhtar annaba university - department of computer sciences, Annaba, Algeria , ghanemi, salim badji mokhtar annaba university - department of computer sciences, Annaba, Algeria
Title Of Article
A process - oriented verification and validation for real time embedded systems
شماره ركورد
42788
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.
From Page
72
NaturalLanguageKeyword
Real Time Embedded Systems (RTES) , Timed CSP (Communicating Sequential Processes) , Clock ConstraintSpecification Language(CCSL) , MARTE (Modelingand Analysis of Real TimeEmbedded Systems) , V V(Verification Validation)
JournalTitle
Revue Des Sciences Et De La Technologie, Synthèse
To Page
81
JournalTitle
Revue Des Sciences Et De La Technologie, Synthèse
Link To Document