OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Contribution à la conception de systèmes temps-réel s'appuyant sur la technique de description formelle RT-LOTOS

Lohr, Christophe. Contribution à la conception de systèmes temps-réel s'appuyant sur la technique de description formelle RT-LOTOS. PhD, Institut National Polytechnique de Toulouse, 2002

[img]
Preview
(Document in French)

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
3MB

Official URL: http://ethesis.inp-toulouse.fr/archive/00000043/

Abstract

Ce mémoire de thèse s'intéresse à la conception de systèmes temps-réel en s'appuyant sur la méthode formelle RT-Lotos, extension temporelle à l'algèbre de processus Lotos. Il aborde plusieurs points relatifs à la spécification, la validation et l'ordonnancement de systèmes concurrents sujets à des contraintes logiques et temporelles. La première partie propose un éventail de méthodes formelles pour la spécification et la validation de systèmes temps-réel. Elle présente également le langage RT-Lotos et la technique de vérification formelle associée basée sur une analyse d'accessibilité. Elle détaille finalement un ensemble de travaux concernant l'automate temporisé (appelé un DTA) dérivé d'une spécification RT-Lotos, avec comme objectifs d'exécuter des simulations rapides, et de s'interfacer avec des outils de vérification de type model-checker. La deuxième partie présente une étude sur la notion de cohérence temporelle et propose une technique ainsi qu'un modèle formel pour exploiter sous un nouvel angle des informations issues de la vérification formelle par analyse d'accessibilité. Cette approche propose de raffiner le graphe des régions, d'en élaguer certaines branches jugées non souhaitables, d'extraire les dates de tir possible des actions, et de présenter ces informations sous la forme d'un nouveau type d'automate temporisé (appelé un TLSA) ayant pour vocation l'ordonnancement dans le temps des actions d'un système. Enfin, la troisième partie se penche sur les liens possibles entre méthodes formelles et semi-formelles. Dans ce cadre, nous proposons une sémantique formelle pour les diagrammes UML s'appuyant sur RT-Lotos, après avoir défini une extension temps-réel à UML appelée TURTLE). Ainsi, nous définissons une méthodologie qui s'inscrit dans les techniques de développement industriel classiques et qui permet une vérification formelle de systèmes temps-réel.

Item Type:PhD Thesis
Uncontrolled Keywords:
Institution: Université de Toulouse > Institut National Polytechnique de Toulouse - INPT
Laboratory name:
Research Director:
Courtiat, Jean-Pierre
Statistics:download
Deposited By: admin admin

Repository Staff Only: item control page