Please use this identifier to cite or link to this item: http://hdl.handle.net/1822/18592

TitleInfluence de la prise en compte dun modèle du processus en vérification formelle des Systèmes à Evénements Discrets
Author(s)Machado, José Mendes
Advisor(s)Silva, Jaime F. da
Lesage, Jean-Jacques
Issue date30-Jun-2006
Abstract(s)Ce travail est une thèse en co-tutelle encadrée par une convention de co-tutelle signée entre l'Université du Minho (UM) et l’École Normale Supérieure de Cachan (ENS). Le Département de Génie Mécanique (DEM) de l’UM et le Laboratoire Universitaire de Recherche en Production Automatisée (LURPA) de l'ENS de Cachan sont les principaux acteurs de cette coopération matérialisé par ce travail de thèse de l’auteur. Le travail de thèse a été élaboré dans les deux institutions et a été devélopé dans le domaine de la Sûreté de Fonctionnement de systèmes automatisés. La Sûreté de Fonctionnement (SdF) fait aujourd’hui irruption dans le cahier des charges d’un nombre de systèmes automatisés beaucoup plus important que par le passé. Assurer la sûreté d’un système nécessite une approche globale (pour ne pas laisser de maillon faible) qui porte sur l’ensemble des activités d’ingénierie puis d’exploitation du système. Dans le domaine des Systèmes à Evénements Discrets (SED), parmi les récentes contributions scientifiques majeures à l’amélioration de la SdF des systèmes automatisés on peut citer : la synthèse de contrôleurs sûrs grâce à la théorie de supervision, le diagnostic qui consiste à identifier des comportements fautifs et la vérification formelle de contrôleurs qui prouve la véracité de propriétés attendues. Nous avons pour notre part considéré un SED comme étant composé d’un contrôleur et d’un processus en boucle fermée, tous deux aux comportements asynchrones, synchronisés lors des échanges d’informations (cadencés par les phases de lecture des entrées et d’affectation des sorties du contrôleur). L'objectif principal de cette thèse est d’évaluer les apports, les limites et les complémentarités de la vérification du comportement d’un contrôleur logique par model-checking en prenant en compte, ou non, un modèle du processus commandé. Pour la modélisation nous proposons une classe d’automates non déterministes, communiquant par partage de variables logiques et aux transitions labellées par des expressions booléennes. Le modèle du processus est alors obtenu par coordination des comportements de modules élémentaires, grâce à un séquenceur qui permet une évolution asynchrone des modules jusqu’à atteindre une situation stable du modèle. La vérification formelle d’un ensemble représentatif de propriétés est traitée sur un système automatisé servant d’exemple support. Nous généralisons ces résultats et présentons une approche mixant la vérification formelle avec et sans modèle de processus. Cette approche est basée sur une double typologie des propriétés et des variables utilisées pour les exprimer. On distingue d’une part les propriétés de vivacité des propriétés de sûreté, et d’autre part les propriétés exprimées à partir de variables contrôlables ou non. Cette approche couplée propose un cadre de vérification plus rigoureux et plus sûr que celui de l’utilisation la plus souvent pratiquée, sans aucun modèle de processus.
Este trabalho consiste na realização de uma tese em co-tutela, enquadrada por uma convenção de co-tutela celebrada entre a Universidade do Minho (UM) e a École Normale Supérieure (ENS) de Cachan. O Departamento de Engenharia Mecânica da UM e o Laboratoire Universitaire de Recherche en Production Automatisé da ENS de Cachan são os principais actores desta colaboração materializada por esta tese de doutoramento do autor. O trabalho de tese foi elaborado nas duas instituições e foi desenvolvido no domínio da Segurança de Funcionamento de sistemas automatizados. A Segurança de Funcionamento (SdF) aparece, nos dias de hoje, tratada nos cadernos de encargos de cada vez mais sistemas automatizados de uma forma mais importante do que no passado. Garantir a segurança de um sistema implica uma abordagem global (para que nenhum aspecto seja descurado) que considera as várias vertentes da actividade de engenharia e posteriormente sobre a colocação em funcionamento e exploração do sistema automatizado. No domínio dos Sistemas a Eventos Discretos (SED), de entre as várias contribuições científicas de maior relevo para a melhoria da SdF de sistemas automatizados, pode-se citar: a síntese de controladores seguros a partir da aplicação da teoria da supervisão, o diagnóstico que consiste em identificar os comportamentos de falha e a verificação formal de controladores que prova a veracidade de certas propriedades comportamentais esperadas. Neste caso específico, foi considerado um SED como sendo composto por um controlador e um processo em malha fechada, cada um deles com comportamentos assíncronos, sendo sincronizados através da troca de informações entre eles (cuja cadência é caracterizada pelas fases de leitura das entradas e afectação das saídas do controlador). O objectivo principal desta tese é de avaliar as vantagens, os limites e a complementaridade na verificação formal de um controlador lógico, por model-checking, considerando, ou não, um modelo do processo comandado. Para a modelização propõe-se uma classe de autómatos não determinísticos, que comunicam por partilha de variáveis lógicas e com transições «labelizadas» por expressões booleanas. O modelo do processo é obtido pela coordenação dos comportamentos de módulos elementares graças a um sequenciador que permite uma evolução assíncrona dos módulos até que se atinja uma situação estável do modelo. A verificação formal de um exemplo representativo de propriedades é tratado num sistema automatizado que serve de exemplo suporte. Generaliza-se os resultados obtidos e apresenta-se uma abordagem onde é misturada a verificação formal com e sem modelo do processo. Esta abordagem é baseada numa dupla tipologia das propriedades e das variáveis utilizadas para as exprimir. Distingue-se, por um lado, as propriedades de vivacidade e de segurança e, por outro, as propriedades exprimidas a partir de variáveis controláveis ou não. Esta abordagem «mista» propõe um quadro de verificação formal mais rigoroso e mais seguro do que é usualmente praticado sem a utilização de qualquer modelo do processo.
TypeDoctoral thesis
DescriptionTese de doutoramento em Engenharia Mecânica (ramo de conhecimento em Eletrónica, Electrotecnia e Automação)
URIhttp://hdl.handle.net/1822/18592
AccessOpen access
Appears in Collections:BUM - Teses de Doutoramento
DEM - Teses de Doutoramento / PhD Thesis

Files in This Item:
File Description SizeFormat 
THESE_JM TOTAL FINAL CD.pdf3,48 MBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID