thesis

Description et verification d'architectures d'application temps reel : clara et les reseaux de petri temporels

Defense date:

Jan. 1, 1998

Edit

Institution:

Nantes

Disciplines:

Directors:

Abstract EN:

Pas de résumé disponible.

Abstract FR:

Concevoir des applications temps reel est une activite reconnue comme difficile, du fait des differentes exigences fonctionnelles dont elles font etat, associees a de multiples contraintes non fonctionnelles. De plus la predictibilite qui caracterise les systemes temps reel critiques exige une garantie a priori du respect de ces diverses contraintes. Le concepteur doit donc etre assiste dans sa tache. Notre outil react (real time application configuration tool) est un outil d'aide a la conception d'application temps reel, predictible en terme d'ordonnancabilite. Il se situe dans le cycle de developpement, en phase de conception preliminaire voire detaillee. Il permet la definition et la construction d'une architecture operationnelle validee vis-a-vis des contraintes temporelles d'execution auxquelles l'application est assujettie. Cette these est une contribution au developpement de react. Elle a pour objectifs d'une part de proposer un langage de configuration appele clara (configuration language for real time application), et d'autre part, de soumettre une approche utilisant les reseaux de petri temporels en vue de la verification. Dans le cadre de ce memoire, clara fournit les abstractions necessaires a la modelisation de l'architecture d'une application dans son aspect logiciel. Differents objets et regles de connexion ont ete ainsi definis. Il offre une syntaxe graphique et textuelle, et s'est inspire de quelques langages de configuration existants. Toutefois, et c'est le caractere original de clara vis-a-vis de ces derniers, il permet la prise en compte des interactions de controle de type synchronisations et activations au sein de la description architecturale ainsi que des contraintes temporelles. L'expression de ces dernieres a consiste a definir de facon qualitative et quantitative les exigences temporelles portant sur des evenements disponibles au niveau de l'architecture logicielle prealablement definie. Valider l'architecture operationnelle decrite en clara consiste a verifier le respect des contraintes temporelles sur son comportement global, comportement decrit en reseaux de petri temporels. Sous quelques hypotheses, la construction du graphe des classes permet de valider ou non l'architecture operationnelle.