O desenvolvimento de sistemas críticos é atualmente um dos problemas mais desafiadores enfrentados pela Engenharia. Há frequentemente uma pressão para se reduzir o tempo total de desenvolvimento, o que dificulta a entrega de sistemas com um mínimo aceitável de defeitos. Nos últimos anos, houve um aumento no tráfego aéreo, o que demanda uma modernização dos sistemas de tráfego aéreo atuais, muito dependentes na figura do controlador. Sistemas de tráfego aéreo são sistemas considerados críticos em segurança e de tempo real. O objetivo do presente trabalho é estabelecer um método de modelagem e verificação formal para sistemas críticos, com aplicação no domínio de tráfego aéreo. Com a adoção de técnicas de modelagem e verificação formal, pretende-se garantir a corretude dos sistemas frente aos requisitos inicialmente especificados e a detecção de erros em fases mais iniciais do projeto, o que resultaria em menores custos envolvidos na sua correção. São fornecidas diretivas para a aplicação do método através de um estudo de caso, baseado em três módulos de um sistema ATC em baixo nível de abstração, para a validação do funcionamento de módulos de software. Para verificação formal, é utilizada a ferramenta NuSMV e as propriedades a serem verificadas são descritas na lógica computacional de árvore (CTL) para garantir que o sistema satisfaça requisitos dos tipos vivacidade e segurança. / Developing safety critical systems is one of the most challenging problems in Engineering nowadays. There is usually a pressure to reduce the total time of the development, what makes it difficult to deliver systems with an acceptable low level of defects. In the recent years, there has been an increase in air trffic, what demands a modernization in the current air traffic systems, which are very dependent on the human controller. Air traffic systems are considered safety critical and real time systems. The objective of the present work is to establish a modeling and formal verification method for critical systems, applicable to the air traffic domain. By adopting modeling and formal verification techniques, it is expected to ensure the systems\' correctness compared with the initially specified requirements and the error detection in the initial phases of the project. Guidelines are provided for applying the method by means of a case study, based in three modules of and ATC system in a low abstraction level, for the validation of the operation of software modules. For the formal verification, it is used the NuSMV tool and the properties to be checked are described in the computational tree logic (CTL) to ensure that the system satisfies requirements of liveness and safety types.

Security is widely recognized as an important property that is tightly interdependentwith safety in safety-critical systems. The goal of this thesis is to conduct case studies on the implications that security attacks may have on the safety of these systems.In these case studies, we formally model the design of a robot arm system, verify itssecurity against some potential attack scenarios, propose mitigation techniques andanalyze their effectiveness. In order to achieve a thorough knowledge about the current formal verification approaches and select a proper modeling language/tool, weconducted an extensive literature review. We performed this review following a wellknown approach proposed by Barbara Kitchenham. The procedure and outcomes ofthis review are detailed in this thesis. Based on the literature review, we chose TRebeca, (a timed extension of Rebeca), as the formal language to model the robot armsystem, attack scenarios and mitigation techniques. Rebeca is an actor-based modeling language with a Java-like syntax that is effectively used to model concurrent anddistributed systems. This language is supported by a full-featured IDE called Afra,which facilitates the development of (T)Rebeca models and verification of correctnessproperties (such as safety and security) on them. Among several functions providedby a robot arm system, we chose two important functions i.e., Stand Still Supervisionand Control Error Supervision, which we believe would be interesting for attackerstrying to get control over robot movements. In particular, attackers may maliciouslymanipulate the parameter values of these functions, which may lead to safety issues.In order to find suitable attack scenarios on these functions, we studied the mostimportant security protocols used in safety-critical industrial control systems. Weobserved that these systems are vulnerable to several attacks, and man-in-the-middleattack is among the most successful attacks on these systems. Based on this study,we devised two attack scenarios for each function and modeled them with TRebeca.To mitigate these attacks, we proposed a redundancy technique, whose effectivenesswas also assured by Afra.

Ce mémoire de thèse propose une approche pour l'obtention des bornes des performances temporelles d'une Architecture d'Automatisation en Réseau par preuves itératives de propriétés d'atteignabilité sur un modèle formel de l'architecture. Ces propriétés d'atteignabilité sont définies grâce à un automate observateur temporisé et paramétré, dont les gardes de certaines transitions sont fonction d'un paramètre temporel. A chaque itération, les résultats de preuves permettent de déterminer la valeur de ce paramètre pour la prochaine itération ; un algorithme de recherche par dichotomie assure la convergence des itérations. La mise en œuvre de cette approche sur des architectures de taille non triviale a nécessité le développement d'une méthode d'abstraction qui comporte deux étapes : simplification de la structure et modification des modèles formels des composants figurant dans la structure simplifiée, ceci afin de prendre en compte les phénomènes de concurrence entre requêtes émises par différents composants. Ces contributions formelles et méthodologiques ont été validées expérimentalement par le traitement de plusieurs cas de taille et complexité croissantes, basés sur le protocole Modbus TCP/IP.

Il y a un besoin grandissant pour d'autonomie dans des systèmes temps réel complexes tels que les robots ou les satellites. Ceci met en avant un problème non trivial : d'un côté il y a des systèmes complexes - donc difficiles à valider - avec une intervention de l'humain dans la boucle qui se veut minimale, de l'autre nous avons des domaines où il faut que le système ait un comportement sûr fonctionnellement afin d'éviter les coûts financiers et/ou humains d'une perte ou d'une détérioration du système. Ces deux notions mises en vis-à-vis semblent contradictoires. En effet comment être sûr qu'un système autonome avec un pouvoir décisionnel fort, n'aura pas un comportement non nominal qui pourra menacer le bon déroulement de la mission ? Comment être sûr qu'un satellite n'allumera pas ses réacteurs sans avoir protégé ses capteurs fragiles (objectif de la caméra, ...) ? Une réponse partielle à ce type de problèmes pourrait être d'utiliser un planificateur de haut niveau qui ne donnerait que des plans garantis comme sûrs et valides. Toutefois ces planificateurs n'ont pas un modèle complet des actions qu'ils effectuent et de leurs conséquences. En effet, les directives données par ce planificateur sont généralement affinées en sous tâches par un superviseur. Le planificateur n'a donc pas un contrôle complet sur le moyen d'effectuer cette action. Nous présentons ici les travaux effectués afin d'intégrer un système de contrôle d'exécution en ligne dans une architecture hiérarchisée. Nous décrivons ici la nécessité et le rôle d'un tel composant dans ce type d'architecture. Nous introduisons le R2C, notre contrôleur basé sur les hypothèses synchrones, ainsi que l'outil permettant sa génération en exploitant des techniques issues du model-checking symbolique. Enfin nous discutons de la nécessité de prendre en compte les com-posants décisionnels dans le contrôle afin d'interférer le moins possible avec les décisions prises par ceux-ci. Les résultats obtenus durant des expérimentations sur une plate-forme robotique confirment les idées développées au cours de ce travail et permettent d'en tirer les conclusions et perspectives sur la mise en place d'un contrôle pour l'amélioration de la fiabilité globale de tels systèmes.

Cette thèse propose une nouvelle technique de vérification par model-checking de propriétés dynamiques PLTL, exprimées au cours d'un processus de spécification de systèmes réactifs par raffinement. La vérification par model-checking a l'avantage d'être entièrement automatisable, mais elle se heurte au problème de l'explosion combinatoire de l'espace d'états à vérifier. Afin de faire face à ce problème, nous proposons de découper par partition l'espace d'états en un ensemble de modules, et de mener la vérification successivement sur chacun des modules, afin de pouvoir conclure sur le modèle dans son ensemble. Nous prouvons que cette méthode de vérification (appelée vérification modulaire) est valide pour tout une classe de propriétés PLTL, que nous caractérisons par des automates de Büchi. Nous présentons les systèmes d'événements B comme cadre d'application de cette technique. Nous proposons une méthode de découpage en modules guidée par le processus de raffinement B.

Le formalisme AltaRica, développé au LaBRI conjointement avec des industriels, permet d'analyser un même système grâce à plusieurs méthodes différentes (arbres de défaillances, réseaux de Petri, chaînes de Markov) afin d'effectuer des études de sûreté de fonctionnement. Ces méthodes sont outillées par des outils industriels. Cette thèse a eu pour but de développer un outil de vérification formelle basé sur une structure de données symbolique, les diagrammes de décision binaires, qui permet de représenter de manière compacte les systèmes de transitions. Cet outil a été doté d'un langage de spécification très expressif, le mu-calcul de Park, qui est la logique du premier ordre étendue par des points fixes sur les relations. Ce mémoire décrit la logique de spécification employée dans le vérificateur de modèles (Mec 5) que nous avons développé, le formalisme AltaRica et les extensions apportées au langage AltaRica durant cette thèse. Ensuite certains aspects de l'implémentation de Mec 5 sont décrits, comme l'architecture du logiciel et certains composants essentiels dont le module de gestion des diagrammes de décision binaires. Puis, une solution élégante et très générique du problème de la synthèse de contrôleurs est décrite, qui permet de spécifier des objectifs de contrôle arborescents et constitue donc une extension naturelle du cadre proposé par Ramadge et Wonham. Cette méthode ramène le problème de la synthèse de contrôleurs à un problème de calcul de stratégies gagnantes. Enfin, une méthode de calcul des stratégies gagnantes dans un jeu de parité est proposée et il est montré que Mec 5 peut calculer de telles stratégies.

Cette thèse traite du problème de la vérification de systèmes ayant un nombre infini d'états. Ces systèmes peuvent être décrits par plusieurs formalismes tels que des algèbres de processus ou des automates finis munis de structures de données non-bornées (automates à pile, réseaux de Petri ou systèmes à files). Dans une première partie de la thèse nous nous intéressons à la caractérisation de classes de systèmes infinis et de propriétés pour lesquels le problème de vérification est décidable. Nous considérons d'abord la complexité de la vérification du mu-calcul linéaire pour les réseaux de Petri. Ensuite, nous définissons des logiques temporelles qui permettent d'exprimer des propriétés non-régulières comportant des contraintes linéaires sur le nombre d'occurrences d'événements. Ces logiques sont plus expressives que les logiques utilisées dans le domaine. Nous montrons en particulier que le problème de la vérification d'une logique qui est plus expressive que le mu-calcul linéaire est décidable pour des classes de systèmes infinis telles que les automates à pile et les réseaux de Petri. Une deuxième partie de la thèse est consacrée aux systèmes communicant par files d'attente, dont le problème de vérification est en général indécidable. Nous appliquons le principe de l'analyse symbolique à ces systèmes. Nous proposons des structures finies qui permettent de représenter et de manipuler des ensembles infinis de configurations de tels systèmes. Ces structures permettent de calculer l'effet exact d'une exécution répétée de tout circuit dans le graphe de transitions du système. Ainsi, chaque circuit peut être considéré comme une nouvelle "transition" du système. Nous utilisons ce résultat pour accélérer le calcul de l'ensemble des configurations atteignables d'un système afin d'augmenter les chances de terminaison de ce calcul.

Les travaux développés dans cette thèse visent à assister le processus d'ingénierie des exigences temporelles pour les systèmes complexes à contraintes de temps. Nos contributions portent sur trois volets : la spécification des exigences, la modélisation du comportement et la vérification. Pour le volet spécification, une nouvelle classification des exigences temporelles les plus communément utilisées a été proposée. Ensuite, afin de cadrer l'utilisateur durant l'expression des exigences, une grammaire de spécification à base de motifs prédéfinis en langage naturel est développée. Les exigences générées sont syntaxiquement précises et correctes quand elles sont prises individuellement, néanmoins cela ne garantie pas la cohérence de l'ensemble des exigences exprimées. Ainsi, nous avons développé des mécanismes capables de détecter certains types d'incohérences entre les exigences temporelles. Pour le volet modélisation du comportement, nous avons proposé un algorithme de transformation des state-machine avec des annotations temporelles en des automates temporisés. L'idée étant de manipuler une notation assez intuitive et de générer automatiquement des modèles formels qui se prêtent à la vérification. Finalement, pour le volet vérification, nous avons adopté une technique de vérification à base d'observateurs et qui repose sur le model-checking. Concrètement, nous avons élaboré une base de patterns d'observation (ou observateurs) ; chacun des patterns développés est relatif à un type d'exigence temporelle dans la nouvelle classification. Ainsi, la vérification est réduite à une analyse d'accessibilité des états correspondants à la violation de l'exigence associée

L'analyse comportementale traditionnelle opère en général au niveau de l'implantation du comportement malveillant. Pourtant, elle s'intéresse surtout à l'identification d'un comportement donné, indépendamment de sa mise en œuvre technique, et elle se situe donc plus naturellement à un niveau fonctionnel. Dans cette thèse, nous définissons une forme d'analyse comportementale de programmes qui opère non pas sur les interactions élémentaires d'un programme avec le système mais sur la fonction que le programme réalise. Cette fonction est extraite des traces d'un programme, un procédé que nous appelons abstraction. Nous définissons de façon simple, intuitive et formelle les fonctionnalités de base à abstraire et les comportements à détecter, puis nous proposons un mécanisme d'abstraction applicable à un cadre d'analyse statique ou dynamique, avec des algorithmes pratiques à complexité raisonnable, enfin nous décrivons une technique d'analyse comportementale intégrant ce mécanisme d'abstraction. Notre méthode est particulièrement adaptée à l'analyse des programmes dans des langages de haut niveau ou dont le code source est connu, pour lesquels l'analyse statique est facilitée : les programmes conçus pour des machines virtuelles comme Java ou .NET, les scripts Web, les extensions de navigateurs, les composants off-the-shelf. Le formalisme d'analyse comportementale par abstraction que nous proposons repose sur la théorie de la réécriture de mots et de termes, les langages réguliers de mots et de termes et le model checking. Il permet d'identifier efficacement des fonctionnalités dans des traces et ainsi d'obtenir une représentation des traces à un niveau fonctionnel ; il définit les fonctionnalités et les comportements de façon naturelle, à l'aide de formules de logique temporelle, ce qui garantit leur simplicité et leur flexibilité et permet l'utilisation de techniques de model checking pour la détection de ces comportements ; il opère sur un ensemble quelconque de traces d'exécution ; il prend en compte le flux de données dans les traces d'exécution ; et il permet, sans perte d'efficacité, de tenir compte de l'incertitude dans l'identification des fonctionnalités. Nous validons nos résultats par un ensemble d'expériences, menées sur des codes malicieux existants, dont les traces sont obtenues soit par instrumentation binaire dynamique, soit par analyse statique.

Dans le cadre de son offre de serveurs haut de gamme, la société Bull conçoit des multiprocesseurs à mémoire distribuée partagée avec un protocole de cohérence de cache CC-DSM (Cache-Coherent Distibuted Shared Memory), et fournit une implémentation de la bibliothèque MPI (Message Passing Interface) pour la programmation parallèle. L'évaluation des performances de cette implémentation permettra, d'une part, de faire les bons choix d'architecture matérielle et de la couche logicielle au moment de la conception et, d'autre part, fournira des éléments d'analyse nécessaires pour comprendre les mesures faites au moment de la validation de la machine réelle. Nous proposons et mettons en œuvre dans ce travail de thèse une méthodologie permettant d'évaluer les performances des algorithmes de la bibliothèque MPI (ping-pong et barrières) en tenant compte de l'architecture matérielle. Cette approche est basée sur l'utilisation des méthodes formelles, elle consiste en 3 étapes principales : 1) la modélisation en langage LOTOS des aspects matériels (topologie d'interconnexion et protocole de cohérence de cache) et logiciels (algorithmes MPI) ; 2) la vérification formelle de la correction fonctionnelle du modèle obtenu ; 3) l'évaluation des performances après l'extension du modèle par des informations quantitatives (latences des transferts des données) en utilisant des méthodes numériques et de la simulation.