A process-oriented verification and validation for real time embedded systems
Other Title(s)
Un processus-vérification et validation orientées pour les systèmes embarqués en temps réel
Joint Authors
Source
Issue
Vol. 25, Issue 1 (30 Jun. 2019), pp.72-81, 10 p.
Publisher
Annaba Badji Mokhtar University
Publication Date
2019-06-30
Country of Publication
Algeria
No. of Pages
10
Main Subjects
Information Technology and Computer Science
Abstract EN
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.
Abstract FRE
Basés sur des notions formelles et robustes, les systèmes temps réel embarqués permettent de répondre aux exigences de qualité des systèmes.
Vu que le profile UML MARTE est le standard par excellence, il a été le plus utilisé dans la modélisation et l’analyse des systèmes.
De plus, pour la prise en charge des contraintes temporelles, le langage CCSL a été proposé.
Cependant, le profile MARTE-CCSL ne permet que la vérification formelle qui représente uniquement une validation statique.
Comme complément à l’analyse l’étape de validation dynamique a été considérée.
Dans cet article une approche de vérification hybride (HV&V) orientée processus pour les modèles MARTE-CCSL est proposée.
L’approche HV&V repose sur une transformation de modèles MARTE-CCSL vers des modèles Timed CSP.
Ainsi, le modèle Timed CSP et les contre-exemples générés seront exploités automatiquement par l’étape de validation.
Cette dernière étape a permis de générer rapidement un prototype fonctionnel et vérifiable avec un faible coût.
L’approche est testée sur un système de contrôles d’un ascenseur.
American Psychological Association (APA)
Shubat, Nadiyah& Ghanimi, Salim. 2019. A process-oriented verification and validation for real time embedded systems. Synthèse،Vol. 25, no. 1, pp.72-81.
https://search.emarefa.net/detail/BIM-890562
Modern Language Association (MLA)
Shubat, Nadiyah& Ghanimi, Salim. A process-oriented verification and validation for real time embedded systems. Synthèse Vol. 25, no. 1 (Jun. 2019), pp.72-81.
https://search.emarefa.net/detail/BIM-890562
American Medical Association (AMA)
Shubat, Nadiyah& Ghanimi, Salim. A process-oriented verification and validation for real time embedded systems. Synthèse. 2019. Vol. 25, no. 1, pp.72-81.
https://search.emarefa.net/detail/BIM-890562
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references : p. 80-81
Record ID
BIM-890562
