Dissertations / Theses: 'Systèmes, Conception de – Méthodes formelles (informatique)'

1

Berner, David. "Utilisation de méthodes formelles dans la conception conjointe de systèmes embarqués." Rennes 1, 2006. http://www.theses.fr/2006REN1S015.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

2

Prigent, Armelle. "Le test des systèmes temps-réel paramétrés : application à la conception d'architectures avioniques." Nantes, 2003. http://www.theses.fr/2003NANT2097.

Full text

Abstract:

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).

APA, Harvard, Vancouver, ISO, and other styles

3

Syed, Alwi Syed Hussein. "Vérification compositionnelle pour la conception sûre de systèmes embarqués." Paris 6, 2013. http://www.theses.fr/2013PA066230.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

4

Kehren, Christophe. "Motifs formels d'architectures de systèmes pour la sûreté de fonctionnement." Phd thesis, Ecole nationale superieure de l'aeronautique et de l'espace, 2005. http://tel.archives-ouvertes.fr/tel-00011496.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

5

Lamboley, Patrick. "Proposition d'une méthode formelle d'automatisation de systèmes de production à l'aide de la méthode B." Nancy 1, 2001. http://www.theses.fr/2001NAN10177.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

6

Hamon, Juan Carlos. "Méthodes et outils de la conception amont pour les systèmes et les microsystèmes." Toulouse, INPT, 2005. http://ethesis.inp-toulouse.fr/archive/00000111/.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

7

Sarray, Ines. "Conception de systèmes de reconnaissance d’activités humaines." Thesis, Université Côte d'Azur (ComUE), 2019. http://www.theses.fr/2019AZUR4016.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

8

Lohr, Christophe. "Contribution à la conception de systèmes temps-réel s'appuyant sur la technique de description formelle RT-Lotos." Phd thesis, Institut National Polytechnique de Toulouse - INPT, 2002. http://tel.archives-ouvertes.fr/tel-00005228.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

9

Aljer, Ammar. "Co-design et raffinement en B : BHDL tool, plateforme pourr la conception de composants numériques." Lille 1, 2004. https://pepite-depot.univ-lille.fr/LIBRE/Th_Num/2004/50376-2004-Aljer.pdf.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

10

Filipiak, Alicia. "Conception et analyse formelle de protocoles de sécurité, une application au vote électronique et au paiement mobile." Thesis, Université de Lorraine, 2018. http://www.theses.fr/2018LORR0039/document.

Full text

Abstract:

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

APA, Harvard, Vancouver, ISO, and other styles

11

Arcile, Johan. "Conception, modélisation et vérification formelle d’un système temps-réel d’agents coopératifs : application aux véhicules autonomes communicants." Thesis, Université Paris-Saclay (ComUE), 2019. http://www.theses.fr/2019SACLE029.

Full text

Abstract:

Cette thèse est motivée par la question de la validation de propriétés dans un système composé de plusieurs agents mobiles prenants individuellement des décisions en temps réel.Chaque agent a une perception de l'environnement qui lui est propre et peut communiquer avec les autres agents à proximité.L'application qui a été choisie comme cas d'étude est celle des véhicules autonomes, qui du fait du large nombre de variables impliquées dans la représentation de tels systèmes, rend impossible des approches naïves.Les problématiques traitées concernent, d'une part, la modélisation d'un tel système, notamment le choix du formalisme et du niveau d'abstraction du modèle, et d'autre part, la mise en place d'un protocole d'évaluation de la prise de décision des véhicules.Ce dernier point inclut la question de l'efficacité de l'exploration de l'espace d'états du modèle.La thèse présente un ensemble de travaux, pouvant être complémentaires, visant à traiter ces problématiques.Tout d'abord, le système, composé des véhicules autonomes et de leur environnement, est défini avec précision.Il permet notamment d'observer l'impact des communications entre véhicules sur leur comportement.Le cadre logiciel VerifCar dédié à l'analyse de prise de décision de véhicules autonomes communicants est ensuite présenté.Il inclut un modèle paramétrique d'automates temporisés offrant la possibilité de vérifier des propriétés de logique temporelle.Une méthodologie d'analyse utilisant ces propriétés est présentée.On propose également une approche complémentaire permettant dans certains cas une meilleure efficacité et une plus grande expressivité.Elle est fondée sur le formalisme des MAPTs (Multi-Agent with timed Periodic Tasks), qui a été conçu pour la modélisation de systèmes temps réel d'agents coopératifs.Des algorithmes permettant une exploration dynamique des états de ce type de modèles (c'est à dire sans que l'espace d'états ne doive être préalablement construit) sont présentés.Enfin, une méthode combinée alliant la simulation aux outils de vérification de modèle afin de contrôler le niveau de réalisme est décrite et appliquée au cas d'étude
This thesis is motivated by the question of the validation of properties in a system composed of several mobile agents individually making decisions in real time.Each agent has a perception of their own environment and can communicate with other agents nearby.The application that has been chosen as a case study is that of autonomous vehicles, which because of the large number of variables involved in the representation of such systems, makes naive approaches impossible.The issues addressed concern, on the one hand, the modeling of such a system, in particular the choice of the formalism and the level of abstraction of the model, and on the other hand, the implementation of an evaluation protocol of decision making of vehicles.This last point includes the question of the efficiency of the exploration of the state space of the model.The thesis presents a set of works, which can be complementary, aiming to treat these problems.First, the system, consisting of autonomous vehicles and their environment, is precisely defined.It allows in particular to observe the impact of communications between vehicles on their behavior.The VerifCar software framework dedicated to decision-making analysis of communicating autonomous vehicles is then presented.It includes a parametric model of timed automata with the ability to check temporal logic properties.An analysis methodology using these properties is presented.A complementary approach is also proposed, which in some cases allows for greater efficiency and greater expressiveness.It is based on the formalism of MAPTs (Multi-Agent with Timed Periodic Tasks), which was designed for modeling real-time systems of cooperative agents.Algorithms allowing a dynamic exploration of the states of this type of model (that is to say without the state space having to be built beforehand) are presented.Finally, a combined method combining simulation and model verification tools to control the level of realism is described and applied to the case study

APA, Harvard, Vancouver, ISO, and other styles

12

Bernard, Romain. "Analyses de sûreté de fonctionnement multi-systèmes." Phd thesis, Université Sciences et Technologies - Bordeaux I, 2009. http://tel.archives-ouvertes.fr/tel-00441310.

Full text

Abstract:

Cette thèse se situe au croisement de deux domaines : la sûreté de fonctionnement des systèmes critiques et les méthodes formelles. Nous cherchons à établir la cohérence des analyses de sûreté de fonctionnement réalisées à l'aide de modèles représentant un même système à des niveaux de détail différents. Pour cela, nous proposons une notion de raffinement dans le cadre de la conception de modèles AltaRica : un modèle détaillé raffine un modèle abstrait si le modèle abstrait simule le modèle détaillé. La vérification du raffinement de modèles AltaRica est supportée par l'outil de model-checking MecV. Ceci permet de réaliser des analyses multi-systèmes à l'aide de modèles à des niveaux de détail hétérogènes : le système au centre de l'étude est détaillé tandis que les systèmes en interface sont abstraits. Cette approche a été appliquée à l'étude d'un système de contrôle de gouverne de direction d'un avion connecté à un système de génération et distribution électrique.

APA, Harvard, Vancouver, ISO, and other styles

13

Sampaio, Paulo Nazarena Maia. "Conception formelle de documents multimédia interactifs : une approche s'appuyant sur RT-Lotos." Toulouse 3, 2003. http://www.theses.fr/2003TOU30020.

Full text

Abstract:

Cette thèse présente une méthodologie pour la conception formelle de documents multimédia interactifs s'appuyant sur la technique de description formelle RT-LOTOS. La complexité de ces documents et l'utilisation de modèles auteur de haut niveau pour leur édition peuvent amener l'auteur, dans certains cas, à spécifier des relations de synchronisation qui ne pourront pas être satisfaites lors de la présentation du document, caractérisant ainsi des situations d'incohérence temporelle. D'où le besoin d'utiliser, lors de la conception d'un document, des techniques permettant de donner une sémantique formelle au comportement dynamique du document, d'appliquer des méthodes de vérification de la cohérence temporelle, et d'ordonnancer la présentation tout en tenant compte du non-déterminisme temporel propre au document. Par la méthodologie présentée dans ce mémoire, nous permettons à l'auteur de concevoir un document en utilisant le modèle auteur de son choix, et montrons comment exprimer le comportement logique et temporel du document en RT-LOTOS. Ensuite, nous développons des techniques pour vérifier la cohérence temporelle du document et ordonnancer sa présentation en s'appuyant sur des modèles (automates temporels) dérivés de la spécification RT-LOTOS. Nous proposons une illustration de la mise en œuvre de cette méthodologie en s'appuyant sur l'utilisation du langage SMIL 2. 0 pour l'édition des documents multimédia interactifs. Les principales contributions présentées dans ce mémoire sont: la définition d'une approche pour traduire automatiquement des documents SMIL 2. 0 en RT-LOTOS, la vérification et la formalisation de propriétés de cohérence temporelle, la proposition de solutions pour maîtriser l'explosion combinatoire des automates temporels sous-jacents, la définition de politiques d'ordonnancement s'appuyant sur un graphe d'ordonnancement dérivé automatiquement de la spécification RT-LOTOS (le TLSA), la définition d'un algorithme pour réengendrer, dans la mesure du possible, des documents SMIL 2. 0 cohérents à partir de documents incohérents, et finalement la mise en œuvre d'un prototype (le TLSA Player) pour présenter des documents multimédia interactifs cohérents
Formal design of interactive multimedia documents using RT-LOTOS. This thesis presents a methodology for the formal design of interactive multimedia documents based on the formal description technique RT-LOTOS. The complexity of these documents and the utilization of high level authoring models for the edition of these documents can lead authors, in certain cases, to specify synchronization relations which could not be satisfied during the presentation of the document, thus characterizing the occurrence of temporal inconsistencies. For this reason, we need to use techniques which provide the formal semantics for the dynamic behaviour of the document, consistency checking, and the scheduling of the presentation taking into account the temporal non-determinism of these documents. By means of the methodology presented in this thesis, we allow the author to design a document using the authoring model of his choice, and then we show how to express the logical and temporal behaviour of the document into an RT-LOTOS specification. Further on, we also propose formal techniques for the temporal consistency checking, and scheduling the presentation of the document based on temporal automata derived from the RT-LOTOS specification. .

APA, Harvard, Vancouver, ISO, and other styles

14

Mokrani, Hocine. "Assistance au raffinement dans la conception des systèmes embarqués." Thesis, Paris, ENST, 2014. http://www.theses.fr/2014ENST0029/document.

Full text

Abstract:

La dernière décennie, la complexité des technologies embarqués a explosé et les flots de conception industrielle habituels ne suffisent plus pour proposer des produits fiables en respectant les exigences du marché. Ainsi, le développement de nouvelles méthodologies de conception est devenu un besoin impératif. La thèse vise l'amélioration des méthodologies de conception des systèmes embarqués. En proposant une approche de conception par niveaux d’abstraction, la nouvelle approche permet de guider et d’assister les concepteurs dans les étapes de conception, précisément de raffiner les composants de communication. Elle offre des garanties de préservation des propriétés fonctionnelles le long du flot de conception. La méthode proposée permet de raisonner sur les différents niveaux de description d'un système en exploitant des techniques de preuve de propriétés associées aux raffinement formel
In the last decade, the complexity of embedded systems has exploded and the usual industrial design flows do not suffice any more to propose reliable products while respecting time to market constrain. Thus, developing new design methodologies has become an imperative. The thesis aims at the improvement of the methodologies of conception of the embedded systems. It proposes a method for assisting the process of refinement along the design flow. The proposed approach splits the design flow into multiple-levels, in order to guide the designer in the design process, from the most abstract model down to a synthesizable model. Furthermore, by using formal techniques the method allows to check the preservation of functional correctness along the design flow

APA, Harvard, Vancouver, ISO, and other styles

15

Kherroubi, Souad. "Un cadre formel pour l'intégration de connaissances du domaine dans la conception des systèmes : application au formalisme Event-B." Thesis, Université de Lorraine, 2018. http://www.theses.fr/2018LORR0230/document.

Full text

Abstract:

Cette thèse vise à définir des techniques pour mieux exploiter les connaissances du domaine dans l’objectif de rendre compte de la réalité de systèmes qualifiés de complexes et critiques. La modélisation est une étape indispensable pour effectuer des vérifications et exprimer des propriétés qu’un système doit satisfaire. La modélisation est une représentation simplificatrice, mais réductionniste de la réalité d’un système. Or, un système complexe ne peut se réduire à un modèle. Un modèle doit s’intégrer dans sa théorie observationnelle pour rendre compte des anomalies qu’il peut y contenir. Notre étude montre clairement que le contexte est la première problématique à traiter car principale source de conflits dans le processus de conception d’un système. L’approche retenue dans cette thèse est celle d’intégrer des connaissances du domaine en associant le système à concevoir à des formalismes déclaratifs qualifiés de descriptifs appelés ontologies. Notre attention est portée au formalisme Event-B dont l’approche correct-par-construction appelée raffinement est le principal mécanisme dans ce formalisme qui permet de faire des preuves sur des représentations abstraites de systèmes pour exprimer/vérifier des propriétés de sûreté et d’invariance. Le premier problème traité concerne la représentation et la modélisation des connaissances du contexte en V&V de modèles. Suite à l’étude des sources de conflits, nous avons établi de nouvelles règles pour une extraction de connaissances liées au contexte par raffinement pour la V&V. Une étude des formalismes de représentation et d’interprétation logiques du contexte a permis de définir un nouveau mécanisme pour mieux structurer les modèles Event-B. Une deuxième étude concerne l’apport des connaissances du domaine pour la V&V. Nous définissons une logique pour le formalisme Event-B avec contraintes du domaine fondées sur les logiques de description, établissons des règles à exploiter pour l’intégration de ces connaissances à des fins de V&V. L’évaluation des propositions faites portent sur des études de cas très complexes telles que les systèmes de vote dont des patrons de conception sont aussi développés dans cette thèse. Nous soulevons des problématiques fondamentales sur la complémentarité que peut avoir l’intégration par raffinement des connaissances du domaine à des modèles en exploitant les raisonnements ontologiques, proposons de définir de nouvelles structures pour une extraction partiellement automatisée
This thesis aims at defining techniques to better exploit the knowledge provided from the domain in order to account for the reality of systems described as complex and critical. Modeling is an essential step in performing verifications and expressing properties that a system must satisfy according to the needs and requirements established in the specifications. Modeling is a representation that simplifies the reality of a system. However, a complex system can not be reduced to a model. A model that represents a system must always fit into its observational theory to account for any anomalies that it may contain. Our study clearly shows that the context is the first issue to deal with as the main source of conflict in the design process of a system. The approach adopted in this thesis is that of integrating knowledge of the domain by associating the system to design with declarative formalisms qualified of descriptive ones that we call ontologies. We pay a particular attention to the Event-B formalism, whose correct-by-construction approach called refinement is the main mechanism at the heart of this formalism, which makes it possible to make proofs on abstract representations of systems for expressing and verifying properties of safety and invariance. The first problem treated is the representation and modeling of contextual knowledge in V&V of models. Following to the study looked at the different sources of conflict, we established new definitions and rules for a refinement context knowledge extraction for Event-B V&V. A study of logical formalisms that represent and interpret the context allowed us to define a new mechanism for better structuring Event-B models. A second study concerns the contribution that domain knowledge can make to the V&V of models. We define a logic for the Event-B formalism with domain constraints based on the description logic, and we define rules to integrate domain knowledge for model V&V. The evaluation of the proposals made deal with very complex case studies such as voting systems whose design patterns are also developed in this thesis. We raise fundamental issues about the complementarity that the integration of domain knowledge can bring to Event-B models by refinement using ontological reasoning, and we propose to define a new structures for a partially automated extraction on both levels, namely the V&V

APA, Harvard, Vancouver, ISO, and other styles

16

Sagaspe, Laurent. "Allocation sûre dans les systèmes aéronautiques : Modélisation, Vériﬁcation et Génération." Phd thesis, Université Sciences et Technologies - Bordeaux I, 2008. http://tel.archives-ouvertes.fr/tel-00906924.

Full text

Abstract:

Cette thèse propose un cadre afin de modéliser, vérifier et générer des allocations de fonctions d'un système embarqué sur des ressources avioniques. Ce cadre est fondé sur l'utilisation du langage Altarica pour décrire formellement la propagation des défaillances au sein d'un système embarqué, sur l'utilisation de techniques de vérification tel que le "model-checking" et la génération d'arbre de défaillances et sur les techniques de résolution de contraintes. Les travaux sont illustrés par deux études de cas: l'allocation de ressources de calcul et de communication à une fonction de "suivi de terrain" d'un avion de chasse, le placement des équipements d'un système hydraulique au sein d'un avion en tenant compte de risques tels que l'éclatement d'un pneu ou d'un réacteur.

APA, Harvard, Vancouver, ISO, and other styles

17

El, Jamal Mohamad Hani. "Contribution à l'évolution des exigences et son impact sur la sécurité." Phd thesis, Université Paul Sabatier - Toulouse III, 2006. http://tel.archives-ouvertes.fr/tel-00139543.

Full text

Abstract:

Le travail de la thèse porte sur la problématique de l'évolution des exigences et son analyse d'impact sur la sécurité. Au cours du développement des systèmes, les parties prenantes demandent l'application des évolutions, afin d'améliorer leurs fonctionnalités. L'occurrence d'une évolution affecte plusieurs aspects comme: la sécurité, le coût du développement et les délais. Lorsque le développement concerne un système complexe où le nombre des exigences est de l'ordre de dizaines de milliers, alors les demandes des évolutions rendent l'analyse d'impact du changement de plus en plus difficile. Malheureusement, la problématique de l'évolution des exigences n'est pas encore complètement résolue en milieu industriel. Notre étude est située dans le contexte d'ingénierie système et ingénierie des exigences, en intégrant des modèles formels et outils supports associés pour la vérification des propriétés de sécurité. La méthodologie est basée sur la norme industrielle de l'EIA-632 et sur le format VOLERE d'ingénierie des exigences en intégrant un modèle de traçabilité. De cette démarche ingénierie système, on a développé une méthodologie associée et un système d'information du processus de changement/évolution des exigences. Enfin, ce travail présente la méthodologie de la recherche d'impact lors de la demande de changement, et les outils qui supportent la méthodologie de la recherche d'impact, en se basant sur la méthode formelle (RAISE), qui nous permet d'analyser l'impact de l'évolution sur la sécurité.

APA, Harvard, Vancouver, ISO, and other styles

18

Mohand, Oussaïd Linda. "Conception et vérification formelles des interfaces homme-machine multimodales : applications à la multimodalité en sortie." Thesis, Chasseneuil-du-Poitou, Ecole nationale supérieure de mécanique et d'aérotechnique, 2014. http://www.theses.fr/2014ESMA0022/document.

Full text

Abstract:

Les interfaces homme-machine (IHM) multimodales offrent à l’utilisateur la possibilité de combiner les modalités d’interaction afin d’augmenter la robustesse et l’utilisabilité de l’interface utilisateur d’un système. Plus particulièrement, en sortie, les IHM multimodales permettent au système de restituer à l’utilisateur, l’information produite par le noyau fonctionnel en combinant sémantiquement plusieurs modalités. Dans l’optique de concevoir de telles interfaces pour des systèmes critiques, nous avons proposé un modèle formel de conception des interfaces multimodales en sortie. Le modèle proposé se décompose en deux modèles : le modèle de fission sémantique qui décrit la décomposition de l’information à restituer en informations élémentaires, et le modèle d’allocation qui spécifie l’allocation des modalités et médias aux informations élémentaires. Nous avons également développé une formalisation B Événementiel détaillée des deux modèles : fission sémantique et allocation. Cette formalisation a été instanciée sur des études de cas puis généralisée dans un processus de développement B Événementiel cadre dans lequel s’inscrivent les modèles de fission sémantique et d’allocation. Cette formalisation a permis de procéder à la vérification de propriétés de sûreté, de vivacité et d’utilisabilité
Multimodal Human-Computer Interfaces (HCI) offer to users the possibility to combine interaction modalities in order to increase user interface robustness and usability. Specifically, output multimodal HCI allow system to return to the user, the information generated by the functional core by combining semantically different modalities. In order to design such interfaces for critical systems, we proposed a formal model for the design of output multimodal interfaces. The proposed model consists of two models: the semantic fission model describes the decomposition of the information to return into elementary information and the allocation model specifies the allocation of the elementary information with modalities and media. We have also developed a detailed Event B formalization for the two models: semantic fission and allocation. This formalization has been instantiated on case studies and generalized in an Event B development process framework including semantic fission and allocation models. This formalization allows to carry out safety, liveness and usability properties verification

APA, Harvard, Vancouver, ISO, and other styles

19

Methni, Amira. "Méthode de conception de logiciel système critique couplée à une démarche de vérification formelle." Thesis, Paris, CNAM, 2016. http://www.theses.fr/2016CNAM1057/document.

Full text

Abstract:

Avec l'évolution des technologies, la complexité des systèmes informatiques ne cesse de s'accroître. Parmi ces systèmes, on retrouve les logiciels critiques qui doivent offrir une garantie de sûreté de fonctionnement qui s'avère crucial et pour lesquels un dysfonctionnement peut avoir des conséquences graves. Les méthodes formelles fournissent des outils permettant de garantir mathématiquement l'absence de certaines erreurs. Ces méthodes sont indispensables pour assurer les plus hauts niveaux de sûreté. Mais l'application de ces méthodes sur un code système bas niveau se heurte à des difficultés d'ordre pratique et théorique. Les principales difficultés concernent la prise en compte des aspects bas niveau, comme les pointeurs et les interactions avec le matériel spécifique. De plus, le fait que ces systèmes soient concurrents conduit à une augmentation exponentielle du nombre de comportements possibles, ce qui rend plus difficile leur vérification. Dans cette thèse, nous proposons une méthodologie pour la spécification et la vérification par model-checking de ce type de systèmes, en particulier, ceux implémentés en C. Cette méthodologie est basée sur la traduction de la sémantique de C en TLA+, un langage de spécification formel adapté à la modélisation de systèmes concurrents. Nous avons proposé un modèle de mémoire et d'exécution d'un programme C séquentiel en TLA+. En se basant sur ce modèle, nous avons proposé un ensemble de règles de traduction d'un code C en TLA+ que nous avons implémenté dans un outil, appelé C2TLA+. Nous avons montré comment ce modèle peut s'étendre pour modéliser les programmes C concurrents et gérer la synchronisation entre plusieurs processus ainsi que leur ordonnancement. Pour réduire la complexité du model-checking, nous avons proposé une technique permettant de réduire significativement la complexité de la vérification. Cette réduction consiste pour un code C à agglomérer une suite d'instructions lors de la génération du code TLA+, sous réserve d'un ensemble de conditions.Nous avons appliqué la méthodologie proposée dans cette thèse sur un cas d'étude réel issu de l'implémentation d'un micronoyau industriel,sur lequel nous avons vérifié un ensemble de propriétés fonctionnelles. L'application de la réduction a permis de réduire considérablement le temps de la vérification, ce qui la rend utilisable en pratique.Les résultats ont permis d'étudier le comportement du système, de vérifier certaines propriétés et de trouver des bugs indétectables par des simples tests
Software systems are critical and complex. In order to guarantee their correctness, the use of formal methodsis important. These methods can be defined as mathematically based techniques, languages and tools for specifying and reasoning about systems. But, the application of formal methods to software systems, implemented in C, is challenging due to the presence of pointers, pointer arithmetic andinteraction with hardware. Moreover, software systems are often concurrent, making the verification process infeasible. This work provides a methodology to specify and verify C software systems usingmodel-checking technique. The proposed methodology is based on translating the semantics of Cinto TLA+, a formal specification language for reasoning about concurrent and reactive systems. We define a memory and execution model for a sequential program and a set of translation rules from C to TLA+ that we developed in a tool called C2TLA+. Based on this model, we show that it can be extended to support concurrency, synchronization primitives and process scheduling. Although model-checking is an efficient and automatic technique, it faces the state explosion problem when the system becomes large. To overcome this problem, we propose a state-space reduction technique. The latter is based on agglomerating a set of C instructions during the generation phase of the TLA+ specification. This methodology has been applied to a concrete case study, a microkernel of an industrial real-time operating system, on which a set of functional properties has been verified. The application of the agglomeration technique to the case study shows the usefulness of the proposed technique in reducing the complexity of verification. The obtained results allow us to study the behavior of the system and to find errors undetectable using traditional testing techniques

APA, Harvard, Vancouver, ISO, and other styles

20

Fournier, Émilien. "Accélération matérielle de la vérification de sûreté et vivacité sur des architectures reconfigurables." Electronic Thesis or Diss., Brest, École nationale supérieure de techniques avancées Bretagne, 2022. http://www.theses.fr/2022ENTA0006.

Full text

Abstract:

Le Model-Checking est une technique automatisée, utilisée dans l’industrie pour la vérification, enjeu majeur pour la conception de systèmes fiables, cadre dans lequel performance et scalabilité sont critiques. La vérification swarm améliore la scalabilité par une approche partielle reposant sur l’exécution concurrente d’analyses randomisées. Les architectures reconfigurables promettent des gains de performance significatifs. Cependant, les travaux existant souffrent d’une conception monolithique qui freine l’exploration des opportunités des architectures reconfigurable. De plus, ces travaux sont limités a la verification de sûreté. Pour adapter la stratégie de vérification au problème, cette thèse propose un framework de vérification matérielle, permettant de gagner, au travers d’une architecture modulaire, une généricité sémantique et algorithmique, illustrée par l’intégration de 3 langages de spécification et de 6 algorithmes. Ce cadre architectural permet l’étude de l’efficacité des algorithmes swarm pour obtenir un cœur de vérification de sûreté scalable. Les résultats, sur un FPGA haut de gamme, montrent des gains d’un ordre de grandeur par rapport à l’état de l’art. Enfin, on propose le premier accélérateur matériel permettant la vérification des exigences de sûreté et de vivacité. Les résultats démontrent un facteur d’accélération moyen de 4875x par rapport au logiciel
Model-Checking is an automated technique used in industry for verification, a major issue in the design of reliable systems, where performance and scalability are critical. Swarm verification improves scalability through a partial approach based on concurrent execution of randomized analyses. Reconfigurable architectures promise significant performance gains. However, existing work suffers from a monolithic design that hinders the exploration of reconfigurable architecture opportunities. Moreover, these studies are limited to safety verification. To adapt the verification strategy to the problem, this thesis first proposes a hardware verification framework, allowing to gain, through a modular architecture, a semantic and algorithmic genericity, illustrated by the integration of 3 specification languages and 6 algorithms. This framework allows efficiency studies of swarm algorithms to obtain a scalable safety verification core. The results, on a high-end FPGA, show gains of an order of magnitude compared to the state-of-the-art. Finally, we propose the first hardware accelerator for safety and liveness verification. The results show an average speed-up of 4875x compared to software

APA, Harvard, Vancouver, ISO, and other styles

21

Pham, Thi-Kim-Dung. "Development of Correct-by-Construction Software using Product Lines." Thesis, Paris, CNAM, 2017. http://www.theses.fr/2017CNAM1138/document.

Full text

Abstract:

Nous avons commencé la thèse par la littérature d'enquête sur les approches SPLE et CbyC dans l'état de l'art. Sur la base de l'aperçu et des connaissances obtenues, nous avons analysé les problèmes existants et suggéré des moyens de les résoudre pour notre objectif principal. Nous avons proposé dans le chapitre 2 une méthodologie pour développer des lignes de produits afin que les produits générés soient corrects par construction. Notre intention principale est qu'un utilisateur n'a pas besoin de connaître le processus de génération de produit mais peut recevoir un produit final correct en sélectionnant une configuration de fonctionnalité. En utilisant la méthodologie, les produits finaux sont générés automatiquement et leur exactitude est garantie. À la suite de cette proposition, nous sommes passés au chapitre 3 pour définir la langue de FFML qui est utilisé pour l'écriture de modules. Le mécanisme de réutilisation et de modification, défini pour la langue et appliqué à toutes sortes d'artefacts (spécification, code et preuve de précision) réduit l'effort de programmation. Au chapitre 4, nous nous sommes concentrés sur la définition des mécanismes de composition pour la composition des modules FFML et les intégrons à l'outil FFML Product Generator. L'évaluation de notre méthodologie est réalisée par le développement de deux lignes de produits logiciels, le compte bancaire SPL et le SPL de poker, ce dernier étant un peu plus complexe que le premier. Dans l'évaluation, nous avons souligné les avantages et la limitation de notre méthodologie
We began the thesis by survey literature on SPLE and CbyC approaches in the State of the Art. Based on the overview and the insights obtained, we have analyzed the existing problems and suggested ways to solve them for our main goal. We have proposed in Chapter 2 a methodology to develop product lines such that the generated products are correct-by-construction. Our main intention is that a user does not need to know the product generation process but can receive a correct final product from selecting a configuration of features. Using the methodology, the final products are generated automatically and their correctness is guaranteed. Following this proposal, we have moved in Chapter 3 to define the FFML language that is used for writing modules. The reuse and modification mechanism, defined for the language and applied to all kinds of artifacts (specification, code and correctness proof), reduce the programming effort. In Chapter 4, we have focused on defining the composition mechanisms for composing FFML modules and embedded them into the FFML Product Generator tool. The evaluation of our methodology is performed through the development of two software product lines, the Bank Account SPL and the Poker SPL, the latter being a bit more complex than the former. In the evaluation, we have highlighted the advantages and the limitation of our methodology

APA, Harvard, Vancouver, ISO, and other styles

22

Courtault, Jean-René. "Logiques de ressources dynamiques : modèles, propriétés et preuves." Thesis, Université de Lorraine, 2015. http://www.theses.fr/2015LORR0033/document.

Full text

Abstract:

En informatique, la notion de ressource est une notion centrale. Nous considérons comme ressource toute entité pouvant être composée ou décomposée en sous-entités. Plusieurs logiques ont été proposées afin de modéliser et d’exprimer des propriétés sur celles-ci, comme la logique BI exprimant des propriétés de partage et de séparation. Puisque les systèmes informatiques manipulent des ressources, la proposition de nouveaux modèles capturant la dynamique de ces ressources, ainsi que la vérification et la preuve de propriétés sur ces modèles, sont des enjeux cruciaux. Dans ce contexte, nous définissons de nouvelles logiques permettant la modélisation logique de la dynamique des ressources, proposant de nouveaux modèles et permettant l’expression de nouvelles propriétés sur cette dynamique. De plus, pour ces logiques, nous proposons des méthodes des tableaux et d’extraction de contre-modèles. Dans un premier temps, nous définissons de nouveaux réseaux de Petri, nommés ß-PN, et proposons une nouvelle sémantique à base de ß-PN pour BI. Puis nous proposons une première extension modale de BI, nommée DBI, permettant la modélisation de ressources ayant des propriétés dynamiques, c’est-à-dire évoluant en fonction de l’état courant d’un système. Ensuite, nous proposons une logique, nommée DMBI, modélisant des systèmes manipulant/produisant/consommant des ressources. Par ailleurs, nous proposons une nouvelle logique (LSM) possédant de nouvelles modalités multiplicatives (en lien avec les ressources). Pour finir, nous introduisons la séparation au sein des logiques épistémiques, obtenant ainsi une nouvelle logique ESL, exprimant de nouvelles propriétés épistémiques
In computer science, the notion of resource is a central concern. We consider as a resource, any entity that can be composed or decomposed into sub-entities. Many logics were proposed to model and express properties on these resources, like BI logic, a logic about sharing and separation of resources. As the computer systems manipulate resources, a crucial issue consists in providing new models that capture the dynamics of resources, and also in verifying and proving properties on these models. In this context, we define new logics with new models and new languages allowing to respectively capture and express new properties on the dynamics of resources. Moreover, for all these logics, we also study the foundations of proof search and provide tableau methods and counter-model extraction methods. After defining new Petri nets, called ß-PN, we propose a new semantics based on ß-PN for BI logic, that allows us to show that BI is able to capture a kind of dynamics of resources. After observing that it is necessary to introduce new modalities in BI logic, we study successively different modal extensions of BI. We define a logic, called DBI, that allows us to model resources having dynamic properties, meaning that they evolve during the iterations of a system. Then, we define a logic, called DMBI, that allows us to model systems that manipulate/produce/consume resources. Moreover, we define a new modal logic, called LSM, having new multiplicative modalities, that deals with resources. Finally, we introduce the notion of separation in Epistemic Logic, obtaining a new logic, called ESL, that models and expresses new properties on agent knowledge

APA, Harvard, Vancouver, ISO, and other styles

23

Garnier, Ilias. "Formalisme pour la conception haut-niveau et détaillée de systèmes de contrôle-commande critiques." Phd thesis, Université Paris Sud - Paris XI, 2012. http://tel.archives-ouvertes.fr/tel-00676901.

Full text

Abstract:

L'importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d'application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s'intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d'outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l'influence du flot d'informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l'applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l'angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d'un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d'établir un formalisme permettant la preuve du délai de bout-en-bout lors d'une démarche de développement incrémentale.

APA, Harvard, Vancouver, ISO, and other styles

24

Nastov, Blazo. "Contribution à une méthode outillée pour la conception de langages de modélisation métier interopérables, analysables et prouvables pour l'Ingénierie Système basée sur des Modèles." Thesis, Montpellier, 2016. http://www.theses.fr/2016MONTT272/document.

Full text

Abstract:

L'Ingénierie des Systèmes (IS) est une approche pluridisciplinaire et collaborative pour mener à bâtir et structurer la conception puis la réalisation et le développement de systèmes complexes. L’IS repose à la fois sur une approche processus et sur la mise en oeuvre de modèles de systèmes s'appuyant de fait dans un contexte basé ou dirigé par des modèles. On parle alors d’Ingénierie Système Basée sur des Modèles (ISBM ou Model based Systems Engineering MBSE). L’ISBM introduit des concepts, méthodes et techniques pour construire et gérer des modèles. Elle a pour objectif l’atteinte et l’amélioration de leur qualité afin de procurer aux parties prenantes un degré de confiance jugé suffisant pour aider la prise des décisions de conception, d'amélioration et de réalisation. Ces décisions conditionnent le fonctionnement, la sûreté, la sécurité, les coûts, et plus généralement tout un ensemble de propriétés attendues à la fois du modèle comme du système modélisé, tout au long de la phase aval de l’ingénierie et de développement, jusqu’à la réalisation et au déploiement du système. La qualité des modèles est obtenue au travers des processus de Vérification et Validation (V&V). Les objectifs sont alors d’assurer que les modèles soient cohérents, bien formés, bien construits et représentés correctement. En effet, aux yeux des parties prenantes, les modèles doivent être fiables, fidèles et pertinents au regard des besoins des concepteurs, représentant aussi précisément que possible le point de vue du système en cours de conception. Des langages de modélisation dit « métier » (Domain Specific Modelling Languages ou DSML) sont spécifiquement créés pour pouvoir fournir des représentations i.e. des modèles dans les différents points de vue sur le système. Un DSML est basé sur une syntaxe et sur une sémantique. La sémantique de ces langages est en général fournie par des approches externes (vérificateurs de modèles). Ces dernières sont, à notre sens, une limitation clé pour le déploiement des stratégies de V&V dans le contexte de l’ISBM. En réponse à cette limitation, la contribution conceptuelle de cette thèse est présentée sous la forme d’un nouveau langage de métamodélisation, nommé xviCore (noyau exécutable, vérifiable et interopérable). xviCore fournit les concepts et les principes pour définir puis vérifier et valdier la syntaxe et la sémantique en phase de construction de tels DSML en combinant trois métalangages : un métalangage orienté objet pour la conception de la partie syntaxique, un métalangage pour la conception du comportement et un métalangage pour la conception de propriétés formelles. La contribution méthodologique de ces travaux permet ensuite le déploiement d’une stratégie de V&V «directe» en lieu et place des traditionnelles approches externes. Elle est basée sur la simulation et la preuve formelle de propriétés. Le mécanisme de simulation permet d’observer le comportement des modèles de systèmes au travers de leur exécution, tandis que le mécanisme de preuve permet de spécifier et ensuite de vérifier des propriétés formelles. La contribution technique se compose d’un ensemble des plugins Eclipse qui implémentent le métalangage xviCore, le mécanisme de simulation et le mécanisme de la preuve formelle
Systems Engineering (SE) is an interdisciplinary and collaborative approach for successful design and management of large scale complex systems. Among other principles, SE promotes and mandates a model-based (or model-driven) approach for all stages of system design processes, denoted Model-Based Systems Engineering (MBSE). This implies concepts, techniques and tools for creating and managing various systems models for the purpose of stakeholders, and for reaching and improving the quality of models helping then stakeholders during decision-making processes, to make decisions faster and efficiently with enough confidence. Indeed, these decisions impact all along the downstream phases of system engineering and development until the realization and deployment of the real system, its functioning, safety, security, induced costs and so on. In this work, a particular attention is given to model verification and validation (V&V). The goals are to assure prior to decision-making processes, first, that models are coherent, well-formed and correctly build and represented, and second, that they are trustworthy and relevant, representing as accurately as possible the viewpoints of a system under design as expected by stakeholders.Such models provide stakeholders with confidence and trust, aiding them in making, but also in arguing decisions. Models are created by using modeling languages that are specifically tailored for a given viewpoint of a system, denoted Domain Specific Modeling Languages (DSMLs).The basic principles on which a DSML is based are its syntax and its semantics, but current DSMLs have been more studied from the syntactical point than from the semantical one that is often neglected or, when needed, provided by means of translating the DSML into third party formalisms. This is the key limitation preventing the deployment of a successful V&V strategy in MBSE context. To overcome this shortcoming, this thesis proposes first a conceptual contribution consisting of a new metamodeling language, called eXecutable, Verifiable and Interoperable Core (xviCore), allowing stakeholders to build DSMLs (called xviDSMLs), that along with their syntax also integrates semantics. Our solution combines, three meta-languages, an object-oriented metamodeling language for the specification of the syntactical part with a formal behavioral modeling language and a property modeling language for the semantical part. The methodological contribution of this work allows the deployment of successful V&V strategies allowing for direct (without transformation) model verification by simulation and properties proof. We propose a mechanism to simulate the expected behavior of a SoI through model execution based on the blackboard-based communication model, and a mechanism for specification and verification of formal properties. The technical contribution consists of an Eclipse-EMF deployable plug-in that implements the metamodeling language xviCore and the mechanisms for simulation and formal property verification

APA, Harvard, Vancouver, ISO, and other styles

25

Petit, Mathieu. "Approche spatiale pour la caractérisation du contexte d'exécution d'un système d'information ubiquitaire." Phd thesis, Paris, ENSAM, 2010. http://pastel.archives-ouvertes.fr/pastel-00511919.

Full text

Abstract:

Les nouvelles technologies en matière d'accès à l'information, de communication sans-fil et de localisation d'informations ouvrent la voie à des innovations majeures dans l'utilisation des systèmes informatiques. Ces avancées permettent d'imaginer de nouveaux usages informatiques dont la mise en œuvre motive le développement de méthodes de conception appropriées. Plus particulièrement, l'informatique mobile combine désormais des enjeux conceptuels tels que l'accès à des services par un utilisateur en mobilité, la généralisation d'outils de localisation, la compréhension de systèmes complexes par un public non-expert ou l'importante variabilité des situations d'exécution. Cette thèse propose un cadre de conception qui adresse certains des enjeux pour la mobilité des systèmes d'information. Dans cette perspective, les attentes des utilisateurs et les contraintes technologiques inhérentes à la mobilité des constituants du système définissent un espace contextuel dont les dimensions sont prises en compte dès les premières étapes de la conception. Le modèle proposé établit comme point d'entrée une description de l'espace géographique du système pour différencier un ensemble de contextes d'exécution. L'énoncé de ces contextes permet de corréler les attentes des utilisateurs avec les capacités techniques de la plate-forme et d'offrir le niveau fonctionnel le plus acceptable dans une situation donnée. Dans un second temps, les différentes fonctionnalités et les données mises en œuvre dans chaque contexte d'exécution peuvent être ordonnées ou filtrées afin d'optimiser la présentation des informations aux utilisateurs. Ces recommandations sont produites par l'analyse conjointe des préférences d'utilisateurs selon leurs interactions et leurs comportements spatiaux. Deux cadres expérimentaux viennent illustrer les propositions du modèle. La conception d'un système mobile de suivi de compétition nautique prend en compte différents contextes d'exécution et adapte un niveau de service à des situations dégradées. Un système de documentation et de visite de campus illustre les algorithmes de recommandation et affine la présentation d'informations localement à chaque contexte d'exécution.

APA, Harvard, Vancouver, ISO, and other styles

26

Yang, Faqing. "Un environnement de simulation pour la validation de spécifications B événementiel." Phd thesis, Université de Lorraine, 2013. http://tel.archives-ouvertes.fr/tel-00951922.

Full text

Abstract:

Cette thèse porte sur la spécification, la vérification et la validation de systèmes critiques à l'aide de méthodes formelles, en particulier, B événementiel. Nous avons travaillé sur l'utilisation de B événementiel pour étudier des algorithmes de contrôle du platooning, à partir d'une version 1D simplifiée vers une version 2D plus réaliste. L'analyse critique du modèle du platooning en 1D a découvert certaines anomalies. La difficulté d'exprimer les théorèmes de deadlock-freeness dans B événementiel nous a motivé pour développer un outil, le générateur de théorèmes de deadlock-freeness, pour construire automatiquement ces théorèmes. Notre évaluation a confirmé que les preuves mathématiques ne sont pas suffisantes pour vérifier la correction d'une spécification formelle : une spécification formelle doit aussi être validée. Nous pensons que les activités de validation, comme les activités de vérification, doivent être associées à chaque raffinement. Pour ce faire, nous avons besoin de meilleurs outils de validation. Certains outils d'exécution existants échouent pour certains modèles non-déterministes exprimés en B événementiel. Nous avons donc conçu et implanté un nouvel outil d'exécution, JeB, un environnement de simulation en JavaScript pour B événementiel. JeB permet aux utilisateurs d'insérer du code sûr à la main pour fournir des calculs déterministes lorsque la traduction automatique échoue. Pour atteindre cet objectif, nous avons défini des obligations de preuve qui garantissent la correction de simulations par rapport au modèle formel.

APA, Harvard, Vancouver, ISO, and other styles

27

Pagani, Florence. "Ordres partiels pour la vérification de systèmes temps réel." Toulouse, ENSAE, 1997. http://www.theses.fr/1997ESAE0005.

Full text

Abstract:

Si l'utilité des méthodes de vérification formelle des systèmes temps réel est désormais reconnue, leur application à des systèmes complexes est encore freinée par les performances des outils disponibles. En particulier, la vérification de modèles fondée sur l'exploration exhaustive de l'espace des états d'un système est souvent limitée par ce que l'on appelle l'explosion combinatoire des états. Ce phénomène est encore accentué lorque des aspects quantitatifs (durée des actions par exemple) sont introduits dans le modèle. Une partie de l'xplosion combinatoire est due à la modélisation du parallélisme par l'entrelacement non déterministe des actions. Les techniques dites d'ordre partiel tirent parti de l'indépendance des actions s'exécutant en parallèle pour réduire l'espace des états à explorer. Ces techniques ont initialement été développées pour la vérification des systèmes temps réels afin de prendre en compte des aspects temporels quantitatifs. Nous nous intéressons en particulier à l'intégration de ces techniques dans les méthodes de vérification symboliques développées pour des automates temporisés.

APA, Harvard, Vancouver, ISO, and other styles

28

Wiels, Virginie. "Modularité pour la conception et la validation formelles de systèmes." Toulouse, ENSAE, 1997. http://www.theses.fr/1997ESAE0001.

Full text

Abstract:

Structuration et compositionnalité sont des besoins importants dans le domaine des techniques formelles pour maîtriser la taille et la complexité des spécifications. Nous proposons un formalisme qui permet de spécifier des systèmes de façon modulaire, mais aussi d'exploiter la structure des spécifications pour réaliser des vérifications modulaires. Un outil de spécification (Moka) est associé à ce formalisme et peut être combiné avec des outils de démonstration logique existants. L'approche est illustrée sur trois applications de domaines différents. Nous mettons d'abord l'accent sur les besoins d'un cadre à la fois structuré, expressif et qui permette d'utiliser des outils de vérificétion et de validation. Pour répondre à ces besoins, nous proposons de combiner la logique temporelle (pour l'expressivité et les outils de vérification) avec des technqiues algébriques (pour la structuration). Nous présentons ensuite l'approche qui combine le calcul de modules défini par Ehrig et Mahr avec une logique temporelle. Elle s'appuie sur les travaux de Fiadeiro et Maibaum utilisant la théorie des catégories pour leur "Object Calculus". L'outil associé utilise les aspects constructifs de la théorie des catégories pour mettre en oeuvre les modules de spécification et les opérations de composition. L'approche est illustrée par une application au domaine des télécommunications. Les aspects vérification sont enfin abordés : nous expliquons comment le formalisme peut être utilisé pour faire de la vérification modulaire et l'intérêt d'interfacer l'outil Moka avec un outil de démonstration logique (ici TRIO). Deux autres applications sont présentées : un mécanisme de tolérence aux fautes et un système de contrôle de commandes d'avion.

APA, Harvard, Vancouver, ISO, and other styles

29

Radhouani, Amira. "Méthodes formelles pour l'extraction d'attaques internes des Systèmes d'Information." Thesis, Université Grenoble Alpes (ComUE), 2017. http://www.theses.fr/2017GREAM025/document.

Full text

Abstract:

La sécurité des Systèmes d’Information (SI) constitue un défi majeur car elle conditionne amplement la future exploitation d’un SI. C’est pourquoi l’étude des vulnérabilités d’un SI dès les phases conceptuelles est cruciale. Il s’agit d’étudier la validation de politiques de sécurité, souvent exprimées par des règles de contrôle d’accès, et d’effectuer des vérifications automatisées sur des modèles afin de garantir une certaine confiance dans le SI avant son opérationnalisation. Notre intérêt porte plus particulièrement sur la détection des vulnérabilités pouvant être exploitées par des utilisateurs internes afin de commettre des attaques, appelées attaques internes, en profitant de leur accès légitime au système. Pour ce faire, nous exploitons des spécifications formelles B générées, par la plateforme B4MSecure, à partir de modèles fonctionnels UML et d’une description Secure UML des règles de contrôle d’accès basées sur les rôles. Ces vulnérabilités étant dues à l’évolution dynamique de l’état fonctionnel du système, nous proposons d’étudier l’atteignabilité des états, dits indésirables, donnant lieu à des attaques potentielles, à partir d’un état normal du système. Les techniques proposées constituent une alternative aux techniques de model-checking. En effet, elles mettent en œuvre une recherche symbolique vers l’arrière fondée sur des approches complémentaires : la preuve et la résolution de contraintes. Ce processus de recherche est entièrement automatisé grâce à notre outil GenISIS qui a montré, sur la base d’études de cas disponibles dans la littérature, sa capacité à retrouver des attaques déjà publiées mais aussi des attaques nouvelles
The early detection of potential threats during the modelling phase of a Secure Information System (IS) is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during the system execution. This involves studying the validation of access control rules and performing vulnerabilities automated checks before the IS operationalization. We are particularly interested in detecting vulnerabilities that can be exploited by internal trusted users to commit attacks, called insider attacks, by taking advantage of their legitimate access to the system. To do so, we use formal B specifications which are generated by the B4MSecure platform from UML functional models and a SecureUML modelling of role-based access control rules. Since these vulnerabilities are due to the dynamic evolution of the functional state, we propose to study the reachability of someundesirable states starting from a normal state of the system. The proposed techniques are an alternative to model-checking techniques. Indeed, they implement symbolic backward search algorithm based on complementary approaches: proof and constraint solving. This rich technical background allowed the development of the GenISIS tool which automates our approach and which was successfully experimented on several case studies available in the literature. These experiments showed its capability to extract already published attacks but also new attacks

APA, Harvard, Vancouver, ISO, and other styles

30

Fayolle, Thomas. "Combinaison de méthodes formelles pour la spécification de systèmes industriels." Thesis, Paris Est, 2017. http://www.theses.fr/2017PESC1078/document.

Full text

Abstract:

La spécification d’un système industriel nécessite la collaboration d’un ingénieur connaissant le système à modéliser et d’un ingénieur connaissant le langage de modélisation. L'utilisation d'un langage de spécification graphique, tel que les ASTD (Algebraic State Transition Diagram), permet de faciliter cette collaboration. Dans cette thèse, nous définissons une méthode de spécification graphique et formelle qui combine les ASTD avec les langages Event-B et B. L’ordonnancement des actions de la spécification est décrit par les ASTD et le modèle de données est décrit dans la spécification Event-B. La spécification B permet de vérifier la cohérence du modèle : les événements Event-B doivent pouvoir être exécutés lorsque les transitions associées doivent l’être. Un raffinement combiné des ASTD et d’Event-B permet la spécification incrémental du système. Afin de valider son apport, la méthode de spécification a été utilisée pour la spécification de cas d’études
Specifying industrial systems requires collaboration between an engineer that knows how the system works and an engineer that know the specification language. Graphical specification languages can help this collaboration. In this PhD Thesis a method is defined that combines ASTD (Algebraic State Transition Diagram), a formal graphical notation, with B and Event-B langagues. The ordering of actions is specified using ASTD and the data model is specified using Event-B. B specification is used to verify the consistency of the model : Event-B events have to be executed when the corresponding transitions have to be executed. A combined refinement allows to incrementaly design the system

APA, Harvard, Vancouver, ISO, and other styles

31

Proch, Cyril. "Assistance au développement incrémental et prouvé de systèmes enfouis." Nancy 1, 2006. http://docnum.univ-lorraine.fr/public/SCD_T_2006_0012_PROCH.pdf.

Full text

Abstract:

Les méthodes de développement rigoureuses ne se sont pas encore imposées en électronique. La validation des systèmes se fait par des séries de tests ou par l'utilisation de model checker ne couvrant pas toutes les possibilités. Nous avons élaboré une méthode de développement par la preuve en nous appuyant sur une étude de cas (TV numérique). Le raffinement est central à nos travaux car il permet de conserver la traçabilité et distribue la complexité du système et des preuves. Les modèles construits aident aux choix architecturaux en structurant les tâches du système. Nous avons proposé un mécanisme de traduction de modèles produisant du code SystemC. Le code obtenu sert de support aux expérimentations électroniques. La traduction est prouvée par des modèles B décrivant la sémantique de simulation SystemC. Un programme est représenté par un modèle B, instanciation des modèles de simulation. Nous montrons que l'exécution des programmes traduits conservent les propriétés des modèles
Design process in electronic engineering is not formally defined and developments are based on empirical knowledge. Systems validation is made by tests but these are incomplete and all scenarios or use cases are not tested. We propose a design method built on proof and based on a case study, the RNRT project EQUAST, in the domain of digital television (DVB-T). Our works are based on refinement and its use helps tracability by distributing complexity in steps of refinement. The models help designer in his choices by structuring tasks of the system thanks to invariant properties and refinement. We propose a translation from models to SystemC code; produced code conserves properties of source models and helps to verify electronic constraints. Translation correction is proved by use of B event-based models which explain simulation semantics of SystemC. A specific SystemC program can be represented with a B model. This model is an instanciation of generic models describing SystemC simulation. With the help of refinement, we have shown that simulation of programs conserves properties of abstract models

APA, Harvard, Vancouver, ISO, and other styles

32

Imine, Abdessamad. "Conception Formelle d'Algorithmes de Réplication Optimiste Vers l'Edition Collaborative dans les Réseaux Pair-à-Pair." Nancy 1, 2006. http://www.theses.fr/2006NAN10184.

Full text

Abstract:

Les systèmes d'édition collaborative permettent la manipulation d'objets, comme des documents texte, par plusieurs personnes qui sont réparties dan le temps et dans l'espace. La réplication des objets est indispensable dans de tels systèmes mais elle peut entraîner un problème de divergence de données. Pour pallier ce problème, une approche optimiste, appelée transformation opérationnelle, est utilisée dans ce domaine. L'objectif de cette thèse est de proposer un cadre formel pour la conception d'algorithmes de transformation corrects qui peuvent être déployés sur des systèmes d'édition collaborative en vue de garantir la convergence des données. Dans un premier temps, nous avons proposé une méthodologie formelle pour spécifier et vérifier des objets collaboratifs synchronisés par une transformation opérationnelle. Cette méthodologie repose sur l'utilisation de techniques avancées de déduction automatique. Son exploitation était conséquente puisqu'elle nous a permis de détecter des situations de divergence dans des systèmes collaboratifs bien connus dans la littérature. Assurer La convergence pour des objets linéaires (tels que la liste, le texte, l'arbre ordonné XML, etc) demeure toujours un défi. A ce titre, nous avons constaté que les conditions de convergence connues dans la littérature sont très difficiles à satisfaire. Aussi, nous avons proposé un nouvel algorithme de transformation basé sur une forme relaxée de ces conditions. Comme complément à cet algorithme de transformation, nous avons conçu un environnement d'intégration pour l'édition collaborative basée sur des objets linéaires. L'originalité de cet environnement est le fait qu'il peut être déployé sur un réseaux pair-à-pair (P2P). Enfin, nous avons proposé une technique permettant la composition d'objets simples pour former des objets complexes tout en préservant des critères de convergence imposés sur les algorithmes de transformation
Collaborative editing systems provide computer support for manipulating objects such as a text document, shared by two or more users that are temporally and spatially distributed. Object replication is essential in such systems, but it can leads to a data divergence problem. To overcome this problem, an optimistic approach, called the operational transformation, is used. This thesis is aimed to propose a formal framework for designing correct transformation algorithms that can be embedded in collaborative editing systems for achieving data convergence. Firstly, we have proposed a formal methodology for specifying and verifying collaborative objects synchronized by operational transformation approach. This methodology relies on using advanced automated deduction techniques. Thanks to our formal framework, we have detected divergence situations in many well-known systems. Ensuring convergence for linear objects (such as a list, a text, an ordered XML tree) still remains challenging. In this respect, we have noticed that the known convergence conditions are hardly to be satisfied. So, we have proposed a new tranformation algorithm based on relaxed form of these conditions. Moreover, we have designed an integration environment for collaborative edition based on linear objects. The novelty of this environment is that it can be deployed in peer-to-peer networks (P2P). Lastly, we have proposed a compositional technique enabling construction of complex objects from primitive objects by preserving convergence criterias imposed on transformation algorithms

APA, Harvard, Vancouver, ISO, and other styles

33

Sagaspe, Laurent. "Allocation sûre dans les systèmes aéronautiques : modélisation, vérification et génération." Thesis, Bordeaux 1, 2008. http://www.theses.fr/2008BOR13707/document.

Full text

Abstract:

Les architectures des systèmes embarqués des nouvelles générations d'avions civils et militaires tendent à s'organiser autour d'une plateforme avionique constituée de calculateurs interconnectés par un réseau central. Ce type d'architecture a fait apparaitre le besoin de développer de nouvelles méthodes de conception afin d'assister le dialogue entre les concepteurs des fonctions à embarquer (commandes de vol, gestion de l'énergie, ...) et les architectes de la plateforme avionique. Il est, en particulier, primordial de s'assurer que l'allocation des ressources de la plateforme aux fonctions embarquées respecte les exigences de sûreté de fonctionnement propres aux systèmes avioniques. Dans un premier temps, un cadre général a été proposé pour modéliser et vérifier l'effet de l'allocation des ressources d'une plateforme avionique du point de la sûreté de fonctionnement. Ce cadre est fondé sur l'utilisation du langage AltaRica pour décrire formellement la propagation des défaillances au sein de systèmes embarqués et des outils associés à ce langage (model-checking, génération de séquences et d'arbres de défaillances) pour vérifier la tenue des exigences de sûreté de fonctionnement. Ce cadre a été utilisé pour étudier, d'une part, l'allocation d'équipements informatiques aux fonctions de systèmes embarqués, et d'autre part, les placements des équipements au sein de l'avion en tenant compte de risques tels que l'éclatement d'un pneu ou l'explosion d'un moteur. Dans un second temps, la génération d'allocations respectant les exigences de sûreté de fonctionnement a été étudiée. L'approche retenue est fondée sur l'expression de contraintes d'allocation sous forme d'inégalités linéaires entières et sur l'utilisation de techniques de résolution de ces contraintes. Plusieurs types de contraintes (ségrégation, co-location, exclusion, ...) sont pris en compte. De plus, des critères d'optimisation permettent de guider la résolution des contraintes de façon à proposer des allocations les plus pertinentes du point de vue des besoins des systèmes aéronautiques. Finalement, une approche intégrant les techniques de vérification et de génération a été proposée. La première étape consiste à vérifier un modèle des fonctions embarquées qui est indépendant de la plateforme avionique. Il est possible d'extraire automatiquement des contraintes d'allocation à partir des résultats de cette vérification. L'étape de résolution de contraintes génère alors une allocation sûre. Les travaux sont illustrés par deux études de cas industrielles : une fonction de suivi de terrain d'un avion de chasse et un système de génération et de distribution hydraulique d'un avion de type A320
Abstract

APA, Harvard, Vancouver, ISO, and other styles

34

Doche, Marielle. "Techniques formelles pour l'évaluation de systèmes critiques complexes : test et modularité." École nationale supérieure de l'aéronautique et de l'espace (Toulouse ; 1972-2007), 1999. http://www.theses.fr/1999ESAE0024.

Full text

Abstract:

L'intérêt des méthodes formelles est de permettre le développement rigoureux de systèmes informatiques critiques. Pour des systèmes complexes, elles peuvent être complétées par des formalismes de structuration et de modularité. Nous proposons ici une démarche pour la génération et l'évaluation de jeux de test fonctionnel à partir de spécifications formelles structurées ou modulaires. Nous nous appuyons sur un formalisme de spécification modulaire Moka-TRIO basé d'une part sur la théorie des catégories et le calcul des modèles défini par Ehrig et Mahr (qui permettent de structurer une modélisation et éventuellement d'encapsuler des données) et d'autre part sur la logique temporelle métrique TRIO (pour décrire des comportements réactifs). Des outils associés à ce formalisme permettent de définir et valider une spécification complexe. Nous montrons comment la structure d'une spécification Moka-TRIO permet de mettre en avant différents niveaux d'abstraction pour le test : unitaire, intégration, agrégat et système. Pour chacun de ces niveaux, nous décrivons un mécanisme de génération de jeux de test à partir d'une spécification complexe en s'appuyant sur la sémantique de celle-ci. Enfin, nous reprenons le cadre théorique d'évaluation défini par Bernot, Gaudel et Marre qui détermine la pertinence d'un jeu de test. En étendant la définition d'institution pour prendre en compte des catégories de cas de test, nous montrons comment nos mécanismes de génération permettent de définir des jeux pertinents. L'outil Moka-TRIO implémente les différents mécanismes de génération. L'approche a été appliquée à un système de contrôle de commandes électriques de vol.

APA, Harvard, Vancouver, ISO, and other styles

35

Hunel, Philippe. "Conception et réalisation d'un environnement intégré de génie logiciel pour le développement des protocoles." Clermont-Ferrand 2, 1994. http://www.theses.fr/1994CLF21624.

Full text

Abstract:

Le travail présenté dans cette thèse porte sur l'élaboration d'un environnement pour concevoir, spécifier et implanter des protocoles de communication en utilisant la Technique de Description Formelle (TDF) Estelle. Les différents outils courants d'aide au développement, basés sur Estelle, ne couvrent généralement pas l'ensemble des objectifs des différentes phases d'un développement de protocole. En outre, ils présentent souvent des interfaces utilisateur variés. Cette thèse propose une solution pour intégrer les outils Estelle existants ou à venir dans un environnement ouvert. La première partie présente la modélisation du processus de production du logiciel, puis le modèle de référence OSI, et enfin, selon un cycle de vie en V, les spécificités du processus de développement des logiciels pour les protocoles de communication. La seconde partie expose tout d'abord une synthèse sur l'intégration d'outils (par les données, par le contrôle, par la présentation et par le procédé), en insistant sur les interfaces publiques de structures d'accueil (ATIS, CAIS-A, PCTE), puis l'environnement support EAST, basé sur PCTE, retenu pour réaliser l'intégration d'outils Estelle. La troisième partie propose une modélisation PCTE d'une spécification en Estelle pour qu'elle soit partageable entre différents outils, une méthodologie d'intégration d'outils Estelle dans EAST (expérimenté par l'intégration des outils VEDA et Pet & Dingo), et un modèle d'aide au développement pour les étapes de spécification, validation et implémentation, indépendant des outils Estelle utilisés. Les résultats obtenus permettent d'envisager l'intégration d'outils associés à diverses TDF à partir d'une modélisation PCTE des concepts du modèle OSI.

APA, Harvard, Vancouver, ISO, and other styles

36

Rauzy, Pablo. "Méthodes logicielles formelles pour la sécurité des implémentations de systèmes cryptographiques." Thesis, Paris, ENST, 2015. http://www.theses.fr/2015ENST0039/document.

Full text

Abstract:

Les implémentations cryptographiques sont vulnérables aux attaques physiques, et ont donc besoin d'en être protégées. Bien sûr, des protections défectueuses sont inutiles. L'utilisation des méthodes formelles permet de développer des systèmes tout en garantissant leur conformité à des spécifications données. Le premier objectif de ma thèse, et son aspect novateur, est de montrer que les méthodes formelles peuvent être utilisées pour prouver non seulement les principes des contre-mesures dans le cadre d'un modèle, mais aussi leurs implémentations, étant donné que c'est là que les vulnérabilités physiques sont exploitées. Mon second objectif est la preuve et l'automatisation des techniques de protection elles-même, car l'écriture manuelle de code est sujette à de nombreuses erreurs, particulièrement lorsqu'il s'agit de code de sécurité
Implementations of cryptosystems are vulnerable to physical attacks, and thus need to be protected against them. Of course, malfunctioning protections are useless. Formal methods help to develop systems while assessing their conformity to a rigorous specification. The first goal of my thesis, and its innovative aspect, is to show that formal methods can be used to prove not only the principle of the countermeasures according to a model, but also their implementations, as it is where the physical vulnerabilities are exploited. My second goal is the proof and the automation of the protection techniques themselves, because handwritten security code is error-prone

APA, Harvard, Vancouver, ISO, and other styles

37

Sassolas, Mathieu. "Méthodes qualitatives et quantitatives pour la détection d'information cachée." Paris 6, 2011. http://www.theses.fr/2011PA066581.

Full text

Abstract:

Les systèmes informatiques sont devenus omniprésents et sont utilisés au quotidien pour gérer toujours plus d'information. Ces informations sont de plus en plus souvent confidentielles: informations stratégiques militaires ou financières, données personnelles. La fuite de ces informations peut ainsi avoir des conséquences graves telles que des pertes humaines, financières, des violations de la vie privée ou de l'usurpation d'identité. Les contributions de cette thèse se découpent en trois parties. Tout d'abord, nous étudions le problème de synthèse d'un canal de communication dans un système décrit par un transducteur. Malgré les limites imposées par ce modèle, nous montrons que le problème de synthèse est indécidable en général. Cependant, lorsque le système est fonctionnel, c'est-à-dire que son fonctionnement externe est toujours le même, le problème devient décidable. Nous généralisons ensuite le concept d'opacité aux systèmes probabilistes, en donnant des mesures groupées en deux familles. Lorsque le système est opaque, nous évaluons la robustesse de cette opacité vis-à-vis des informations données par les lois de probabilités du système. Lorsque le système n'est pas opaque, nous évaluons la taille de la faille de sécurité induite par cette non opacité. Enfin, nous étudions le modèle des automates temporisés à interruptions (ITA) où les informations sur l'écoulement du temps sont organisées en niveaux comparables à des niveaux d'accréditation. Nous étudions les propriétés de régularité et de clôture des langages temporisés générés par ces automates et proposons des algorithmes de model-checking pour des fragments de logiques temporelles temporisées.

APA, Harvard, Vancouver, ISO, and other styles

38

Demangeon, Romain. "Terminaison des systèmes concurrents." Lyon, Ecole normale supérieure, 2010. http://www.theses.fr/2010ENSL0595.

Full text

Abstract:

Cette thèse propose une étude de la terminaison dans les systèmes concurrents. La terminaison est une propriété désirable pour les programmes en elle même et comme prérequis pour d'autres propriétés. La cadre du pi calccul est présente dans la section 2. Dans la section 3, des systèmes de types de bases sur le poids sont présentés. Dans la section 4, on montre comment utiliser des approches pour aborder la question de la terminaison des langages concurrents d'ordre supérieur. Dans la section 5, on propose une étude de la complexité du problème de l'inférence pour les analyses basées sur le poids. La section 6 présente brièvement des analyses sémantiques de la terminaison. La section 7 s'intéresse à l'étude de la terminaison d'un pi-calcul impur composé d'un noyau fonctionnel et de constructions impératives. Une nouvelle technique de preuve par élagage est développée. Enfin, on illustre l'efficacité de cette technique en montrant comment elle peut-être appliquée à un lambda calcul avec références
This thesis proposes a study of termination for concurrent languages. Termination is a key-property for concurrent programs. It is useful in itself and as a prerequisite for other properties. The framework of the pi-calculus is presented in section 2. Some existing weight-based type systems as well as new refinments are presented in Section 3. Section 4 is dedicated to results about termination in higher-order concurrent calculi where the [m]essages exchanges are pieces of code. Section 5, we propose a study of the complexity of the inference problem for the weight-based type systems. In section 6, termination techniques based on logical relations are presented. Section 7 contained results about the termination of an impure pi-calculus where a functional core is distinguished from the imperative constructs. A new pruning technique is used for the soundness proof. A last chapter illustrates the efficiency of this new method by ensuring terrmination in a impure lambda-calculi

APA, Harvard, Vancouver, ISO, and other styles

39

Chauvel, Franck. "Méthodes et outils pour la conception de systèmes logiciels auto-adaptatifs." Phd thesis, Université de Bretagne Sud, 2008. http://tel.archives-ouvertes.fr/tel-00512189.

Full text

Abstract:

Because of the increasing need of mobiles devices, most of software systems need to take into account a highly dynamic environment including hardware and software resources. This need for self-adaptation arises in both large-scale systems such as peer-to-peer systems and small-scale systems such as embedded systems. Those systems, so called ``self-adaptive systems'', have to observe the changes which occur in their environment in order to maximize the quality of the services they provide. ``Observation, Decision, Action'' have thus become the three basic capabilities of self-adaptive systems. They observe the environment in order to decide on what and when the system's architecture must be modified. The design and the development of such systems is a crossroad between three research fields in Computer Science: Software Engineering, Artificial Intelligence, and Distributed Systems. First, Software Engineering and especially Dynamic Architectures enable the definition of software systems as assemblies of well-defined software components. Then, Artificial Intelligence enables the automation of the decision process. Finally, the Distributed Systems and specially Context-Aware Systems focus on the collection and the aggregation of environmental information. However, the design and the development of self-adaptive systems are still hand-written and error prone tasks because of a lack of devoted tools and methodologies. Although most recent middleware platforms enable the dynamic updating of component-based systems, the underlying adaptation mechanisms are still too technical to fit the abstraction level needed by the system architect. Most platforms keep providing API or, at best, some low-level and platform dependant scripts. Good practices in software engineering (such as, design methods, validation tools, etc) are thus not applied to the self-adaptation concerns. The contribution of this thesis is to help the system architect by providing the tools and the methods he needs to describe self-adaptation concerns at the appropriate abstraction level. Self-adaptation behaviours are described as rules expressed in a pseudo natural language which avoid the quantification of environment properties. The system architect can define his own terminologies to portray the environment. The semantics of those rules are based on fuzzy logic and enable a direct interpretation and, therefore, the simulation, at design-time, of self-adaptive systems. Such a simulation at design time is a first validation which reduces the risk of conflicts between the architectural choices and the adaptation requirements. Such conflicts lead to expensive roll-backs in the design process. The TanGraM tool supports the definition of self-adaptive architectures, including the structure, the behaviour, and the manipulated data. It supports as well the integration and the simulation of qualitative adaptation policies at design time. An extension of the Fractal platform has also been released and enables the direct reuse of those adaptation policies in a real Fractal system. We use those tools to design and deploy a self-adaptive HTTP server which has been used as a case study. It adapts its architecture according to the average load and density of HTTP requests. However, the description of qualitative adaptation policies is a first step towards a reliable design process for self-adaptive systems.

APA, Harvard, Vancouver, ISO, and other styles

40

Masson, Lola. "Safety monitoring for autonomous systems : interactive elicitation of safety rules." Thesis, Toulouse 3, 2019. http://www.theses.fr/2019TOU30220.

Full text

Abstract:

Un moniteur de sécurité actif est un mécanisme indépendant qui est responsable de maintenir le système dans un état sûr, en cas de situation dangereuse. Il dispose d'observations (capteurs) et d'interventions (actionneurs). Des règles de sécurité sont synthétisées, à partir des résultats d'une analyse de risques, grâce à l'outil SMOF (Safety MOnitoring Framework), afin d'identifier quelles interventions appliquer quand une observation atteint une valeur dangereuse. Les règles de sécurité respectent une propriété de sécurité (le système reste das un état sûr) ainsi que des propriétés de permissivité, qui assurent que le système peut toujours effectuer ses tâches. Ce travail se concentre sur la résolution de cas où la synthèse échoue à retourner un ensemble de règles sûres et permissives. Pour assister l'utilisateur dans ces cas, trois nouvelles fonctionnalités sont introduites et développées. La première adresse le diagnostique des raisons pour lesquelles une règle échoue à respecter les exigences de permissivité. La deuxième suggère des interventions de sécurité candidates à injecter dans le processus de synthèse. La troisième permet l'adaptation des exigences de permissivités à un ensemble de tâches essentielles à préserver. L'utilisation des ces trois fonctionnalités est discutée et illustrée sur deux cas d'étude industriels, un robot industriel de KUKA et un robot de maintenance de Sterela
An active safety monitor is an independent mechanism that is responsible for keeping the system in a safe state, should a hazardous situation occur. Is has observations (sensors) and interventions (actuators). Safety rules are synthesized from the results of the hazard analysis, using the tool SMOF (Safety MOnitoring Framework), in order to identify which interventions to apply for dangerous observations values. The safety rules enforce a safety property (the system remains in a safe state) and some permissiveness properties, ensuring that the system can still perform its tasks. This work focuses on solving cases where the synthesis fails to return a set of safe and permissive rules. To assist the user in these cases, three new features are introduced and developed. The first one addresses the diagnosis of why the rules fail to fulfill a permissiveness requirement. The second one suggests candidate safety interventions to inject into the synthesis process. The third one allows the tuning of the permissiveness requirements based on a set of essential functionalities to maintain. The use of these features is discussed and illustrated on two industrial case studies, a manufacturing robot from KUKA and a maintenance robot from Sterela

APA, Harvard, Vancouver, ISO, and other styles

41

Bonnefoi, Fabien. "Vérification formelle des spécifications de systèmes complexes par réseaux de Petri : application aux systèmes de transport intelligents." Paris 6, 2010. http://www.theses.fr/2010PA066616.

Full text

APA, Harvard, Vancouver, ISO, and other styles

42

Tchuenkam, Tchoneng Honoré. "Techniques formelles pour le développement de systèmes de conduite de procédés manufacturiers : abstraction, spécification, synthèse et optimisation." Nancy 1, 1991. http://www.theses.fr/1991NAN10413.

Full text

Abstract:

Nous utilisons des techniques classiques d'abstraction, de spécification et de synthèse de programmes pour proposer une démarche de développement formel de systèmes temps réels dans le cadre (restreint) de la conduite des processus de productions discrètes. Dans le type de problème que nous avons à traiter, on dispose d'une installation industrielle dont les composants assurent des fonctions élémentaires de transformation, d'assemblage et de manutention de produits. Ces composants peuvent être mis en marche par des actionneurs et des capteurs fournissent des renseignements sur l'état du système et des produits. On souhaite construire un logiciel qui pilote l'installation existante pour obtenir un système global ayant certaines fonctionnalités. Nous préconisons une démarche qui consiste à:―faire une description abstraite et formelle de l'installation existante sans préjuger de son utilisation future, en combinant le formalisme des types abstraits et une extension temps réelle de la logique temporelle;―spécifier formellement le résultat attendu de son fonctionnement en indiquant essentiellement la relation qui existe entre les produits fabriqués et ceux de base. A partir des éléments précédents, nous synthétisons des programmes séquentiels de commande de l'installation donnée. Nous optimisons ensuite ces programmes en essayant de les paralléliser au maximum.

APA, Harvard, Vancouver, ISO, and other styles

43

Darlot, Christophe. "Reformulation et vérification de propriétés temporelles dans le cadre du raffinement de systèmes d'évènements." Besançon, 2002. http://www.theses.fr/2002BESA2054.

Full text

Abstract:

Les travaux présentés se placent dans le contexte de la vérification de propriétés temporelles sur des systèmes d'événements spécifiés par raffinement. Notre démarche se décompose en quatre étapes : 1-Nous vérifions une propriété abstraite par model-checking; 2- Nous raffinons le système et vérifions ce raffinement ; 3- Nous raffinons la propriété abstraite en une propriété dite reformulée; 4- Nous vérifions la propriété reformulée. L'apport de ces travaux est d'une part de permettre à l'utilisateur de raffiner les propriétés pour tenir compte des détails introduits lors du raffinement, d'autre part de diminuer l'effort de vérification en combinant preuve et model-checking. Ce travail, basé sur une définition de raffinement entre structures de Kripke étiquetées, nous a conduit a prouver la préservation des propriétés PLTL par raffinement et la correction de la démarche de vérification pour un ensemble de schémas de reformulation. Notre technique est implantée dans un prototype utilisant le prouveur PVS
We are interested in verifying temporal properties in event systems specified by refinement. We adopt a four-step method : 1- We verify an abstract property by model-checking; 2- We refine the system and verify the refinement; 3- We refine the abstract property into a reformulated property; 4- We verify the reformulated property; The main interest is in one hand to have the abstract properties refined by the specifier to take into account the details introduced during refinement, on the other hand to decrease the verification effort by combining proof and model-checking. This work, based on a refinement definition between labelled Kripke structures lead us to prove the preservation of PLTL properties through refinement and the correctness of the verification method for a set of reformulation patterns. This work is implemented in a prototype using the PVS prover

APA, Harvard, Vancouver, ISO, and other styles

44

Gervais, Frédéric. "Combinaison de spécifications formelles pour la modélisation des systèmes d'information." Phd thesis, Conservatoire national des arts et metiers - CNAM, 2006. http://tel.archives-ouvertes.fr/tel-00121006.

Full text

Abstract:

L'objectif de cette thèse est de profiter des avantages de deux formes de modélisation complémentaires pour représenter de manière formelle les systèmes d'information (SI). Un SI est un système informatisé qui permet de rassembler les informations d'une organisation et qui fournit des opérations pour les manipuler. Les SI considérés sont développés autour de systèmes de gestion de bases de données (SGBD). Notre motivation est d'utiliser des notations et des techniques formelles pour les concevoir, contrairement aux méthodes actuelles qui sont au mieux semi-formelles. D'une part, EB3 est un langage formel basé sur les traces d'événements qui a été défini pour la spécification des SI. En particulier, EB3 met en avant le comportement dynamique du système. D'autre part, B est un langage formel basé sur les états qui se prête bien à la spécification des propriétés statiques des SI. Nous avons défini une nouvelle approche, appelée EB4, qui bénéficie à la fois des avantages d'EB3 et B. Dans un premier temps, les processus décrits en EB3 sont utilisés pour représenter et pour valider le comportement du système. Ensuite, la spécification est traduite en B pour spécifier et vérifier les principales propriétés statiques du SI. Enfin, nous avons défini des techniques de synthèse automatique de transactions BD relationnelles à partir du modèle de données d'EB3 pour compléter le cycle de développement du SI.

APA, Harvard, Vancouver, ISO, and other styles

45

Hachicha, Rim. "Modélisation et analyse de la flexibilité dans les systèmes workflow." Paris, CNAM, 2007. http://www.theses.fr/2007CNAM0565.

Full text

Abstract:

Cette thèse est consacrée à la modélisation formelle et la gestion des systèmes workflows. Nous nous intéressons à apporter une solution à l'un des principaux problèmes des systèmes workflows est celui de la flexibilité : les modèles aussi bien que les systèmes actuels ne sont pas suffisamment flexibles et adaptables. Dans ce but, nous proposons un modèle de tâches et d'acteurs précisant les relations formelles entre les tâches workflow et les acteurs et permettant une assignation flexible des acteurs ux activités workflow. L'allocation des tâches workflows est fondée sur le concept de distance acteur/tâche et sur le processus de formation de coalitions d'agents. Le modèle permet de vérifier l'interchangeabilité des acteurs et la cohérence des tâches workflows suite à l'évolution de l'environnement. Nous proposons une architecture orientée agent distribuée intégrant le modèle formel et permettant de réaliser les fonctionnalités requises par les systèmes workflows. Cette architecture est capable de s'adapter de façon réactive aux changements tout en assurant la réutilisabilité du système Workflow. Nous avons implémenté le modèle sur la plate forme JADE en utilisant le système expert JESS et nous l'avons validé sur une réelle application
This thesis is devoted to formal modeling and management of workflow system. We are interested to bring a solution to the one of the principal problems of workflow systems is that of flexibility : the models as well as the current systems are not sufficiently flexible and adaptable. For these requirements, we propose a task model and actor model specifying the formal relations between workflow tasks and actors and allowing a flexible assignment of actors to workflow activities. The workflow task allocation is based on the concept of actor/task distance and agent coalition formation process. The model allows checking the interchangeability of the actors and the coherence of the workflows tasks following the evolution of the environment. We propose a distributed agent architecture integrating the formal model and permitting to carry out the functionalities required by the workflow system. This architecture is adaptable, reactive and ensures the reusability of the workflow system. We implemented the proposed model on JADE agent platform using expert system JESS and we validated our model on a real application

APA, Harvard, Vancouver, ISO, and other styles

46

Belguidoum, Meriem. "Conception d'une infrastructure pour un déploiement sûr et flexible des composants logiciels." Télécom Bretagne, 2008. http://www.theses.fr/2008TELB0060.

Full text

Abstract:

Le déploiement de logiciels est une tâche complexe car elle nécessite la réalisation de nombreuses actions ayant de fortes contraintes de dépendance. Il recouvre toutes les activités qui composent le cycle de vie du logiciel depuis son développement jusqu’à son utilisation. Dans le cadre de ce travail, nous nous intéressons aux activités d’installation, de désinstallation et de mise à jour. En parallèle, les applications deviennent de plus en plus complexes, ce qui provoque une explosion de leur taille. Pour faciliter leur gestion et leur réutilisation, elles sont représentées par des collections de composants qui sont partagés entre plusieurs applications. Ainsi, une opération de déploiement concernant une application aura un effet sur toutes les applications qui l’utilisent. Une telle opération, nécessite la connaissance préalable de l’architecture sur laquelle repose les applications avec toutes leurs dépendances. Les approches de gestion du déploiement actuelles sont souvent ad-hoc et se basent sur l’intervention d’experts pour résoudre les problèmes et mener à bien le déploiement. De plus, il n’existe pas de moyens efficaces pour garantir le bon déroulement du déploiement. Il est donc crutial de changer ces approches en des approches plus structurées, plus flexibles et plus sûres afin de maîtriser et de vérifier le déploiement. Pour cela, nous proposons un méta-modèle générique pour le déploiement automatique des composants ainsi qu’un système formel pour vérifier et garantir le bon déroulement du déploiement. Le méta-modèle permet d’abstraire tous les concepts nécessaires au déploiement ainsi, il peut être réutilisable dans plusieurs contextes. Le système formel est une formalisation mathématique du modèle générique. Il permet de démontrer et de prouver la réussite (le bon déroulement) et la sûreté (maintien de la cohérence du système) des opérations de déploiement. Enfin, nous proposons un système formel intégrant les propriétés non fonctionnelles (version, niveau de sécurité, performance, etc. ) dans la gestion du déploiement. L’intérêt est de pouvoir prendre en compte plusieurs instances d’un même composant ou d’un même service selon la plate-forme visée afin de personnaliser le déploiement
Software deployment is a complex task because it requires numerous dependent actions to be carried out. It covers all the activities of the software life cycle from its development to its use. In this work, we are interested in the installation, deinstallation and update activities. At the same time, applications are becoming more complex, causing an explosion in their size. To facilitate their management and reuse, they are represented as collections of components that are shared between several applications. Thus, deploying an application will affect all the applications that use it. Such an operation requires prior knowledge of the architecture of the applications with all their dependencies. The current approaches for managing deployment are often ad hoc and necessitate the intervention of experts to solve problems and carry out the deployment. Moreover, there is no way to guarantee the correctness of the deployment operation. Therefore, it is necessary to change to more structured, flexible and reliable approaches to be able to verify the deployment. Hence, we propose a generic meta-model for automatic component deployment and a formal system to check and ensure correct deployment. The metamodel represents the main deployment concepts so it can be re-used in several contexts. The formal system represents the mathematical description of the generic model. It allows the success and safety (maintaining consistency of the system) of the deployment operations to be demonstrated and proved. Finally, we propose a formal system which integrates the non-functional properties (version, level of security, performance, etc. ) in managing the deployment. The interest of these properties is that they can take into account multiple instances of the same component or the same service in order to personalize deployment, depending on the target system

APA, Harvard, Vancouver, ISO, and other styles

47

Mammar, Amel. "Un environnement formel pour le développement d'applications bases de données." Paris, CNAM, 2002. http://www.theses.fr/2002CNAM0437.

Full text

Abstract:

Ce travail présente une approche formelle pour le développement d'applications bases de données sûres. Cette approche consiste en la génération d'une implémentation relationnelle à partir de spécifications formelles. On décrit préalablement l'application à l'aide de notations UML, puis un processus automatique est appliqué afin de les traduire en spécifications B. En utilisant le processus de raffinement, un ensemble de règles de raffinement; opérant sur les données et les opérations, est utilisé sur les spécifications obtenues. Ces phases de raffinement ont pour but de rendre les spécifications proches du langage d'implémentation cible choisi, la dernière phase de codage devient intuitive et naturelle. De manière générale, le raffinement est manuel, relativement coûteux, en particulier en phase de preuve. Grâce au caractère générique de ces règles de raffinement, un outil de raffinement assisté peut être réalisé, permettant la réduction du côut du processus de raffinement
This work presents a formal approach for developing safety database applications. This approach consists of generating relational database implementations from formal specifications. We begin by designing the application with graphical notations such as UML, OMT,. . . Then an automatic process is used to translate them into B formal specifications. Using the B refinement process, a set of refinement rules, acting on both data and operations (programs), are applied on the specifications. These refinement process is generally a manuel and very costy task especially in proff phase. Thanks to the generic feauture of the refinement rules, an assistant refiner can be elaborated, allowing the cost of the refienement process to be reduced

APA, Harvard, Vancouver, ISO, and other styles

48

Colange, Maximilien. "Symmetry reduction and symbolic data structures for model-checking of distributed systems." Paris 6, 2013. http://www.theses.fr/2013PA066724.

Full text

Abstract:

Les systèmes répartis deviennent omniprésents au quotidien, en particulier dans des domaines critiques, requérant une forte garantie de fiabilité. Les approches basées sur le test sont intrinsèquement non-exhaustives, rendant nécessaire l’usage de méthodes formelles. Parmi elles, nous nous concentrons sur le model-checking, qui explore tous les comportements d’un système pour s’assurer que sa spécification est respectée. Mais cette approche se heurte à l’explosion combinatoire : le nombre d’états d’un système réparticroît exponentiellement avec son nombre de composants. Nous retenons deux des nombreuses solutions à ce problème :- les symétries pour identifier des comportements similaires : ils partagent des propriétés communes, ce qui réduit le nombre d’états à explorer. - des structures de données compactes, comme les diagrammes de décision (DD), pour réduire l’empreinte mémoire de l’exploration. Nous proposons trois principales contributions :- La réduction par symétries et les DD sont théoriquement orthogonaux, mais se combinent mal en pratique, car l’efficacité des DD repose sur l’emploi d’algorithmes dédiés. Nous proposons un nouvel algorithme pour appliquer la réduction par symétries sur des DD, et démontrons son efficacité pratique. - Classiquement, les opérations sur les DD sont encodées après un pré-calcul de toutes les entrées possibles. Nous offrons un nouveau mécanisme de manipulation des DD, entièrement symbolique, qui évite un tel pré-calcul. Nous démontrons son efficacité pour encoder une relation de transition. - Nous montrons comment ces deux contributions peuvent être appliquées à un formalisme déjà existant, les Symmetric Nets with Bags
Distributed systems are becoming omnipresent in our daily life, especially in critical domains, thus requiring a strong guarantee of reliability. Approaches like testing are inherently not exhaustive, so that formal methods are needed. Among those, we focus on model-checking, that consists in exploring exhaustively all the behaviors of a system to ensure that the specification is enforced. However, this approach faces the “combinatorial explosion” problem: the number behaviors of a distributed system increases exponentially with its number of components. To tackle this explosion, several approaches have been proposed. We focus on two of them:- symmetries to identify similar behaviors: they share similar properties, thus allowing to reduce the number of behaviors to explore;- symbolic compact data structures, namely decision diagrams (DD), to reduce the memory footprint of the explored behaviors. We propose three main contributions:- Symmetry reduction and DD are theoretically orthogonal techniques, but are not known to combine well in practice, because efficiency of DD heavily relies on the use of dedicated algorithms. We propose a novel algorithm to use symmetry reduction on DD, and demonstrate experimentally its efficiency. - Classical operations on DD are encoded using a pre-computation of all possible inputs. We offer a new mechanism of manipulation of DD, fully symbolic, that avoids such a pre-computation. We demonstrate its efficiency to encode a transition relation, and to improve our symmetry reduction algorithm- We show how to use the two previous contributions to model-check an existing class of models, the Symmetric Nets with Bags

APA, Harvard, Vancouver, ISO, and other styles

49

Jaeger, Éric. "Study of the benefits of using deductive formal methods for secure developments." Paris 6, 2010. http://www.theses.fr/2010PA066048.

Full text

Abstract:

La mise en oeuvre des méthodes formelles déductives lors du développement de systèmes permet d'obtenir des garanties mathématiques quant à leur validité. Pour cette raison, leur utilisation est recommandée ou exigée par certains standards relatifs à la sûreté de fonctionnement ou la sécurité. Il reste cependant légitime de s'interroger sur la portée exacte des bénéfices. Certains aspects d'un système peuvent échapper à la formalisation, et il n'est pas toujours facile d'identifier ces limitations ou leurs conséquences. De même, si la validité d'une preuve est difficilement contestable, son utilisation pour justifier d'une confiance réelle dans le système physique n'est pas toujours admise. De telles questions sont particulièrement pertinentes dans le domaine de la sécurité, lorsque les systèmes font l'objet d'attaques de la part d'agents intelligents ; par rapport à la sûreté, il y a un changement radical de point de vue, qui justifie de s'interroger quant à l'application de principes ou de pratiques bien connus. Nous identifions les bénéfices et évaluons la confiance résultant de l'application des méthodes formelles déductives lors de développements de systèmes de sécurité. Cette analyse aborde les éventuelles difficultés, déviations ou problèmes qui peuvent être rencontrés, et les illustre par des exemples. Elle comporte également une étude détaillée du concept de raffinement, et présente un plongement profond visant à valider la logique de la méthode B; ce plongement conduit par ailleurs à l'étude des représentations à la de Bruijn.

APA, Harvard, Vancouver, ISO, and other styles

50

Collé, Frédéric. "Un modèle de conception centré interaction : formalisation et application à la conception de systèmes complexes." La Rochelle, 2006. http://www.theses.fr/2006LAROS168.

Full text

Abstract:

Nous nous intéressons à représenter, analyser et mettre en oeuvre le comportement dans des systèmes complexes (tels que des environnements de réalité augmentée), mobiles et évolutifs. Le travail effectué se situe dans une approche globale d’un outil d’aide à la conception de systèmes interactifs, i. E. Des systèmes s’appuyant sur une interaction forte avec un composant de visualisation. Pour ce faire, une approche de modélisation et de conception orientée agent est retenue. Plus particulièrement, nos travaux nous ont conduit à nous intéresser au développement d’un modèle et d’une méthode de conception centré interaction ainsi qu’à la formalisation de l'interactivité par analyse de scénarios. Classiquement les méthodologies de conception de systèmes multi agent mettent en évidence la notion de rôle des agents. Nous pensons qu’un rôle est relatif à une interaction et ainsi centrons la conception sur les points de vues que représentent les interactions. L’approche développée s’appuie sur une représentation formelle des agents fondée sur le modèle des Ambients. Cette approche nous permet de mettre en avant des solutions architecturales. Parallèlement, la prise en compte de l’utilisateur final ou d’un utilisateur expert dans le cadre du développement de systèmes interactifs nous a conduit à définir une formalisation de scénarios. Cette formalisation réalisée en Logique Linéaire permet en particulier d’analyser les besoins utilisateurs et de mettre en évidence des propriétés de ces scénarios. Cela nous permet de disposer d’un langage de commande dans lequel des simulations peuvent être exprimées. Une application est menée pour l’aide à la conception de systèmes de trafic urbain
We are interested in representing, analyzing and implementing some behaviours in complex systems (such as augmented reality environments) which are mobile and scalable. Our work is carried out in an approach which leads to an helping tool for the design of interactive systems, i. E systems which are based on a strong interaction with a component of visualization. So, an agent oriented approach is adopted in order to model and to design such systems. More particularly, our work led us on the one hand to develop a model and a design method which are focused on the concept of interaction and on the other hand to formalize the interactivity by means of a scenario analysis. Usually, multi-agent system design methodologies highlight the concept of role the agents have to play. We think that a role is related to an interaction and thus we focus the design phase on the viewpoints that the interactions represent. Our developed approach is based on a formal representation of the agents using the Ambient calculus. This approach underlines several architectural solutions. At the same time, we want to consider the end-user or an expert user during the interactive system development. So, we were led to define a formalization of scenarios. This formalization in Linear Logic allows us to analyze user needs and to check some properties of these scenarios. So, we have a language of control that can express simulation processes. An application is carried out in the case of the design of urban traffic systems

APA, Harvard, Vancouver, ISO, and other styles

Dissertations / Theses on the topic 'Systèmes, Conception de – Méthodes formelles (informatique)'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles