Spécifications formelles de systèmes de commande à événements discrets

Dans cette thèse, nous proposons une méthodologie "multi-formalisme" pour spécifier et valider des systèmes à événements discrets. Nous spécifions ces systèmes, à l'aide d'un langage déclaratif de haut niveau, basé sur un formalisme appelé DECM. Ce langage utilise des concepts proches du langage naturel, basés sur le concept d'événement. On peut décrire le processus concerné, sous la forme d'une séquence d'actions à effectuer tout le long d'un cycle de fonctionnement normal. Enfin, nous proposons une méthodologie de validation par simulation. Dans cette méthodologie, les spe cifications de haut niveau d'un système sont transformées dans un formalisme de plus bas niveau, DEVS, qui permet d'exprimer des modèles directement simulables. Nous avons développé pour cela un logiciel de transformation DECM-DEVS, qui permet d'obtenir automatiquement ces modèles simulables, décrits dans un langage formel adéquat et utilisables par un simulateur développé dans le laboratoire d'accueil LSIS. Nous montrons comment une simulation "incrémentale" permet de valider les spécifications initiales, en partant de modèles atomiques et en construisant des modèles simulables de plus en plus complexes pour obtenir finalement le modèle du système complet. Nous utilisons pour cela la technique de couplage, qui permet une construction modulaire et hiérarchique de modèles. Nous avons effectué quelques expérimentations sur des modèles complexes. Celles-ci nous permettent de détecter des erreurs de spécification, de révéler la nécessité d'affiner les spécifications de haut niveau, notamment au sujet des délais temporels, et de constater que des spécifications correctes sont suffisamment robustes.AIX-MARSEILLE1-BU Sci.St Charles (130552104) / SudocSudocFranceF