Добірка наукової літератури з теми "Systèmes, Conception de – Méthodes formelles (informatique)"

La modélisation du contenu des puces pour systèmes embarqués s'avère de plus en plus difficile puisque le développement des outils et des méthodologies de modélisation n'a pas su accompagner l'explosion de la complexité des systèmes. Les méthodes formelles ont su démontrer dans les dernières années leurs capacités de prévention et de détection d'erreurs, ainsi que leurs avantages dans l'expression univoque de demandes et dans la spécification de systèmes. Malgré cela, leur utilisation reste toujours restreinte en raison d'un manque de liens avec les méthodes existantes et la difficulté de leur utilisation. Dans ce document, on essaye de montrer dans quelle mesure la conception de systèmes embarqués peut profiter de l'utilisation de méthodes formelles. Pour cela, plusieurs exemples sont présentés qui démontrent comment l'utilisation des méthodes formelles peut être intégrée dans la conception conjointe tout en cachant - du moins en partie - leur complexité inhérente.

Les systèmes embarqués critiques doivent être soumis à une validation rigoureuse afin d'assurer leurs performances et leur sûreté de fonctionnement. Le test de conformité est l'activité permettant de s'assurer que le produit final correspond aux attentes de la spécification. Dans le cas des systèmes temps-réel, il est important de tester la conformité en prenant en considération les contraintes temporelles du modèle. Cette thèse propose une approche de génération de tests pour des systèmes d'automates temporisés paramétrés. L'algorithme de construction des tests utilise un objectif de test pour sélectionner les comportements à tester. Les tests sont construits grâce à une analyse d'accessibilité symbolique des états du modèle, et une représentation des contraintes d'horloges par une extension paramétrée des diagrammes différentiels d'horloges Clock difference diagrams. Au cours de ce travail, nous avons développé un outil de génération de tests : RTT (Real Time Test Generator).

Afin d’améliorer la vérification de systèmes synchrones synthétisables, une méthode de vérification par model-checking basée sur une procédure de raffinement d’abstraction s’appuyant sur la structure en composants du système est proposée. Ayant opté pour la génération d'abstraction à partir des propriétés vérifiées des composants, différentes méthodes de sélection de propriétés pour l'abstraction initiale et les stratégies de raffinement pour améliorer le modèle abstrait sont présentées et analysées. La stratégie la plus directe est la technique de la Négation du Contre-exemple qui raffine le modèle abstrait en éliminant uniquement le contre-exemple fourni par le model-checker. La technique de la sélection de propriété est une autre stratégie où les propriétés disponibles sont organisées en fonction de leur pertinence par rapport à la propriété globale en exploitant les graphes de dépendances de ses variables. De plus, la phase de raffinement est assistée par un mécanisme de filtrage qui assure l’élimination du contre-exemple. Une technique complète basée sur le FSM a également été proposée pour résoudre les principaux problèmes dans l'abstraction dérivée des propriétés, notamment le manque de propriétés exploitables et la génération d’une bonne abstraction. Les techniques proposées ont été testées sur une plate-forme expérimentale d'un protocole industriel, le bus CAN. Les résultats expérimentaux montrent l'applicabilité des techniques proposées, les gains par rapport aux techniques traditionnelles et l’efficacité relative des trois stratégies proposées varient selon le contexte d’utilisation
In the aim of improving the verification of synthesizable synchronous systems, a model-checking method based on the abstraction-refinement procedure which relies on the compositional structure of the system is proposed. Having opted for the abstraction generation from verified component properties, different methods of property selection for the initial abstraction and the refinement strategies to improve the abstract model are presented and analyzed. The most straight-forward strategy is the Negation of the Counterexample Technique which refines the abstract model by eliminating exclusively the spurious counterexample provided by the model checker. The Property Selection Technique is another abstraction-refinement strategy where the available properties are ordered according to their relevance towards the global property by exploiting the dependency graphs of its variables. Furthermore, the refinement phase is assisted by a filtering mechanism that ensures the current counterexample will be eliminated. A comprehensive FSM-based technique has also been proposed to address the main problems in property based abstraction in compositional verification notably the lack of exploitable properties and the generation of a good abstraction. The techniques proposed have been tested on an experimental platform of an industrial protocol, the Controller Area Network (CAN). The experimental results demonstrate the applicability of the techniques proposed, the gains in comparison to conventional techniques and the relative effectiveness of the three strategies proposed varies according to the application context

Cette thèse propose des méthodes assistant la modélisation et l'évaluation qualitative de l'architecture de sûreté de fonctionnement des systèmes embarqués complexes. Ces architectures sont souvent construites à partir de motifs généraux d'architectures de systèmes correspondant à des mécanismes de sûreté récurrents comme des redondances, des détections, etc. En s'inspirant des principes des "patrons de conception" développés en génie logiciel, nous avons proposé une modélisation de ces mécanismes et des attributs permettant leur réutilisation lors des analyses de sûreté de fonctionnement. Ces analyses nécessitent de raisonner sur le comportement des systèmes en présence de pannes qui peut être modélisé à l'aide de langages formels comme AltaRica. Dans notre cas, les motifs correspondent à des abstractions d'architectures concrètes et donc requièrent une modélisation plus déclarative. Les propriétés étudiées étant en général dynamiques, nous avons choisi d'utiliser une logique temporelle pour les exprimer. Les motifs sont donc constitués d'une partie AltaRica et d'une partie propriétés. Ce type de modélisation mixte possède plusieurs intérêts, notamment lors de la conception en phase amont d'architectures de systèmes où il est possible de manipuler à la fois des parties d'un système conçues de manière détaillée et des spécifications. Elle a également pour buts de faciliter l'allocation d'exigences pour la validation d'architectures ainsi que le prototypage. Nous avons donc défini une notation mixant ces aspects opérationnels et déclaratifs.

Les travaux s'inscrivent dans le cadre d'une ingénierie système afin de faciliter, au plus tôt, une représentation commune et consensuelle des services attendus d'un système automatisé par les différents acteurs du procédé d'automatisation. Ils ont pour objet de proposer, notamment dans la phase initiale de spécification, une méthode formelle vérifiant le prédicat d'automatisation : Spécifications des processus de commande ^ Spécifications des processus opérants => Spécifications des objectifs "système". De manière complémentaires aux travaux développés en Automatique, dans le cadre de la théorie de la Supervision, pour lesquels les objectifs du système à automatiser et les comportements des processus opérants sont parfaitement connus et modélisés, notre approche se caractérise par un processus incrémental de spécification, basé sur le langage B, permettant aux acteurs d'un processus d'automatisation d'aboutir progressivement à une vision commune et cohérente du système automatisé
Presented works refers to system engineering in order to facilitate, as soon as possible, a common and consensual representation of services expected from an automated system by the various actors involved in an automation life cycle. Objective is to propose, especially in the initial phase of specification, a formal method that helps in verifying the following predicate : Control specifications ^ Process spécifications => Specifications of system goals. In a complementary way to the works in Automatic control, within the framework of the Supervisory Control theory, for which the system objectives and the process behaviors are perfectly known and modeled, our approach is characterized by a formal abstract representation, based on the B language, that offers a common and consistent vision of the various engineering processes (automation engineering, mechanical engineering, ) and that should be more or less refined before the use of skill-oriented representations

Ce travail de thèse porte sur l'élaboration de modèles de haut-niveau de systèmes pluridisciplinaires à base d'électronique. L'objectif est de réaliser des prototypes virtuels de ces systèmes et de vérifier formellement leur comportement dès les premières étapes du cycle de conception. Grâce à une approche descendante et au formalisme HiLeS, nous réalisons des représentations hiérarchiques qui associent des réseaux de Petri à un ensemble de blocs et de canaux interagissant mutuellement. Nous avons développé l'outil HiLeS Desiner pour rendre utilisable le formalisme avec plusieurs améliorations opérationnelles telles que le couplage avec un outil d'analyse de réseaux de Petri (TINA) et la compatibilité avec VHDL-AMS. Nous proposons donc, une plate-forme de conception amont autour de l'outil HiLeS Designer avec des passerelles vers TINA et VHDL-AMS. L'utilisation de cette plate-forme nous a permis d'identifier plusieurs perspectives de développement, notamment vers la conduite de projet.

La reconnaissance d'activités est un domaine de recherche qui vise à décrire, analyser, reconnaître, comprendre et suivre les activités et les mouvements de personnes, d'animaux, ou d'objets animés. De nombreux domaines d'applications, importants et critiques, tels que la surveillance, la sécurité ou la santé, nécessitent une certaine forme de reconnaissance d'activités (humaines). Dans ces domaines, la reconnaissance d'activités peut être utile pour détecter tôt les comportements anormaux de certaines personnes : actes de vandalisme ou difficultés dues à l'âge ou la maladie. Les systèmes de reconnaissance doivent être temps réel, réactifs, corrects, complets et fiables. Ces exigences strictes nous amènent à l'utilisation de méthodes formelles pour décrire, analyser, vérifier et générer des systèmes de reconnaissance efficaces et corrects. L'objectif de cette thèse est de contribuer à la définition d'un tel système en se focalisant sur les aspects de description et de vérification. Parmi les nombreuses approches envisageables, nous proposons d'étudier comment le paradigme synchrone peut s'appliquer aux besoins de la reconnaissance d'activités. En effet, cette approche possède des atouts qui semblent intéressants : une sémantique bien fondée, l'assurance du déterminisme, une composition parallèle sûre, et la possibilité de vérification grâce au model checking. Les langages synchrones existants peuvent être utilisés pour décrire des modèles d'activités, mais ils sont difficiles à maîtriser par des non informaticiens (ex : médecins). Nous proposons donc un nouveau langage dédié à ce type d'utilisateurs pour décrire les activités qu'ils souhaitent reconnaitre. Ce langage nommé ADeL (Activity Description Language) propose deux formats équivalents, l'un textuel et l'autre graphique. Afin de permettre à la fois les vérifications et l'implémentation, nous munissons notre langage de deux sémantiques synchrones complémentaires. D'abord, une sémantique comportementale qui donne une définition référentielle du comportement d'un programme en utilisant des règles de réécriture. Deuxièmement, une sémantique opérationnelle qui décrit le comportement d'une manière constructive et peut être directement mise en œuvre. Comme l'environnement des systèmes de reconnaissance n'est généralement pas conforme aux hypothèses du paradigme synchrone, notre système doit comporter un transformateur asynchrone/synchrone. Ce transformateur, que nous appelons "synchroniseur", reçoit les évènements asynchrones de l'environnement, les filtre, décide lesquels peuvent être considérés comme "simultanés", et les regroupe en instants logiques selon des politiques prédéfinies pour les envoyer au moteur de reconnaissance d'activités
The research area of activity recognition aims at describing, analyzing, recognizing, understanding and following the activities and movements of persons, animals, or animated objects. Numerous important and critical application domains, such as surveillance or health-care, require a certain form of recognition of (human) activities. In these domains, activity recognition can be useful for the early detection of abnormal behavior of people, such as vandalism, troubles due to age, or illness. Recognition systems must be real-time, reactive, correct, complete, and reliable. These stringent requirements led us to use formal methods to describe, analyze, verify, and generate effective and correct recognition systems. This thesis aims at contributing to define such a system while focusing on description and verification issues. Among many possible approaches, we propose to study how the synchronous paradigm can cope with the requirements of activity recognition. Indeed, this approach has several major assets such as well founded semantics, assurance of determinism, safe parallel composition, and possibility of verification owing to model checking. Existing synchronous languages can be used to describe models of activities, but they are difficult to master by non specialists (e.g., doctors). Therefore, we propose a new language to allow this kind of users to describe the activities that they wish to recognize. This language, named ADeL (Activity Description Language), proposes two input formats, the first textual, the other graphic. In order to make both verification and implementation possible, we supply this language with two synchronous and complementary semantics. First, a behavioral semantics gives a reference definition of program behavior using rewriting rules. Second, an operational semantics describes the behavior in a constructive way and can be directly implemented. The environment of recognition systems does not usually comply with the hypotheses of the synchronous paradigm. Hence, we propose an asynchronous/synchronous adapter. This adapter, that we call "synchronizer", receives the asynchronous events from the environment, filters them, decides on which ones can be considered as "simultaneous", groups them in logical instants according to predefined politics, and send them to the activity recognition engine

Ce mémoire de thèse s'intéresse à la conception de systèmes temps-réel en s'appuyant sur la méthode formelle RT-Lotos, extension temporelle à l'algèbre de processus Lotos. Il aborde plusieurs points relatifs à la spécification, la validation et l'ordonnancement de systèmes concurrents sujets à des contraintes logiques et temporelles. La première partie propose un éventail de méthodes formelles pour la spécification et la validation de systèmes temps-réel. Elle présente également le langage RT-Lotos et la technique de vérification formelle associée basée sur une analyse d'accessibilité. Elle détaille finalement un ensemble de travaux concernant l'automate temporisé (appelé un DTA) dérivé d'une spécification RT-Lotos, avec comme objectifs d'exécuter des simulations rapides, et de s'interfacer avec des outils de vérification de type model-checker. La deuxième partie présente une étude sur la notion de cohérence temporelle et propose une technique ainsi qu'un modèle formel pour exploiter sous un nouvel angle des informations issues de la vérification formelle par analyse d'accessibilité. Cette approche propose de raffiner le graphe des régions, d'en élaguer certaines branches jugées non souhaitables, d'extraire les dates de tir possible des actions, et de présenter ces informations sous la forme d'un nouveau type d'automate temporisé (appelé un TLSA) ayant pour vocation l'ordonnancement dans le temps des actions d'un système. Enfin, la troisième partie se penche sur les liens possibles entre méthodes formelles et semi-formelles. Dans ce cadre, nous proposons une sémantique formelle pour les diagrammes UML s'appuyant sur RT-Lotos, après avoir défini une extension temps-réel à UML (appelée TURTLE). Ainsi, nous définissons une méthodologie qui s'inscrit dans les techniques de développement industriel classiques et qui permet une vérification formelle de systèmes temps-réel.

Dans le cadre de la modélisation de systèmes complexes, la conception d'entrée ou appelée système représente le plus haut niveau d'abstraction du système global, ceci avant tout choix en terme d'implantation et de technologies. À ce tout premier stade de la conception, l'utilisation d'un langage formel de spécification est de plus en plus considéré comme le fondement d'un réel processus de validation en particulier dans le cas d'exigences de sûreté. Cette thèse met en lumière la nécessité d'une modélisation par raffinement: de la spécfication la plus abstraite vers un point de description proche de l'implémentation afin d'assurer (1) la traçabilité des besoins et des exigences, (2) une meilleure gestion du développement et (3) surtout une conception sûre des systèmes car générée par construction prouvée et ceci que ces sytèmes fassent appel à des technologies logicielles, numériques ou analogiques, voire autres. Le travail qui a été mené a consisté à mettre en perspective la taxinomie des langages ADL, le modèle de développement utilisé dans le cadre des composants électroniques et la méthode par raffinement, dite Méthode B. Ceci nous a permis de réaliser la plateforme BHDL Tool : plateforme de conception de circuits électroniques intégrant (1) une interface de description structurelle de composants électroniques, (2) un générateur de code VHDL et enfin (3) un traducteur en un langage formel pour les preuves de raffinement sous l'Atelier B.

Les “smart-devices” tels les smartphones, tablettes et même les montres ont été largement démocratisés au cours de la dernière décennie. Dans nos sociétés occidentales, on ne garde plus seulement son ordinateur personnel chez soi, on le transporte dans la poche arrière de son pantalon ou bien autour de son poignet. Ces outils ne sont d’ailleurs plus limités, en termes d’utilisation, à de la simple communication par SMS ou bien téléphone, on se fie à eux pour stocker nos photos et données personnelles, ces dernières parfois aussi critiques que des données de paiement bancaires, on gère nos contacts et finances, se connecte à notre boite mail ou un site marchand depuis eux. . . Des exemples récents nous fournissent d’ailleurs un aperçu des tâches de plus en plus complexes que l’on confie à ces outils : l’Estonie autorise l’utilisation de smartphones pour participer aux scrutins nationaux et en 2017, la société Transport for London a lancé sa propre application autorisant l’émulation d’une Oyster card et son rechargement pour emprunter son réseau de transports publics. Plus les services se complexifient, plus la confiance qui leur est accordée par les groupes industriels et les utilisateurs grandit. Nous nous intéressons ici aux protocoles cryptographiques qui définissent les échanges entre les outils et entités qui interviennent dans l’utilisation de tels services et aux garanties qu’ils proposent en termes de sécurité (authentification mutuelle des agent, intégrité des messages circulant, secret d’une valeur critique…). Moult exemples de la littérature et de la vie courante ont démontré que leur élaboration était hautement vulnérable à des erreurs de design. Heureusement, des années de recherches nous ont fournis des outils pour rendre cette tâche plus fiable, les méthodes formelles font partie de ceux-là. Il est possible de modeler un protocole cryptographique comme un processus abstrait qui manipule des données et primitives cryptographiques elles aussi modélisées comme des termes et fonctions abstraites. On met le protocole à l’épreuve face à un attaquant actif et on peut spécifier mathématiquement les propriétés de sécurité qu’il est censé garantir. Ces preuves de sécurité peuvent être automatisées grâce à des outils tels que ProVerif ou bien Tamarin. L’une des grandes difficultés lorsque l’on cherche à concevoir et prouver formellement la sécurité d’un protocole de niveau industriel réside dans le fait que ce genre de protocole est généralement très long et doit satisfaire des propriétés de sécurité plus complexes que certains protocoles universitaires. Au cours de cette thèse, nous avons souhaité étudier deux cas d’usage : le vote électronique et le paiement mobile. Dans les deux cas, nous avons conçu et prouvé la sécurité d’un protocole répondant aux problématiques spécifiques à chacun des cas d’usage. Dans le cadre du vote électronique, nous proposons le protocole Belenios VS, une variante de Belenios RF. Nous définissons l’écosystème dans lequel le protocole est exécuté et prouvons sa sécurité grâce à ProVerif. Belenios VS garantit la confidentialité du vote et le fait qu’un utilisateur puisse vérifier que son vote a bien fait parti du résultat final de l’élection, tout cela même si l’outil utilisé par le votant est sous le contrôle d’un attaquant. Dans le cadre du paiement, nous avons proposé la première spécification ouverte de bout en bout d’une application de paiement mobile. Sa conception a pris en compte le fait qu’elle devait pouvoir s’adapter à l’écosystème de paiement déjà existant pour être largement déployable et que les coûts de gestion, de développement et de maintenance de la sécurité devait être optimisés
The last decade has seen the massive democratization of smart devices such as phones, tablets, even watches. In the wealthiest societies of the world, not only do people have their personal computer at home, they now carry one in their pocket or around their wrist on a day to day basis. And those devices are no more used simply for communication through messaging or phone calls, they are now used to store personal photos or critical payment data, manage contacts and finances, connect to an e-mail box or a merchant website... Recent examples call for more complex tasks we ask to such devices: Estonia voting policy allows the use of smart ID cards and smartphones to participate to national elections. In 2017, Transport for London launched the TfL Oyster app to allow tube users to top up and manage their Oyster card from their smartphone. As services grow with more complexity, so do the trust users and businesses put in them. We focus our interest into cryptographic protocols which define the exchanges between devices and entities so that such interaction ensure some security guarantees such as authentication, integrity of messages, secrecy… Their design is known to be an error prone task. Thankfully, years of research gave us some tools to improve the design of security protocols, among them are the formal methods: we can model a cryptographic protocol as an abstract process that manipulates data and cryptographic function, also modeled as abstract terms and functions. The protocol is tested against an active adversary and the guarantees we would like a protocol to satisfy are modeled as security properties. The security of the protocol can then be mathematically proven. Such proofs can be automated with tools like ProVerif or Tamarin. One of the big challenge when it comes to designing and formally proving the security an “industrial- level” protocol lies in the fact that such protocols are usually heavier than academic protocols and that they aim at more complex security properties than the classical ones. With this thesis, we wanted to focus on two use cases: electronic voting and mobile payment. We designed two protocols, one for each respective use case and proved their security using automated prover tools. The first one, Belenios VS, is a variant of an existing voting scheme, Belenios RF. It specifies a voting ecosystem allowing a user to cast a ballot from a voting sheet by flashing a code. The protocol’s security has been proven using the ProVerif tool. It guarantees that the vote confidentiality cannot be broken and that the user is capable of verifying their vote is part of the final result by performing a simple task that requires no technical skills all of this even if the user’s device is compromised – by a malware for instance. The second protocol is a payment one that has been conceived in order to be fully scalable with the existing payment ecosystem while improving the security management and cost on the smartphone. Its security has been proven using the Tamarin prover and holds even if the user’s device is under an attacker’s control