Expression et validation de contraintes temporelles pour la spécification des systèmes réactifs / David Delfieu ; sous la direction de Abd-El-Kader Sahraoui

Date :

Editeur / Publisher : [Lieu de publication inconnu] : [éditeur inconnu] , [1995]

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Esterel (langage de programmation)

Temps réel (informatique)

GRAFCET

Réseaux de Petri

Sahraoui, Abd-El-Kader (1955-....) (Directeur de thèse / thesis advisor)

Université Toulouse 3 Paul Sabatier (1969-2024) (Organisme de soutenance / degree-grantor)

Collection : Rapport LAAS / Laboratoire d'automatique et d'analyse des systèmes, [puis] Laboratoire d'analyse et d'architecture des systèmes / Toulouse : Laboratoire d'automatique et d'analyse des systèmes du CNRS , 1986-...

Relation : Expression et validation de contraintes temporelles pour la spécification des systèmes réactifs / David Delfieu ; sous la direction de Abd-El-Kader Sahraoui / Grenoble : Atelier national de reproduction des thèses , 1995

Résumé / Abstract : La specification des systemes temps reel pose le probleme de l'expression du temps et des contraintes temporelles pour lesquels nous proposons dans ce memoire, une nouvelle representation. Cette representation est basee sur l'hypothese que l'ecoulement du temps est modelise par l'occurrence d'un evenement specifique. Cette conception nous permet de considerer les contraintes temporelles comme des proprietes de sequences d'evenements observables. En relation avec une notation simple, basee sur la notion de grammaire, les proprietes temporelles deviennent des proprietes syntaxiques. Ces considerations nous ont amenes a proposer une nouvelle methode d'analyse des contraintes temporelles qui a pour objet de verifier que toutes les contraintes temporelles d'un cahier des charges ont bien ete prises en compte dans l'etape de specification. Pour realiser cette verification, on elabore un analyseur de traces temporisees dont la construction se fait en deux etapes. On extrait d'abord les contraintes temporelles en suivant une decomposition structuree. Cette decomposition permet d'identifier un ensemble d'operateurs (periodique, sporadique, de disjonction ou de conjonction) liant les contraintes temporelles. On exprime ensuite ces contraintes, sous la forme de grammaires types. La seconde etape est la recomposition de ces grammaires, par l'ensemble des operateurs precedemment identifies. Pour cela, on a redefini chacun de ces operateurs pour qu'ils puissent s'appliquer sur des grammaires. Le resultat final de cette recomposition produit une grammaire globale qui constitue un analyseur syntaxique, capable de verifier si une trace temporisee verifie ou non, toutes les contraintes temporelles du cahier des charges