Meliouh, Amel (2021) UML et Model-Checking pour la Modélisation et la Vérification des Systèmes Embarqués. Doctoral thesis, Université de mohamed kheider biskra.
![[img]](http://thesis.univ-biskra.dz/style/images/fileicons/text.png) |
Text
these meliouh vers finale.pdf Download (3MB) |
Abstract
Ce travail présente une approche formelle de modélisation et de vérification des systèmes embarqués. L’approche repose sur une modélisation du comportement temporel du système et une génération automatique de code. Le concept clé est l'utilisation combinée d'un ensemble de diagrammes comportementaux d’UML étendu par des annotations temporelles (diagrammes Statechart temps réel et de collaboration temps réel) pour la modélisation du système et le langage Maude pour la vérification. Tout d'abord, un outil de modélisation UML est développé, ensuite, une grammaire de graphes est exécutée pour générer automatiquement des spécifications en Maude équivalentes. L'approche repose sur la génération de code, donc il est possible d'utiliser un outil de vérification de modèles (Model-cheking) pour vérifier certaines propriétés temporelles représentées dans la logique temporelle temps réel (MITL).
| Item Type: | Thesis (Doctoral) |
|---|---|
| Uncontrolled Keywords: | UML, Real-Time Statechart diagram, Real-Time Collaboration diagram, génération de code, Méta-modélisation, Grammaire de graphes, ATOM3, MITL, Model checking, language Maude. |
| Subjects: | Q Science > Q Science (General) |
| Divisions: | Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie > Département d'informatique |
| Depositing User: | BFSE |
| Date Deposited: | 07 Apr 2021 10:40 |
| Last Modified: | 07 Apr 2021 10:40 |
| URI: | http://thesis.univ-biskra.dz/id/eprint/5366 |
Actions (login required)
 |
View Item |
