An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF language
La validation des systèmes critiques réalistes nécessite d'être capable de modéliser et de vérifier formellement des données complexes, du parallélisme asynchrone, et du temps-réel simultanément. Des langages de haut-niveau, comme ceux qui héritent des fondations théoriques des algèbres de proc...
Main Author: | |
---|---|
Language: | ENG |
Published: |
2009
|
Subjects: | |
Online Access: | http://tel.archives-ouvertes.fr/tel-00551724 http://tel.archives-ouvertes.fr/docs/00/55/17/24/PDF/thesis_stoecker.pdf |
id |
ndltd-CCSD-oai-tel.archives-ouvertes.fr-tel-00551724 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-CCSD-oai-tel.archives-ouvertes.fr-tel-005517242013-01-07T17:48:56Z http://tel.archives-ouvertes.fr/tel-00551724 http://tel.archives-ouvertes.fr/docs/00/55/17/24/PDF/thesis_stoecker.pdf An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF language Stöcker, Jan [INFO:INFO_MO] Computer Science/Modeling and Simulation algèbre de processus automate concurrence méthode formelle modèle intermédiaire temps-réel réseau de Petri vérification La validation des systèmes critiques réalistes nécessite d'être capable de modéliser et de vérifier formellement des données complexes, du parallélisme asynchrone, et du temps-réel simultanément. Des langages de haut-niveau, comme ceux qui héritent des fondations théoriques des algèbres de processus, ont une syntaxe concise et une grande expressivité pour représenter ces aspects. Cependant, ils disposent de peu d'outils logiciels permettant d'appliquer des algorithmes efficaces du model-checking. Néanmoins, de tels outils existent pour des modèles graphiques, de niveau plus bas, tels que les automates temporisés (par exemple Uppaal) et les réseaux de Petri temporisés (par exemple Tina). Les modèles intermédiaires sont un moyen pour combler le fossé qui sépare les langages des modèles graphiques. Par exemple, NTIF (New Technology Intermediate Format) a été proposé pour représenter des processus séquentiels non-temporisés qui manipulent des données complexes. Dans cette thèse, nous proposons un nouveau modèle nommé ATLANTIF, qui enrichit NTIF de constructions temps-réel et de compositions parallèles de processus séquentiels. Leur synchronisation est exprimée d'une manière simple et intuitive par la nouvelle notion de synchroniseur. Nous montrons qu'ATLANTIF est capable d'exprimer les constructions principales des langages de haut niveau. Nous présentons aussi des traducteurs d'ATLANTIF vers des automates temporisés (pour la vérification avec Uppaal) et vers des réseaux de Petri temporisés (pour la vérification avec Tina). Ainsi, ATLANTIF étend la classe des systèmes qui peuvent en pratique être vérifiés formellement, ce que nous illustrons par un exemple. 2009-12-09 ENG PhD thesis |
collection |
NDLTD |
language |
ENG |
sources |
NDLTD |
topic |
[INFO:INFO_MO] Computer Science/Modeling and Simulation algèbre de processus automate concurrence méthode formelle modèle intermédiaire temps-réel réseau de Petri vérification |
spellingShingle |
[INFO:INFO_MO] Computer Science/Modeling and Simulation algèbre de processus automate concurrence méthode formelle modèle intermédiaire temps-réel réseau de Petri vérification Stöcker, Jan An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF language |
description |
La validation des systèmes critiques réalistes nécessite d'être capable de modéliser et de vérifier formellement des données complexes, du parallélisme asynchrone, et du temps-réel simultanément. Des langages de haut-niveau, comme ceux qui héritent des fondations théoriques des algèbres de processus, ont une syntaxe concise et une grande expressivité pour représenter ces aspects. Cependant, ils disposent de peu d'outils logiciels permettant d'appliquer des algorithmes efficaces du model-checking. Néanmoins, de tels outils existent pour des modèles graphiques, de niveau plus bas, tels que les automates temporisés (par exemple Uppaal) et les réseaux de Petri temporisés (par exemple Tina). Les modèles intermédiaires sont un moyen pour combler le fossé qui sépare les langages des modèles graphiques. Par exemple, NTIF (New Technology Intermediate Format) a été proposé pour représenter des processus séquentiels non-temporisés qui manipulent des données complexes. Dans cette thèse, nous proposons un nouveau modèle nommé ATLANTIF, qui enrichit NTIF de constructions temps-réel et de compositions parallèles de processus séquentiels. Leur synchronisation est exprimée d'une manière simple et intuitive par la nouvelle notion de synchroniseur. Nous montrons qu'ATLANTIF est capable d'exprimer les constructions principales des langages de haut niveau. Nous présentons aussi des traducteurs d'ATLANTIF vers des automates temporisés (pour la vérification avec Uppaal) et vers des réseaux de Petri temporisés (pour la vérification avec Tina). Ainsi, ATLANTIF étend la classe des systèmes qui peuvent en pratique être vérifiés formellement, ce que nous illustrons par un exemple. |
author |
Stöcker, Jan |
author_facet |
Stöcker, Jan |
author_sort |
Stöcker, Jan |
title |
An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF language |
title_short |
An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF language |
title_full |
An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF language |
title_fullStr |
An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF language |
title_full_unstemmed |
An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF language |
title_sort |
intermediate model for the verification of asynchronous real-time embedded systems: definition and application of the atlantif language |
publishDate |
2009 |
url |
http://tel.archives-ouvertes.fr/tel-00551724 http://tel.archives-ouvertes.fr/docs/00/55/17/24/PDF/thesis_stoecker.pdf |
work_keys_str_mv |
AT stockerjan anintermediatemodelfortheverificationofasynchronousrealtimeembeddedsystemsdefinitionandapplicationoftheatlantiflanguage AT stockerjan intermediatemodelfortheverificationofasynchronousrealtimeembeddedsystemsdefinitionandapplicationoftheatlantiflanguage |
_version_ |
1716397095571685376 |