To see the other types of publications on this topic, follow the link: Méthode de spécification formelle.
Dissertations / Theses on the topic 'Méthode de spécification formelle'
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the top 50 dissertations / theses for your research on the topic 'Méthode de spécification formelle.'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Browse dissertations / theses on a wide variety of disciplines and organise your bibliography correctly.
1
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 textAbstract:
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é<br>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
2
Loubersac, Jérôme. "Définition d'une méthodologie pour le langage de spécification formelle VDM." Paris 9, 1994. https://portail.bu.dauphine.fr/fileviewer/index.php?doc=1994PA090025.
Full textAbstract:
La généralisation de l'utilisation de méthodes formelles telles que VDM se heurte aujourd'hui principalement à trois obstacles: leur carence en méthodologie, l'hermétisme de leurs notations, et la résistance des utilisateurs potentiels face à un changement aussi radical de méthode. L'objectif de ce travail était de contribuer à lever ces trois obstacles. Pour cela, nous avons défini une approche originale de spécification basée sur des diagrammes possédant une sémantique formelle et pouvant être traduits en VDM, et nous avons proposé des techniques pour le raffinement des spécifications VDM. Ceci permettait de répondre aux besoins méthodologiques tout en éliminant l'hermétisme du langage. Puis nous avons défini une utilisation nouvelle de VDM dans le domaine de la refonte (re-engineering), permettant d'approcher une audience plus réceptive et de rendre VDM plus convaincante. (VDM est l'acronyme de Vienna Development Method)
3
Barros, Tomás. "Spécification et vérification formelles des systèmes de composants répartis." Phd thesis, Université de Nice Sophia-Antipolis, 2005. http://tel.archives-ouvertes.fr/tel-00090718.
Full textAbstract:
Un composant est une entité autonome qui interagit avec son environnement par des interfaces correctement spécifiées. Fractive est une implantation du modèle de composants Fractal qui propose des primitives de haut niveau et une sémantique pour la programmation à base de composants Java distribués, asynchrones et hiérarchiques. Fractive propose également une séparation entre aspects fonctionnels et non-fonctionnels, ces derniers permettant un contrôle de l´exécution d´un composant et de son évolution dynamique. Dans cette thèse, nous proposons un outillage formel pour la vérification d´applications construites avec Fractive. Cela permet de vérifier que chaque composant remplit correctement le rôle qui lui a été assigné au sein du système, et que la mise à jour ou le remplacement d´un composant n´engendre pas d´interblocage ou de panne du système. Nous avons défini un nouveau format intermédiaire qui étend les réseaux d´automates communicants, en paramétrisant leurs événements de communication et de traitement. Nous avons ensuite utilisé ce format intermédiaire pour définir les spécifications comportementales d´applications Fractive. Nous considérons que les modèles des composants primitifs sont connus (donnés par l´utilisateur ou par analyse statique). En utilisant la description des composants, nous construisons un contrôleur décrivant le comportement non fonctionnel du composant. La sémantique d´un composant est ensuite générée comme le produit de synchronisation des LTSs de ses sous-composants et du contrôleur. Le système résultant peut être vérifié par rapport aux besoins exprimés dans un ensemble de formules de logique temporelle, comme illustré dans le manuscrit.
4
Lopez, Nestor. "Spécification formelle de systèmes complexes : méthodes et techniques." Paris, CNAM, 2002. http://www.theses.fr/2001CNAM0410.
Full textAbstract:
Nous proposons une methodologie de specification et de construction de systemes qui transforme la specification evenementielle d'un systeme en une specification pre-post, ce qui permet d'effectuer le processus de developpement a l'aide de techniques connues de derivation de programmes par raffinements et sans rompre le processus de raisonnement formel. Le role de la specification evenementielle est de decrire les interactions du systeme avec son environnement. Le resultat de la transformation est un module qui fournit les moyens de communication du systeme. Pour prendre en compte les aspects concurrents et distribues d'un systeme, nous proposons la notion de module partage. Nous utilisons des variables auxiliaires, non implantees, pour exprimer des proprietes abstraites et pour faire la preuve de correction des implantations effectuees. Pour repondre au besoin de reutilisation de modules existants, nous proposons une technique pour completer une specification a l'aide de variables auxiliaires afin de l'adapter a la solution de problemes particuliers, tout en preservant l'implantation fournie initialement.
5
De, Almeida Pereira Dalay Israel. "Analyse et spécification formelle des systèmes d’enclenchement ferroviaire basés sur les relais." Thesis, Ecole centrale de Lille, 2020. http://www.theses.fr/2020ECLI0009.
Full textAbstract:
Les Systèmes d'Enclenchement Ferroviaire (SEF) basés sur des relais sont des systèmes critiques, ils doivent être spécifiés et leur sécurité doit être prouvée afin de garantir l'absence de dangers lors de leurs exécutions. Toutefois, il s'agit d'une tâche difficile, car les SEF à relais ne sont généralement modélisés que de manière structurelle, de sorte que leur analyse comportementale est effectuée manuellement sur la base des connaissances des experts sur le système. Cependant, l'existence d'une description formelle du comportement des SEF est impérative pour pouvoir effectuer des preuves de sécurité. En outre, comme les SEF informatisés ont tendance à être moins chers, plus faciles à entretenir et à faire évoluer, le secteur ferroviaire a intérêt à ce qu'il existe une méthodologie pour transformer des SEF à relais existants en SEF informatisés.Les méthodologies formelles de spécification sont fondées sur des bases mathématiques solides qui permettent de prouver la sécurité des systèmes. En outre, de nombreux langages de spécification formelle prennent en charge non seulement la vérification, mais aussi la mise en œuvre de ces systèmes par un processus de développement formalisé. Ainsi, les méthodes formelles peuvent être la clé pour prouver la sécurité des SEF et les mettre en œuvre en utilisant des technologies informatiques.Cette thèse aborde deux propositions principales. Premièrement, elle présente une analyse des informations des diagrammes à relais et de la formalisation de la structure et du comportement des SEF basés sur des expressions mathématiques afin de créer un certain niveau de formalisation des systèmes. Le modèle résultant peut être étendu et adapté afin de se conformer à différents contextes ferroviaires et il peut aussi être utilisé afin de soutenir la spécification de ces systèmes dans différents langages de spécification formels. Ensuite, cette thèse présente comment le modèle formel des SEF peut être adapté afin de spécifier formellement ces systèmes selon la méthode B, un langage de spécification formel qui a déjà été utilisé avec succès dans le domaine ferroviaire et qui permet de prouver la sécurité du système et de le mettre en œuvre en tant que système informatique.En définitive, cette thèse présente une méthodologie complète pour la spécification et la vérification des Systèmes d'Enclenchement Ferroviaire basés sur des relais, en fournissant un support pour la preuve des systèmes dans différents contextes et pour leur spécification et leur mise en œuvre dans de nombreux langages formels différents<br>Relay-based Railway Interlocking Systems (RIS) are critical systems and must be specified and safety proved in order to guarantee the absence of hazards during their execution. However, this is a challenging task, since Relay-based RIS are generally only structurally modelled in a way that their behavioural analysis are made manually based on the experts knowledge about the system. Thus, the existence of a RIS behavioural formal description is imperative in order to be able to perform safety proofs. Furthermore, as Computer-based RIS tend to be less expensive, more maintainable and extendable, the industry has interest in the existence of a methodology for transforming the existing Relay-based RIS into Computer-based RIS.Formal specification methodologies are grounded in strong mathematical foundations that allow the systems safety proof. Besides, many formal specification languages support not only the verification, but also the implementation of these systems through a formal development process. Thus, Formal Methods may be the key in order to prove the RIS safety and implement them with computer-based technologies.This thesis addresses two main propositions. Firstly, it presents an analysis of the relay diagrams information and a formalisation of the Relay-based RIS structure and behaviour based on mathematical expressions as a way to create a certain level of formalisation of the systems. The resulting model can be extended and adapted in order to conform to different railway contexts and it can be used in order to support the specification of these systems in different formal specification languages. Then, this thesis presents how the RIS formal model can be adapted in order to formally specify these systems in B-method, a formal specification language with a successful history in the railway field and which allows the system safety proof and implementation as computer-based systems.As a result, this thesis presents a complete methodology for the specification and verification of Relay-based Railway Interlocking Systems, giving support for the systems safety proof in different contexts and for their specification and implementation in many different formal languages
6
Mrhailaf, Rachid. "Vers une reformulation de la spécification dans la commande des systèmes de production : approches multi-formalismes." Toulouse 3, 1997. http://www.theses.fr/1997TOU30124.
Full textAbstract:
La spécification complète de la conduite des systèmes de production nécessite différents approches et formalismes afin de tenir compte de ses différents aspects (système hétérogène). Couvrir tous les aspects d'un système hétérogène est ramené au problème d'intégration de différentes méthodes sous une approche globale d'analyse et de décomposition (approche multi-formalismes). Deux cas de systèmes hétérogènes ont été étudiés. Le premier cas est celui d'un système réactif et transformationnel ou nous avons proposé l'intégration des méthodes SA/RT et SC sous une approche fonctionnelle globale. Le deuxième cas concerne les systèmes comportant, en plus des sous-systèmes réactifs et transformationnels, des sous-systèmes d'information. Pour ce type de systèmes, nous avons proposé l'intégration des méthodes SA/RT, SC, MI et OMT sous une approche globale basée sur le concept de domaine et d'objet domaine. Afin d'intégrer des méthodes formelles (VDM) dans le cycle de developpement d'un système, Nous avons proposé une démarche de passage d'un modèle semi-formel à un modèle formel. Cette démarche s'applique aussi bien dans le cas d'un développement fonctionnel que d'un développement orienté objet. Il a été étudié en particulier le passage d'un modèle semi-formel SA-RT à un modèle formel VDM. Les différentes approches sont illustrées à travers des études de cas sur un exemple de cellule d'usinage.
7
Nasr, Odile. "Spécification et vérification des ordonnanceurs temps réel en B." Toulouse 3, 2007. http://thesesups.ups-tlse.fr/58/.
Full textAbstract:
L'objectif de cette thèse est de proposer une démarche de spécification et de validation des ordonnanceurs temps réel. Le modèle à analyser et les politiques d'ordonnancement sont exprimés à l'aide du langage Cotre. Ce dernier peut être considéré comme un langage de description d'architecture permettant la description formelle du comportement d'un système, ainsi que les contraintes à respecter. La vérification du système ordonnancé repose sur la traduction du modèle en automates temporisés. Notre modélisation des ordonnanceurs préemptifs devant être traduite en Uppaal, ne doit gérer le temps qu'à travers des horloges. Nous cherchons ensuite à valider notre modélisation en utilisant la méthode B. Pour cela, nous avons débuté par une spécification abstraite des ordonnanceurs, et nous l'avons raffiné par étapes successives afin de prendre en compte les caractéristiques des automates temporisés. Nous avons ensuite vérifié la hiérarchie des raffinements en prouvant les différentes obligations de preuve générées. Afin de traduire la modélisation B des ordonnanceurs en Uppaal, nous avons défini un langage B0_Uppaal et des règles à respecter lors de la transformation. Cette traduction est enfin vérifiée par des propriétés d'ordonnançabilité exprimées en logique CTL<br>The purpose of this thesis is to propose a methodology for specifying and verifying of real time schedulers. The model to be analyzed and the scheduling policies are expressed using the Cotre language. This one can be considered as an architecture description language allowing the formal description of the system's behavior, as well as the constraints to be respected. The verification of the scheduled system relies on the translation of the model to timed automata. Our modeling of the preemptive schedulers to be translated into Uppaal, should manage time only through clocks. We then seek to validate our modeling using the B method. For that, we begin with an abstract specification of the schedulers, and we refined it by successive steps in order to take into account the characteristics of timed automata. We then verified the refinements hierarchy by proving the various generated proof obligations. In order to translate the B modeling of the schedulers into Uppaal, we defined a B0_Uppaal language and rules to be respected for the transformation. This translation is finally checked by schedulability properties expressed in the CTL logic
8
Sampaio, Elesbao Mazza Eduardo. "Méthode pour la spécification de responsabilité pour les logiciels : Modelisation, Tracabilité et Analyse de dysfonctionnements." Thesis, Grenoble, 2012. http://www.theses.fr/2012GRENM022/document.
Full textAbstract:
Malgré les progrès importants effectués en matière de conception de logiciels et l'existence de méthodes de développement éprouvées, il faut reconnaître que les défaillances de systèmes causées par des logiciels restent fréquentes. Il arrive même que ces défaillances concernent des logiciels critiques et provoquent des dommages significatifs. Considérant l'importance des intérêts en jeu, et le fait que la garantie de logiciel "zéro défaut" est hors d'atteinte, il est donc important de pouvoir déterminer en cas de dommages causés par des logiciels les responsabilités des différentes parties. Pour établir ces responsabilités, un certain nombre de conditions doivent être réunies: (i) on doit pouvoir disposer d'éléments de preuve fiables, (ii) les comportements attendus des composants doivent avoir été définis préalablement et (iii) les parties doivent avoir précisé leurs intentions en matière de répartition des responsabilités. Dans cette thèse, nous apportons des éléments de réponse à ces questions en proposant un cadre formel pour spécifier et établir les responsabilités en cas de dysfonctionnement d'un logiciel. Ce cadre formel peut être utilisé par les parties dans la phase de rédaction du contrat et pour concevoir l'architecture de logs du système. Notre première contribution est une méthode permettant d'intégrer les définitions formelles de responsabilité et d'éléments de preuves dans le contrat juridique. Les éléments de preuves sont fournis par une architecture de logs dite "acceptable" qui dépend des types de griefs considérés par les parties. La seconde contribution importante est la définition d'une procédure incrémentale, qui est mise en ?uvre dans l'outil LAPRO, pour l'analyse incrémentale de logs distribués<br>Despite the effort made to define methods for the design of high quality software, experience shows that failures of IT systems due to software errors remain very common and one must admit that even critical systems are not immune from that type of errors. One of the reasons for this situation is that software requirements are generally hard to elicit precisely and it is often impossible to predict all the contexts in which software products will actually be used. Considering the interests at stake, it is therefore of prime importance to be able to establish liabilities when damages are caused by software errors. Essential requirements to define these liabilities are (1) the availability of reliable evidence, (2) a clear definition of the expected behaviors of the components of the system and (3) the agreement between the parties with respect to liabilities. In this thesis, we address these problems and propose a formal framework to precisely specify and establish liabilities in a software contract. This framework can be used to assist the parties both in the drafting phase of the contract and in the definition of the architecture to collect evidence. Our first contribution is a method for the integration of a formal definition of digital evidence and liabilities in a legal contract. Digital evidence is based on distributed execution logs produced by "acceptable log architectures". The notion of acceptability relies on a formal threat model based on the set of potential claims. Another main contribution is the definition of an incremental procedure, which is implemented in the LAPRO tool, for the analysis of distributed logs
9
Maillot, Yvan. "Contribution à la spécification d'un environnement de simulation à événements discrets : spécification formelle d'une méthode de traduction automatique d'un modèle comportemental en un modèle exécutable." Besançon, 1997. http://www.theses.fr/1997BESA2053.
Full textAbstract:
Il y a dix ans à peine, la simulation n'était utilisée qu'en dernier recours. Force est de constater qu'aujourd'hui elle a pris le pas sur les autres techniques d'évaluation de systèmes. L'étude présentée concerne la simulation à événements discrets (SED) dont les outils sont de plus en plus sophistiqués avec, notamment, l'apparition d'environnements de SED. L'objet de cette thèse est de fournir une contribution à la spécification d'un environnement de SED. Il s'agit, en premier lieu, de cerner ses orientations et de dresser la liste des exigences qu'il doit satisfaire. Un deuxième travail consiste à caractériser le profil d'une méthode de modélisation pour la SED dont l'application conduit à plusieurs abstractions du système étudié, et notamment une description de son comportement basée sur le formalisme des Statecharts. La principale contribution de cette étude est de fournir une spécification formelle d'une méthode de traduction automatique d'un modèle comportemental en un modèle exécutable. La méthode proposée généralise l'expression de la traduction d'un sous-ensemble des Statecharts en code VHDL. Elle présente des avantages certains par rapport aux outils déjà existants, comme celui d'être clairement reproductible et facilement adaptable en machine, contrairement aux traducteurs commerciaux qui ne dévoilent pas leurs solutions techniques ; en outre, c'est une méthode formelle au sens où l'on sait établir qu'un Statechart est dans l'ensemble des <<<>traduisibles<>>> ; à chacun d'eux, on associe un code unique, dont le calcul est explicite. D'autres avantages majeurs sont inhérents à la technique de traduction qui respecte totalement la structure originelle du modèle et permet de générer un code modulaire, générique, réutilisable et hiérarchique. De plus, la hiérarchie ainsi respectée permet de conserver tout le potentiel de parallélisation du modèle originel.
10
Sampaio, elesbao mazza Eduardo. "Méthode pour la spécification de responsabilité pour les logiciels : Modelisation, Tracabilité et Analyse de dysfonctionnements." Phd thesis, Université de Grenoble, 2012. http://tel.archives-ouvertes.fr/tel-00767942.
Full textAbstract:
Malgré les progrès importants effectués en matière de conception de logiciels et l'existence de méthodes de développement éprouvées, il faut reconnaître que les défaillances de systèmes causées par des logiciels restent fréquentes. Il arrive même que ces défaillances concernent des logiciels critiques et provoquent des dommages significatifs. Considérant l'importance des intérêts en jeu, et le fait que la garantie de logiciel "zéro défaut" est hors d'atteinte, il est donc important de pouvoir déterminer en cas de dommages causés par des logiciels les responsabilités des différentes parties. Pour établir ces responsabilités, un certain nombre de conditions doivent être réunies: (i) on doit pouvoir disposer d'éléments de preuve fiables, (ii) les comportements attendus des composants doivent avoir été définis préalablement et (iii) les parties doivent avoir précisé leurs intentions en matière de répartition des responsabilités. Dans cette thèse, nous apportons des éléments de réponse à ces questions en proposant un cadre formel pour spécifier et établir les responsabilités en cas de dysfonctionnement d'un logiciel. Ce cadre formel peut être utilisé par les parties dans la phase de rédaction du contrat et pour concevoir l'architecture de logs du système. Notre première contribution est une méthode permettant d'intégrer les définitions formelles de responsabilité et d'éléments de preuves dans le contrat juridique. Les éléments de preuves sont fournis par une architecture de logs dite "acceptable" qui dépend des types de griefs considérés par les parties. La seconde contribution importante est la définition d'une procédure incrémentale, qui est mise en ?uvre dans l'outil LAPRO, pour l'analyse incrémentale de logs distribués.
11
ANDRE, Pascal. "Méthodes formelles et à objets pour le développement du logiciel :." Phd thesis, Université Rennes 1, 1995. http://tel.archives-ouvertes.fr/tel-00006148.
Full textAbstract:
Les spécifications formelles et la modélisation par objets sont considérés comme deux champs ayant un fort potentiel d'influence sur l'avenir du génie logiciel. Dans un premier temps, nous étudions cette affirmation en dégageant les caractéristiques essentielles du développement du logiciel. L'intersection des deux champs est un domaine nouveau et prometteur. Nous en étudions les différents variantes et nous synthétisons les choix faits dans les méthodes formelles à objets actuelles. Dans ce contexte, cette thèse propose une méthode de spécification et de conception de composants logiciels destinée à faciliter la formalisation, automatiser partiellement le processus de conception, permettre le contrôle et la réutilisation des classes avant implantation. L'accent est mis sur la séparation entre les niveaux de description pour clarifier le processus de conception et sur l'uniformisation à l'intérieur des niveaux de description pour assurer la cohérence. Deux modèles sont décrits. Le premier modèle, dit des types abstraits graphiques, définit les composants suivant un axe dynamique et suivant un axe fonctionnel. La modélisation dynamique, naturelle pour des objets est donnée en termes d'automates d'états finis gardés. Outre sa lisibilité, le modèle dynamique a pour intérêt majeur la construction guidée de spécifications algébriques, support de l'axe fonctionnel. Le second modèle, dit des classes formelles, est un modèle général, formel et abstrait pour la conception à objets. Basé sur les types abstraits algébriques, il permet le raisonnement abstrait et ma mise en oeuvre dans différents langages de programmation à objets. Les modèles présentés sont indépendants et sont adaptables dans d'autres méthodes de développement. Nous proposons une méthode de transition entre ces deux modèles, qui favorise le contrôle et la réutilisation des spécifications. Plusieurs outils d'écriture et de preuve sont communs aux deux modèles et nous insistons sur l'ouverture vers d'autres environnements de spécification.
12
Clochard, Martin. "Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels." Thesis, Université Paris-Saclay (ComUE), 2018. http://www.theses.fr/2018SACLS071/document.
Full textAbstract:
Cette thèse se positionne dans le domaine de la vérification déductive de programmes, qui consiste à transformer une propriété à vérifier sur un programme en un énoncé logique, pour ensuite démontrer cet énoncé. La vérification effective d'un programme peut poser de nombreuses difficultés pratiques. En fait, les concepts mis en jeu derrière le programme peuvent suffire à faire obstacle à la vérification. En effet, certains programmes peuvent être assez courts et n'utiliser que des constructions simples, et pourtant s'avérer très difficiles à vérifier. Cela nous amène à la question suivante: dans le contexte d'un environnement de vérification déductive de programmes basé sur les démonstrateurs automatiques, quelles méthodes appliquer pour réduire l'effort nécessaire à la fois pour spécifier des comportements attendus complexes, ainsi que pour démontrer qu'un programme respecte ces comportements attendus? Pour mener notre étude, nous nous sommes placés dans le cadre de l'environnement de vérification déductive de programmes Why3. La vérification de programmes en Why3 est basée sur la génération de conditions de vérification, et l'usage de démonstrateurs externes pour les prouver, que ces démonstrateurs soient automatiques ou interactifs. Nous avons développé plusieurs méthodes, certaines générales et d'autres spécifiques à des classes de programmes, pour réduire l'effort manuel. Nos contributions sont les suivantes. Tout d'abord, nous ajoutons des fonctionnalités à Why3 pour assister le processus de vérification, notamment un mécanisme léger de preuve déclarative basé sur la notion d'indicateurs de coupures. Ensuite, nous présentons une méthode de vérification d'absence de débordement arithmétique pour une classe d'utilisation des entiers difficile à traiter par les méthodes standards. Enfin, nous nous intéressons au développement d'une bibliothèque générique pour la spécification et la preuve de programmes générateurs de code<br>This thesis is set in the domain of deductive verification of programs, which consists of transforming a property to be verified about a program into a logical statement, and then proving this statement. Effective verification of a program can pose many practical difficulties. In fact, the concepts behind the program may be sufficient to impede verification. Indeed, some programs can be quite short and use only simple constructions, and yet prove very difficult to verify. This leads us to the following question: in the context of a deductive program verification environment based on automatic provers, what methods can be applied to reduce the effort required both to specify complex behaviors, as well as to prove that a program respects these expected behaviors? To carry out our study, we placed ourselves in the context of the deductive verification environment of programs Why3. The verification of programs in Why3 is based on the generation of verification conditions, and the use of external provers to prove them, whether these provers are automatic or interactive. We have developed several methods, some general and others specific to some program classes, to reduce manual effort. Our contributions are as follows. First, we add features to Why3 to assist the verification process, including a lightweight declarative proof mechanism based on the notion of cut indicators. Then we present a method for checking the absence of arithmetic overflow, for use cases which are difficult to process by standard methods. Finally, we are interested in the development of a generic library for the specification and proof of code generating programs
13
Messabihi, Mohamed El-Habib. "Contribution à la spécification et à la vérification des logiciels à base de composants : enrichissement du langage de données de Kmelia et vérification de contrats." Nantes, 2011. http://www.theses.fr/2011NANT2017.
Full textAbstract:
L'utilisation croissante des composants et des services logiciels dans les différents secteurs d'activité (télécommunications, transports, énergie, finance, santé, etc …) exige des moyens (modèles, méthodes, outils, etc. . . ) rigoureux afin de maîtriser leur production et d'évaluer leur qualité. En particulier, il est crucial de pouvoir garantir leur bon fonctionnement en amont de leur déploiement lors du développement modulaire de systèmes logiciels. Kmelia est un modèle à composants multi-services développé dans le but de construire des composants logiciels et des assemblages prouvés corrects. Trois objectifs principaux sont visés dans cette thèse. Le premier consiste à enrichir le pouvoir d'expression du modèle Kemlia avec un langage de données afin de satisfaire le double besoin de spécification et de vérification. Le deuxième vise l'élaboration d'un cadre de développement fondé sur la notion de contrats multi-niveaux. L'intérêt de tels contrats est de maîtriser la construction progressive des systèmes à base de composants et d'automatiser le processus de leur vérification. Nous nous focalisons dans cette thèse sur la vérification des contrats fonctionnels en utilisant la méthode B. Le troisième objectif est l'instrumentation de notre approche dans la plate-forme COSTO/Kmelia. Nous avons implanté un prototype permettant de connecter COSTO aux différents outils associés à la méthode B. Ce prototype permet de construire les machines B à partir de spécifications Kmelia en fonction des propriétés à vérifier. Nous montrons que la preuve des spécifications B générées garantit la cohérence des spécifications Kmelia de départ. Les illustrations basées sur l'exemple CoCoMe confortent nos propositions<br>The pervasiveness of software components and services in various domains (telecommunications, transportation, energy financial transactions, health, etc. ) requires rigorous means (models, methods, tools, etc. ) to control their production and to assess their quality. In particular, when developing such modular systems, it is crucial to ensure their safe bahaviour before deployment. Kmelia is a multi-services component model developed with the aim of building correct software components and assemblies. Three main goals are covered in this thesis. The first one is to enrich the expressiveness of the Kmelia model with a data language in order to satisfy the twofold need of specification and verification. The second one is to provide a framework development based on the concept of multi-level contracts. The interest of such contracts is to master the incremental construction of component-based systems and to automate the process of their verification. In this thesis, we focus on the verification of functional contracts using the B method. The last goal is to implement our approach in the COSTO/Kmelia platform. We developed a prototype that connects COSTO to various B method tools. This prototype builds B machines from Kmelia specifications according to the set of properties to check. We show that proof of the generated B specifications ensures consistency of initial Kmelia specifications. Several examples from the CoCoME ease study consolidate our proposal
14
MARQUESUZAÀ, Christophe. "OMAGE : Outils et Méthode pour la spécification des connaissances au sein d'un Atelier de Génie Educatif." Phd thesis, Université de Pau et des Pays de l'Adour, 1998. http://tel.archives-ouvertes.fr/tel-00003699.
Full textAbstract:
Les nouvelles technologies de l'information sont entrées au cœur de notre société et provoquent de profonds changements dans notre vie quotidienne, notamment dans le monde du travail. Or le métier d'enseignant n'a pas vraiment évolué, même si les méthodes éducatives changent, car toute tentative d'introduction de l'informatique se heurte à la méfiance des enseignants qui ont peur de perdre leur liberté de choix éducatifs. De plus, les avancées technologiques n'ont d'intérêt que si elles sont intégrées dans un processus global de conception d'applications éducatives. Nos recherches ont donc pour objectif principal de faciliter la tâche de l'enseignant dans la préparation de ses séquences pédagogiques. Nous définissons ainsi le support méthodologique d'un environnement informatique d'aide à la spécification des connaissances éducatives. Nous organisons alors nos travaux autour de trois axes. Tout d'abord, nous proposons la mise en place d'enseignements axés sur la notion de situations-problèmes au sens IUFM car elle met les apprenants en situation de projet tout en répondant aux objectifs pédagogiques fixés. Nous exposons ensuite la nécessité pour les enseignants de se reposer sur un processus de spécification formelle que nous définissons et pour lequel nous proposons un cycle de vie basé sur le prototypage rapide. Nous proposons aussi une ontologie de l'enseignement s'appuyant sur une architecture orientée-objet. Nous montrons enfin que l'utilisation de méta-outils CASE permet de développer un environnement ayant une assistance adaptée et suffisamment flexible pour permettre différentes façons de spécifier et différents points de vue et-ou formalismes de représentation sur une spécification. Le prototype développé couple le méta-outil CASE HARDY, qui fournit une interface diagrammatique supportant les étapes du processus de développement, et le générateur de système expert CLIPS qui assure la cohésion globale en terme de guidage et de flexibilité.
15
Akhtar, Nadeem. "Contribution à la spécification formelle et à la vérification de systèmes multi-agents robotiques." Lorient, 2010. http://www.theses.fr/2010LORIS190.
Full textAbstract:
L'une des tâches les plus difficiles en ingénierie des spécifications de systèmes multi-agents robotiques est d'assurer les propriétés d’exactitude que sont la sûreté et la vivacité. Comme ces systèmes complexes sont concurrents et s’exécutent dans des environnements dynamiques et distribués, leur spécification formelle, leur vérification ainsi que leur transformation par raffinement jouent un rôle majeur dans la fiabilité du système. Nos objectifs sont de proposer une approche de développement basée sur une combinaison de méthodes et de techniques qui permettent la vérification formelle et la validation pendant la définition des spécifications et qui soit flexible. Cette approche permet la transformation par raffinement des spécifications abstraites et des propriétés fonctionnelles et non-fonctionnelles en des spécifications concrètes permettant leur vérification formelle. Les systèmes multi-agents robotiques sont des systèmes concurrents ayant des processus parallèles qui peuvent avoir des besoins de synchronisation. Une étude de cas de systèmes multi-agents robotiques a été présentée pour illustrer des spécifications formelles et leurs vérifications. Une combinaison d'algèbre de processus et de techniques basées sur des automates à état nous a permis de défini r les spécifications formelles de notre système, vérifier les propriétés de sûreté et de vivacité ainsi que le déroulement possible d'exécutions simultanées, cela nous a également permis d’identifié les avantages des méthodes formelles pour les systèmes multi-agents robotiques. Les méthodes formelles et les langues sont fondées sur des bases mathématiques solides. Notre capacité à construire des systèmes complexes devient d’autant plus grande que les techniques de vérification formelles deviennent plus matures. Pour traiter les problèmes de complexité des systèmes multi-agent et obtenir des résultats significatifs avec l'analyse formelle, nous devons nous occuper de la complexité à chaque stade du système multi-agent : de la phase de spécification à l'analyse, conception et la phase de vérification. La vérification formelle peut accomplir la couverture exhaustive complète du système garantissant ainsi que les échecs non détectés dans le comportement sont exclus. L'approche prise est de spécifier formellement chaque sous-portion d'un système et de la vérifier et ensuite, si c'est en accord avec du système ensemble, passer à la vérification formelle de chaque sous-partie du système. De cette manière les propriétés de sûreté et de vivacité du système peuvent être prouvées en formalisant les différentes composantes et des processus dans le cycle de vie de développement de système. Avoir une fondation formelle pour les langues et les instruments permit : l’amélioration de la documentation et la compréhension des spécifications, l'analyse rigoureuse de propriétés de système, être certain que les transformations et l'implémentation sont possibles sans erreur tout en conservant leurs propriétés, l’amélioration de la rigueur et de la qualité du processus de développement entier et fournir une fondation ferme pendant le processus d'évolution et d’adaptation. Par conséquent une solution est proposée se composant des méthodes multiples et des techniques pour la spécification formelle et la vérification de ces systèmes. Nous avons utilisé la méthode multi-agents Gaia ainsi que des processus et des automates d’états finis, et avons défini les spécifications formelles de notre système, vérifié leur correction avec propriétés de sûreté et de vivacité en générant tous les flux d'exécutions possibles. La logique temporelle LTS utilise le Processus d'État Fini (FSP) comme langue de contribution pour officiellement définir et vérifier que notre système et vérifier ses limites par l'enquête exhaustive de système expose l'espace pour la vérification formelle de chaque composante du système pour garantir les propriétés de sûreté et de vivacité. π-ADL dot NET est utilisé pour définir l'architecture de système et vérifier les aspects statiques aussi bien que dynamiques d'architecture. Le système est exécuté en utilisant le Microsoft Robotics Developer Studio (MRDS) l'environnement de simulation. Cette recherche présente une étude de cas complète qui est illustré au travers de la spécification d’un système multi-agents robotiques<br>One of the most challenging tasks in software engineering for multi-agent robotic systems is to ensure correctness properties of safety and liveness. As these systems have concurrency, and often have dynamic environments, the formal specification and verification of these systems along with step-wise refinement from abstract to concrete concepts play a major role in system correctness. The problem statement is: How can a safe multi-agent robotic system be developed? Here by safe the focus is on correctness properties which can be described by a combination of safety and liveness. How can safety and liveness properties be enforced during the development of multi-agent robotic system? Our objectives are to propose a development approach based on a combination of methods and techniques that allow for formal verification and evaluation during specification definition and that is also flexible. An approach which supports analysis with respect to functional, as well as non-functional properties by step-wise refinement from abstract to concrete specifications and then formal verification of these specifications. We have analysed the development process of a robotic multi-agent system after classifying it in the major phases of requirement specifications, verification specifications, architecture specifications and implementation. Formal methods and languages are based on a solid mathematical foundation. To catch up with the complexity problems in multi-agent systems and get significant results with formal analysis, we must cope with complexity at every stage of development: from the specification phase to the analysis, design and verification phase. Formal verification can be used for exhaustive investigation of system space thus ensuring that undetected failures in the behaviour are excluded. We construct the system incrementally from subcomponents, based on software architecture. State reduction is achieved by hiding actions and minimising; property checks remain in the minimised subcomponents. Each component of a specification is described as LTS, which has all the possible states a component may reach and all possible transitions it may perform. The reasons for having a formal foundation for the languages and tools are: (1) to enable rigorous analysis of system properties; (2) to be as certain as possible that the specifications, transformations, and implementation are property-preserving and error-free; (3) to improve rigor and quality of the whole development process; (4) to provide a firm foundation during the adaptation and evolution process; (5) to improve documentation and understanding of specifications. A solution has been proposed for formal specification and verification of safety and liveness properties. Our contributions are (1) an approach based on a combination of methods to allow for formal verification and evaluation during requirement specifications, verification specifications, architecture specifications, and implementation; (2) checking safety and liveness properties of correctness during each development phase; (3) a multi-agent robotic system case study to exemplify formal specifications and verification; (4) a combination of process algebra and finite automata based techniques to define the formal specifications of our system, using a model-checking method and verifying all possible flow of concurrent executions; (5) identifying the benefits of formal methods for multi-agent robotic systems. We have used the Gaia multi-agent method for requirement specifications; Labelled Transition Systems (LTS) based finite automata techniques, which take Finite State Process (FSP) as input language for verification specification; The π-ADL dot NET is used to define architecture specifications and check the static, as well as dynamic aspects of architecture; Then the system is implemented by using Service-Oriented Architecture (SOA) based Microsoft Robotics Developer Studio (MRDS) simulation environment
16
Rached, Miloud. "Spécification et vérification des systèmes temps réel réactifs en B." Toulouse 3, 2007. http://www.theses.fr/2007TOU30050.
Full textAbstract:
L'objectif de cette thèse est de développer des méthodes formelles permettant la spécification et la vérification des systèmes critiques. Plus précisément, nous proposons des extensions temporisées à la méthode B. Ces extensions vont nous permettre de spécifier et de vérifier des systèmes temps réel, ainsi que les interactions possibles avec leur environnement. Nous distinguons dans ce cas les propriétés qui doivent être satisfaites par l'environnement de celles qui doivent être satisfaites par le système. Dans ces dernières, nous nous intéressons plus particulièrement aux contraintes de réaction du contrôleur. Nous décrivons des modèles temporisés permettant la manipulation explicite du temps, afin qu'il soit possible d'exprimer des contraintes temps réel d'un système sous forme de propriétés quantitatives sur des délais. Pour la description du comportement dynamique des systèmes, nous avons choisi d'étendre la logique MITL (Metric Interval Temporal Logic) en EMITL (Event/state Metric Interval Temporal Logic) avec passé. Notre extension permet d'introduire des propriétés d'événements et des opérateurs temporisés sur le passé<br>The purpose of this Phd thesis is to develop formal methods allowing the specification and the verification of critical systems. More precisely, we propose timed extensions to the B method. These extensions will allow to specify and check real time systems, as well as the possible interactions with their environment. We distinguish in this case the properties which must be satisfied by the environment and those which must be satisfied by the system. In the latter, we are interested more particularly in the reaction constraints of the controller. We describe timed models allowing the explicit modeling of time, so that it is possible to express real time constraints of a system as quantitative properties on deadlines. For the description of the dynamic behavior of the systems, we chose to extend MITL logic (Metric Interval Temporal Logic) into EMITL (Event/state Metric Interval Temporal Logic) with past operators and event properties. Our extension allows the simultaneous occurrence of several events
17
Bon, Philippe. "Du cahier des charges aux spécifications formelles : une méthode basée sur les réseaux de Pétri de haut niveau." Lille 1, 2000. https://pepite-depot.univ-lille.fr/RESTREINT/Th_Num/2000/50376-2000-149.pdf.
Full textAbstract:
Aujourd'hui, un des points cruciaux dans le développement des logiciels critiques est le passage de l'informel au formel. Le but de cette thèse est de définir ici une méthodologie de développement permettant un passage plus intuitif du cahier de charges (spécifications informelles) aux spécifications formelles d'un système, en tenant compte de son comportement dynamique. Cette méthodologie se base sur l'utilisation d'un modèle lisible et expressif. Notre choix s'est donc porté les réseaux de Pétri de haut niveau qui combinent trois qualités importantes : la représentation graphique, le comportement dynamique et l'abstraction des traitements. Elle peut se décomposer en plusieurs phases. D'abord nous tenterons une représentation graphique du cahier des charges par le réseau de Pétri proprement dit. Puis la phase d'interprétation du cahier des charges où nous annoterons le réseau de Pétri obtenu par du langage naturel. La troisième phase, dite de formalisation, transformera les annotations du réseau de Pétri en formules mathématiques (contraintes). Enfin nous terminerons par une phase de traduction automatique du réseau de Pétri en machine abstraite b et nous poursuivrons par une procédure b classique.
18
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 textAbstract:
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.
19
Marquesuzaà, Christophe. "OMAGE : Outils et Méthode pour la spécification des connaissances au sein d'un Atelier de Génie Educatif." Phd thesis, Université de Pau et des Pays de l'Adour, 1998. http://tel.archives-ouvertes.fr/hal-00002957.
Full textAbstract:
Les nouvelles technologies de l'information sont entrées au cœur de notre société et provoquent de profonds changements dans notre vie quotidienne, notamment dans le monde du travail. Or le métier d'enseignant n'a pas vraiment évolué, même si les méthodes éducatives changent, car toute tentative d'introduction de l'informatique se heurte à la méfiance des enseignants qui ont peur de perdre leur liberté de choix éducatifs. De plus, les avancées technologiques n'ont d'intérêt que si elles sont intégrées dans un processus global de conception d'applications éducatives. Nos recherches ont donc pour objectif principal de faciliter la tâche de l'enseignant dans la préparation de ses séquences pédagogiques. Nous définissons ainsi le support méthodologique d'un environnement informatique d'aide à la spécification des connaissances éducatives. Nous organisons alors nos travaux autour de trois axes. Tout d'abord, nous proposons la mise en place d'enseignements axés sur la notion de situations-problèmes au sens IUFM car elle met les apprenants en situation de projet tout en répondant aux objectifs pédagogiques fixés. Nous exposons ensuite la nécessité pour les enseignants de se reposer sur un processus de spécification formelle que nous définissons et pour lequel nous proposons un cycle de vie basé sur le prototypage rapide. Nous proposons aussi une ontologie de l'enseignement s'appuyant sur une architecture orientée-objet. Nous montrons enfin que l'utilisation de méta-outils CASE permet de développer un environnement ayant une assistance adaptée et suffisamment flexible pour permettre différentes façons de spécifier et différents points de vue et-ou formalismes de représentation sur une spécification. Le prototype développé couple le méta-outil CASE HARDY, qui fournit une interface diagrammatique supportant les étapes du processus de développement, et le générateur de système expert CLIPS qui assure la cohésion globale en terme de guidage et de flexibilité.
20
Gaspar, Nuno. "Support mécanisé pour la spécification formelle, la vérification et le déploiement d'applications à base de composants." Thesis, Nice, 2014. http://www.theses.fr/2014NICE4127/document.
Full textAbstract:
Cette thèse appartient au domaine des méthodes formelles. Nous nous concentrons sur leur application à une méthodologie spécifique pour le développement de logiciels: l'ingénierie à base de composants. Le Grid Component Model (GCM) suit cette méthodologie en fournissant tous les moyens pour définir, composer, et dynamiquement reconfigurer les applications distribuées à base de composants. Dans cette thèse, nous abordons la spécification formelle, la vérification et le déploiement d'applications GCM reconfigurables et distribuées. Notre première contribution est un cas d'étude industriel sur la spécification comportementale et la vérification d'une application distribuée et reconfigurable: L'HyperManager. Notre deuxième contribution est une plate-forme, élaborée avec l'assistant de preuve Coq, pour le raisonnement sur les architectures logicielles: Mefresa. Cela comprend la mécanisation de la spécification du GCM, et les moyens pour raisonner sur les architectures reconfigurables GCM. En outre, nous adressons les aspects comportementaux en formalisant une sémantique basée sur les traces d'exécution de systèmes de transitions synchronisées. Enfin, notre troisième contribution est un nouveau langage de description d'architecture (ADL): Painless. En outre, nous discutons son intégration avec ProActive, un intergiciel Java pour la programmation concurrente et distribuée, et l'implantation de référence du GCM<br>This thesis belongs to the domain of formal methods. We focus their application on a specific methodology for the development of software: component-based engineering.The Grid Component Model (GCM) endorses this approach by providing all the means to define, compose and dynamically reconfigure component-based distributed applications. In this thesis we address the formal specification, verification and deployment of distributed and reconfigurable GCM applications. Our first contribution is an industrial case study on the behavioural specification and verification of a reconfigurable distributed application: The HyperManager. Our second contribution is a framework, developed with the Coq proof assistant, for reasoning on software architectures: Mefresa. This encompasses the mechanization of the GCM specification, and the means to reason about reconfigurable GCM architectures. Further, we address behavioural concerns by formalizing a semantics based on execution traces of synchronized transition systems. Overall, it provides the first steps towards a complete specification and verification platform addressing both architectural and behavioural properties. Finally, our third contribution is a new Architecture Description Language (ADL), denominated Painless. Further, we discuss its proof-of-concept integration with ProActive, a Java middleware for concurrent and distributed programming, and the de facto reference implementation of the GCM
21
Guesmi, Asma. "Spécification et analyse formelles des politiques de sécurité dans un processus de courtage de l'informatique en nuage." Thesis, Orléans, 2016. http://www.theses.fr/2016ORLE2010/document.
Full textAbstract:
Les offres de l’informatique en nuage augmentent de plus en plus et les clients ne sont pas capables de lescomparer afin de choisir la plus adaptée à leurs besoins. De plus, les garanties de sécurité proposées parles fournisseurs restent incompréhensibles pour les clients. Cela représente un frein pour l'adoption dessolutions de l’informatique en nuage.Dans cette thèse, nous proposons un mécanisme de courtage des services de l’informatique en nuage quiprend en compte les besoins du client en termes de sécurité.Les besoins exprimés par le client sont de deux natures. Les besoins fonctionnels représentent lesressources et leurs performances. Les besoins non-fonctionnels représentent les propriétés de sécurité etles contraintes de placement des ressources dans le nuage informatique. Nous utilisons le langage Alloypour décrire les offres et les besoins. Nous utilisons l'analyseur Alloy pour l'analyse et la vérification desspécifications du client. Le courtier sélectionne les fournisseurs qui satisfont les besoins fonctionnels et nonfonctionnelsdu client. Il vérifie ensuite, que la configuration du placement des ressources chez lesfournisseurs respecte toutes les propriétés de sécurité exigées par le client.Toutes ces démarches sont effectuées avant le déploiement des ressources dans le nuage informatique.Cela permet de détecter les erreurs et conflits des besoins du client tôt. Ainsi, on réduit les vulnérabilités desressources du client une fois déployées<br>The number of cloud offerings increases rapidly. Therefore, it is difficult for clients to select the adequate cloud providers which fit their needs. In this thesis, we introduce a cloud service brokerage mechanism that considers the client security requirements. We consider two types of the client requirements. The amount of resources is represented by the functional requirements. The non-functional requirements consist on security properties and placement constraints. The requirements and the offers are specified using the Alloy language. To eliminate inner conflicts within customers requirements, and to match the cloud providers offers with these customers requirements, we use a formal analysis tool: Alloy. The broker uses a matching algorithm to place the required resources in the adequate cloud providers, in a way that fulfills all customer requirements, including security properties. The broker checks that the placement configuration ensures all the security requirements. All these steps are done before the resources deployment in the cloud computing. This allows to detect the conflicts and errors in the clients requirements, thus resources vulnerabilities can be avoided after the deployment
22
Matiedje, Tawa Jeanne. "Extension événementielle d'une méthode formelle légère et application à l'analyse du protocole distribué Chord." Thesis, Toulouse, ISAE, 2019. http://www.theses.fr/2019ESAE0029.
Full textAbstract:
Cette étude concerne l’utilisation de la logique du premier ordre et la logique temporelle linéaire pour la spécification et la vérification des systèmes dynamiques ayant des structures riches. Elle concerne l’étude de la correction de fonctionnement du protocole de recherche distribuée Chord. L’objectif est d’une part d’améliorer la spécification et la vérification des systèmes dans le langage formel Electrum qui est une extension dynamique du langage formel Alloy basé sur la logique du premier ordre temporelle linéaire.Pour ce faire, nous avons développé une couche syntaxique au-dessus d’Electrum. L’objectif de cette couche est de faciliter la spécification du comportement dans Electrum, pour ce faire, nous avons défini une syntaxe permettant de générer automatiquement une partie de la spécification du comportement. Par ailleurs cette couche permet également de réduire les erreurs de spécification en déchargeant les utilisateurs de la spécification de certaines tâches comportementales ardues et sujettes aux erreurs.D’autre part, l’objectif est d’analyser formellement la correction de la propriété fondamentale de vivacité du protocole Chord. Pour ce faire nous avons spécifié et vérifié le protocole Chord avec l’extension d’Electrum que nous avons développée, puis nous avons prouvé sa correction et montré les avantages de notre méthode d’analyse<br>This study deals with the use of first-order logic and linear temporal logic for specificationand verification of dynamics system with rich structural properties. It also concerns the studyof the operating safety of the distributed lookup protocol Chord. The aim is on the one hand toimprove the specification and verification of systems whith the formal language Electrum a dynamicextension of the formal language Alloy based on first-order linear temporal logic. To do this, we havedeveloped an action layer above Electrum. The purpose of this layer is to make the specification ofthe behavior in Electrum easier, to do this, we have defined a syntax to automatically generate partof the specification of the behavior. Moreover, this layer also makes it possible to reduce specificationerrors by getting rid the users of the specification of certain laborious and error-prone behavioraltasks. On the other hand, the aim is the formal analyzing of the fundamental liveness property ofthe Chord protocol. To do this, we specified and verified the Chord protocol with the extension ofElectrum that we have developed, then we proved its correctness and showed the advantages of ouranalysis method
23
Petit, Dorian. "Génération automatique de composants logiciels sûrs à partir de spécifications formelles B." Valenciennes, 2003. http://www.theses.fr/2003VALE0039.
Full textAbstract:
Ce mémoire est consacré à l'étude de la génération de code à partir de spécifications formelles B. L'aspect primordial à maîtriser pour la génération de code est la modularité du langage B. Pour ce faire, nous avons modélisé le système de modules du langage B en l'exprimant par un système de modules à la Harper-Lillibridge-Leroy. Cette modélisation nous permet de clarifier certains aspects de la modularité de B et nous permet ainsi d'avoir une représentation des spécifications B qui pourra ensuite être utilisée lors de la phase de génération de code. Ce nouveau système de module pour B nous permet également d'aborder une technique de production de logiciel, la programmation par composants. Cette technique est souvent utilisée conjointement à la programmation par contrats. Notre démarche de génération de code permet de marier ces deux techniques à celle du développement formel B pour tirer partie des avantages de chacune des méthodes de développement<br>These works are related to the study of the code generation from B formal specifications. The main aspect that should be studied in the code generation is the modularity of the B language. We have expressed the B modularity with an Harper-Lillibridge-Leroy module system (an ML-like module system). This modelisation clarifies some aspects of the B modularity and gives us a representation of the B modules that are used during the phase of code generation. This new module system for the B language allows us to tackle a software production technique: the components based approach. This technique is often used conjointly with the design by contracts technique. Our code generation process allows to blend the design by contracts approach, the component based approach and the B method. We can take advantage of the three approaches to develop software
24
Embe, Jiague Michel. "Approches formelles de mise en oeuvre de politiques de contrôle d'accès pour des applications basées sur une architecture orientée services." Thèse, Université de Sherbrooke, 2012. http://hdl.handle.net/11143/6683.
Full textAbstract:
La sécurité des systèmes d'information devient un enjeu préoccupant pour les organisations tant publiques que privées, car de tels systèmes sont pour la plupart universellement accessibles à partir de navigateurs Web. Parmi tous les aspects liés à la sécurité des systèmes d'information, c'est celui de la sécurité fonctionnelle qui est étudié dans cette Thèse sous l'angle de la mise en oeuvre de politiques de contrôle d'accès dans une architecture orientée services. L'élément de base de la solution proposée est un modèle générique qui introduit les concepts essentiels pour la conception de gestionnaires d'exécution de politiques de contrôle d'accès et qui établit une séparation nette entre le système d'information et les mécanismes de contrôle d'accès. L'instanciation de ce modèle conduit à un cadre d'applications qui comporte, entre autres, un filtre de contrôle d'accès dynamique. Cette Thèse présente également deux méthodes systématiques d'implémentation de ce filtre à partir de politiques écrites en ASTD, une notation graphique formelle basée sur les statecharts augmentés d'opérateurs d'une algèbre de processus. La notation ASTD est plus expressive que la norme RBAC et ses extensions. La première méthode repose sur une transformation de politiques de contrôle d'accès, instanciées à partir de patrons de base exprimés en ASTD, en des processus BPEL. La deuxième méthode est basée sur une interprétation de spécifications ASTD par des processus BPEL. Dans les deux cas, les processus BPEL s'exécutent dans un moteur d'exécution BPEL et interagissent avec le système d'information. Ces deux méthodes permettent une implémentation automatique d'un cadre d'applications à partir de la spécification de départ. Finalement, un prototype a été réalisé pour chacune des deux méthodes afin de montrer leur faisabilité au niveau fonctionnel et de comparer leurs performances au niveau système.
25
Idani, Akram. "B/UML : Mise en relation de spécifications B et de descriptions UML pour l'aide à la validation externe de développements formels en B." Phd thesis, Université Joseph Fourier (Grenoble), 2006. http://tel.archives-ouvertes.fr/tel-00118718.
Full textAbstract:
Les exigences qui s'appliquent aux composants logiciels et aux logiciels embarqués justifient l'utilisation des meilleures techniques disponibles pour garantir la qualité des spécifications et conserver cette qualité lors du développement du code. Les méthodes formelles, et parmi elles la méthode B, permettent d'atteindre ce niveau de qualité. Cependant, ces méthodes utilisent des notations et des concepts spécifiques, qui génèrent souvent une faible lisibilité et une difficulté d'intégration dans les processus de développement et de certification. Ainsi, proposer des environnements de spécification, de développement de programmes et de logiciels, combinant des méthodes formelles et des méthodes semi-formelles largement utilisées dans les projets industriels, en l'occurrence B et UML, s'avère d'une grande importance. Notre intérêt porte précisément sur la méthode B qui est une méthode formelle utilisée pour modéliser des systèmes et prouver l'exactitude de leur conception par raffinements successifs. Mais les spécifications formelles sont difficiles à lire quand elles ne sont pas accompagnées d'une documentation. Cette lisibilité est essentielle pour une bonne compréhension de la spécification, notamment dans des phases de validation ou de certification. Aujourd'hui, en B, cette documentation est fournie sous forme de texte, avec, quelquefois, des schémas explicitant certaines caractéristiques du système. L'objectif de ce travail de thèse est de mettre en relation des spécifications en B avec des diagrammes UML, qui constituent un standard de facto dans le monde industriel et dont le caractère graphique améliore la lisibilité. Nous avons axé notre processus de dérivation de diagrammes de classes à partir de spécifications B autour d'une technique d'ingénierie inverse guidée par un ensemble de correspondances structurelles et sémantiques spécifiées à un méta-niveau. Quant à la dérivation de diagrammes d'états/transitions, elle a été orientée vers une technique d'abstraction de graphes d'accessibilité construits par une exploration exhaustive du comportement de la spécification.
26
Lambolais, Thomas. "Modélisation du développement de spécifications LOTOS." Vandoeuvre-les-Nancy, INPL, 1997. http://www.theses.fr/1997INPL106N.
Full textAbstract:
Notre travail s'inscrit dans les premières étapes du développement de logiciels concernant le passage d'un cahier des charges à une spécification formelle, dans le domaine des réseaux de télécommunications. Notre sujet consiste à étudier la modélisation des étapes de développement de spécifications en langage LOTOS. Le modèle utilisé, PROPLANE, a été préalablement établi pour d'autres domaines. Par le biais d'un nouveau domaine d'application, l'objectif à long terme de notre étude est d'évaluer le modèle PROPLANE et de proposer des améliorations si nécessaire. LOTOS est constitué d'une algèbre de processus et d'une algèbre de données. Nous nous sommes concentrés sur la construction des expressions de comportement, c'est-à-dire des processus, en ayant éventuellement recours aux données. Sous le modèle PROPLANE, toute évolution d'un développement est gérée par des operateurs de développement. Notre modélisation correspond ainsi à des définitions d'operateurs pouvant s'enchainer les uns aux autres. Nous distinguons les constructions architecturale et, comportementale, pour lesquelles les mécanismes utilisés en LOTOS diffèrent. L’architecture fait une large utilisation des operateurs de composition parallèle, avec lesquels il faut veiller à conserver des processus effectifs, voire réguliers. Nous définissons pour cela des notions telles que la rigidité. La construction comportementale demande de définir des opérateurs permettant de gérer le développement d'arbres de transitions, ainsi que le détail de ces transitions. La nouveauté de notre approche consiste à chercher à profiter des propriétés sémantiques des processus en cours de développement. Afin de supporter des lignes de construction incrémentale par réduction de l'indéterminisme, nous donnons une définition opérationnelle des relations d'extension et de réduction de processus. Il apparait que PROPLANE doit être étendu pour manipuler des propriétés temporelles sur les états de développement.
27
Lecoeuche, Renaud. "Formalisation et évaluation des théories traitant des centres d'attention et application aux dialogues en langue naturelle d'acquisition des besoins." Rouen, 1999. http://www.theses.fr/1999ROUES043.
Full textAbstract:
L'acquisition des besoins est une étape difficile de l'ingénierie logicielle, pendant laquelle les spécifications d'un nouveau logiciel sont discutées avec les futurs utilisateurs. Vérifier que cette étape est correcte est une tâche complexe. Une aide informatique est donc souvent bénéfique. Cette aide nécessite des spécifications formelles. Cependant, peu de gens sont habitues à utiliser des langages de spécifications formels. Des langages adaptés à un domaine particulier peuvent aider dans l'écriture de spécifications formelles, mais l'acquisition reste souvent entachée d'erreurs. Un outil qui interagit avec les utilisateurs et les aide à exprimer leurs besoins pourrait réduire le nombre d'erreurs commises. Le but est ici d'extraire les besoins activement par un dialogue avec les utilisateurs. Malgré le développement de nombreux moyens de représentation et d'analyse des besoins, peu d'attention a été donnée au contrôle du dialogue ordinateur-utilisateur lors de l'acquisition des besoins. Les théories traitant des centres d'attention expliquent comment les protagonistes d'un dialogue portent leur attention sur certaines choses à certains moments du dialogue. Dans cette thèse, nous proposons d'utiliser ces théories afin d'améliorer la qualité du dialogue ordinateur-utilisateurs. Nous montrons qu'en combinant les contraintes sur l'évolution du dialogue données par ces théories et les contraintes inhérentes à l'acquisition des besoins nous pouvons guider l'acquisition d'une manière naturelle et facile à suivre pour les utilisateurs. Cette utilisation interactive des théories traitant des centres d'attention est nouvelle. Nous comparons également différentes théories pour cette tâche. Cela nous force à formaliser les théories et à développer une méthode originale pour les tester empiriquement.
28
Mariano, Georges. "Evaluation de logiciels critiques développés par la méthode B : une approche quantitative." Valenciennes, 1997. https://ged.uphf.fr/nuxeo/site/esupversions/823185e9-e82a-44fc-b3e2-17a0b205165e.
Full textAbstract:
Dans le cadre de l'utilisation de la méthode formelle B, nous proposons de contribuer à l'évaluation des développements de logiciels critiques, par la mise en place de techniques quantitatives. Ces techniques s'articulent autour de la définition, de l'extraction et de l'interprétation de mesures (ou métriques) issues du produit à évaluer. Notre progression vers cet objectif se décompose en trois étapes. La première étape est constituée par la modélisation des spécifications formelles définissant le logiciel. Le modèle obtenu repose sur l'ensemble des arbres syntaxiques correspondant à chaque composant B. Ces arbres sont obtenus par la définition d'une grammaire BNF (backus-naur form) couvrant l'intégralité de la notation B. Ceci nous a amené à proposer des modifications de la notation B. La deuxième étape consiste à définir des mesures primitives à partir des informations contenues dans les arbres syntaxiques des composants B. Ces mesures sont basées sur un mécanisme générique de filtrage syntaxique arborescent. La troisième étape concerne la définition de mesures spécifiques adaptées aux caractéristiques de la méthode B. Nous donnons trois exemples de mesures spécifiques. La première mesure, LARA, concerne l'évaluation de la phase de preuve, la deuxième mesure, MONA, évalue le niveau d'abstraction des spécifications formelles et enfin la troisième mesure, CIEL, s'efforce de caractériser la complexité des spécifications formelles. Pour terminer, sur une étude de cas bien connue, la chaudière (Boiler), nous appliquons les outils développés pour extraire ces mesures. Nous présentons les valeurs obtenues sous une forme graphique spécialement adaptée à la structure des projets B, et nous montrons comment ces outils peuvent-être utilisés pour élaborer des analyses portant sur la qualité globale des développements de logiciel en B.
29
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 textAbstract:
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.
30
Nganyewou, Tidjon Lionel. "Modélisation formelle des systèmes de détection d'intrusions." Electronic Thesis or Diss., Institut polytechnique de Paris, 2020. http://www.theses.fr/2020IPPAS021.
Full textAbstract:
L'écosystème de la cybersécurité évolue en permanence en termes du nombre, de la diversité, et de la complexité des attaques. De ce fait, les outils de détection deviennent inefficaces face à certaines attaques. On distingue généralement trois types de système de détection d'intrusions: détection par anomalies, détection par signatures et détection hybride. La détection par anomalies est fondée sur la caractérisation du comportement habituel du système, typiquement de manière statistique. Elle permet de détecter des attaques connues ou inconnues, mais génère aussi un très grand nombre de faux positifs. La détection par signatures permet de détecter des attaques connues en définissant des règles qui décrivent le comportement connu d'un attaquant. Cela demande une bonne connaissance du comportement de l'attaquant. La détection hybride repose sur plusieurs méthodes de détection incluant celles sus-citées. Elle présente l'avantage d'être plus précise pendant la détection. Des outils tels que Snort et Zeek offrent des langages de bas niveau pour l'expression de règles de reconnaissance d'attaques. Le nombre d'attaques potentielles étant très grand, ces bases de règles deviennent rapidement difficiles à gérer et à maintenir. De plus, l'expression de règles avec état dit stateful est particulièrement ardue pour reconnaître une séquence d'événements. Dans cette thèse, nous proposons une approche stateful afin d'identifier des attaques complexes. Nous considérons l'approche diagramme état-transition hiérarchique, en utilisant les ASTDs. Les ASTDs permettent de représenter de façon graphique et modulaire une spécification, ce qui facilite la maintenance et la compréhension des règles. Nous étendons la notation ASTD avec de nouvelles fonctionnalités pour représenter des attaques complexes. Ensuite, nous spécifions plusieurs attaques avec la notation étendue et exécutons les spécifications obtenues sur des flots d'événements à l'aide d'un interpréteur pour identifier des attaques. Nous évaluons aussi les performances de l'interpréteur avec des outils industriels tels que Snort et Zeek. Puis, nous réalisons un compilateur afin de générer du code exécutable à partir d'une spécification ASTD, capable d'identifier efficacement les séquences d'événements<br>The cybersecurity ecosystem continuously evolves with the number, the diversity, and the complexity of cyber attacks. Generally, we have three IDS types: anomaly-based detection, signature-based detection, and hybrid detection. Anomaly detection is based on the usual behavior description of the system, typically in a static manner. It enables detecting known or unknown attacks, but generating also a large number of false positives. Signature based detection enables detecting known attacks by defining rules that describe known attacker's behavior. It needs a good knowledge of attacker behavior. Hybrid detection relies on several detection methods including the previous ones. It has the advantage of being more precise during detection. Tools like Snort and Zeek offer low level languages to represent rules for detecting attacks. The number of potential attacks being large, these rule bases become quickly hard to manage and maintain. Moreover, the representation of stateful rules to recognize a sequence of events is particularly arduous. In this thesis, we propose a stateful approach to identify complex attacks. We consider the hierarchical state-transition diagram approach, using the ASTDs. ASTDs allow a graphical and modular representation of a specification that facilitates maintenance and understanding of rules. We extend the ASTD notation with new features to represent complex attacks. Next, we specify several attacks with the extended notation and run the resulting specifications on event streams using an interpreter to identify attacks. We also evaluate the performance of the interpreter with industrial tools such as Snort and Zeek. Then, we build a compiler in order to generate executable code from an ASTD specification, able to efficiently identify sequences of events
31
Monmege, Benjamin. "Specification and verification of quantitative properties : expressions, logics, and automata." Thesis, Cachan, Ecole normale supérieure, 2013. http://www.theses.fr/2013DENS0039/document.
Full textAbstract:
La vérification automatique est aujourd'hui devenue un domaine central de recherche en informatique. Depuis plus de 25 ans, une riche théorie a été développée menant à de nombreux outils, à la fois académiques et industriels, permettant la vérification de propriétés booléennes - celles qui peuvent être soit vraies soit fausses. Les besoins actuels évoluent vers une analyse plus fine, c'est-à-dire plus quantitative. L'extension des techniques de vérification aux domaines quantitatifs a débuté depuis 15 ans avec les systèmes probabilistes. Cependant, de nombreuses autres propriétés quantitatives existent, telles que la durée de vie d'un équipement, la consommation énergétique d'une application, la fiabilité d'un programme, ou le nombre de résultats d'une requête dans une base de données. Exprimer ces propriétés requiert de nouveaux langages de spécification, ainsi que des algorithmes vérifiant ces propriétés sur une structure donnée. Cette thèse a pour objectif l'étude de plusieurs formalismes permettant de spécifier de telles propriétés, qu'ils soient dénotationnels - expressions régulières, logiques monadiques ou logiques temporelles - ou davantage opérationnels, comme des automates pondérés, éventuellement étendus avec des jetons. Un premier objectif de ce manuscript est l'étude de résultats d'expressivité comparant ces formalismes. En particulier, on donne des traductions efficaces des formalismes dénotationnels vers celui opérationnel. Ces objets, ainsi que les résultats associés, sont présentés dans un cadre unifié de structures de graphes. Ils peuvent, entre autres, s'appliquer aux mots et arbres finis, aux mots emboîtés (nested words), aux images ou aux traces de Mazurkiewicz. Par conséquent, la vérification de propriétés quantitatives de traces de programmes (potentiellement récursifs, ou concurrents), les requêtes sur des documents XML (modélisant par exemple des bases de données), ou le traitement des langues naturelles sont des applications possibles. On s'intéresse ensuite aux questions algorithmiques que soulèvent naturellement ces résultats, tels que l'évaluation, la satisfaction et le model checking. En particulier, on étudie la décidabilité et la complexité de certains de ces problèmes, en fonction du semi-anneau sous-jacent et des structures considérées (mots, arbres...). Finalement, on considère des restrictions intéressantes des formalismes précédents. Certaines permettent d'étendre l'ensemble des semi-anneau sur lesquels on peut spécifier des propriétés quantitatives. Une autre est dédiée à l'étude du cas spécial de spécifications probabilistes : on étudie en particulier des fragments syntaxiques de nos formalismes génériques de spécification générant uniquement des comportements probabilistes<br>Automatic verification has nowadays become a central domain of investigation in computer science. Over 25 years, a rich theory has been developed leading to numerous tools, both in academics and industry, allowing the verification of Boolean properties - those that can be either true or false. Current needs evolve to a finer analysis, a more quantitative one. Extension of verification techniques to quantitative domains has begun 15 years ago with probabilistic systems. However, many other quantitative properties are of interest, such as the lifespan of an equipment, energy consumption of an application, the reliability of a program, or the number of results matching a database query. Expressing these properties requires new specification languages, as well as algorithms checking these properties over a given structure. This thesis aims at investigating several formalisms, equipped with weights, able to specify such properties: denotational ones - like regular expressions, first-order logic with transitive closure, or temporal logics - or more operational ones, like navigating automata, possibly extended with pebbles. A first objective of this thesis is to study expressiveness results comparing these formalisms. In particular, we give efficient translations from denotational formalisms to the operational one. These objects, and the associated results, are presented in a unified framework of graph structures. This permits to handle finite words and trees, nested words, pictures or Mazurkiewicz traces, as special cases. Therefore, possible applications are the verification of quantitative properties of traces of programs (possibly recursive, or concurrent), querying of XML documents (modeling databases for example), or natural language processing. Second, we tackle some of the algorithmic questions that naturally arise in this context, like evaluation, satisfiability and model checking. In particular, we study some decidability and complexity results of these problems depending on the underlying semiring and the structures under consideration (words, trees...). Finally, we consider some interesting restrictions of the previous formalisms. Some permit to extend the class of semirings on which we may specify quantitative properties. Another is dedicated to the special case of probabilistic specifications: in particular, we study syntactic fragments of our generic specification formalisms generating only probabilistic behaviors
32
Morin-Allory, Katell. "Vérification Formelle dans le Modèle Polyédrique." Phd thesis, Université Rennes 1, 2004. http://tel.archives-ouvertes.fr/tel-00011522.
Full textAbstract:
Les travaux présentés dans ce document sont orientés vers la vérification formelle de propriétés de sûreté dans le cadre de la conception des systèmes enfouis. Nous nous plaçons dans le formalisme du modèle polyédrique, combinaison des systèmes d'équations récurrentes affines avec les polyèdes entiers. Ce modèle permet de faire de la synthèse de haut niveau pour générer des architectures parallèles à partir de la description d'un système régulier dont les dimensions sont définies par des paramètres symboliques. Nous nous intéressons à la vérification de propriétés de sûreté portant sur des signaux booléens de contrôle, générés ou introduits manuellement lors de la synthèse. Les propriétés sur de tels signaux seront appelées propriétés de contrôle. Nous montrons dans ce document que le modèle polyédrique est adapté pour la vérification formelle de propriétés de contrôle.<br /> Dans ce travail, nous développons une "logique polyédrique" qui nous permet de spécifier et prouver des propriétés dans le modèle polyédrique. La syntaxe et la sémantique des formules logiques s'appuient sur celles d'un langage de description de systèmes d'équations récurrentes affines sur des domaines polyédriques. Les règles de déduction sont de différents types : des règles "classiques" sur les connecteurs logiques, des règles de réécriture et des règles induites par des calculs dans le modèle. Nous développons des algorithmes pour automatiser la construction des preuves, ainsi que des techniques heuristiques permettant d'accélérer cette construction. Ces algorithmes nous permettent de prouver des propriétés simples, comme par exemple la propriété qu'un signal vaut toujours vrai pour un ensemble de processeurs et une durée déterminés. Nous présentons ensuite et commençons à développer des pistes afin d'enrichir notre logique pour exprimer des propriétés plus complexes, comme par exemple des propriétés d'exclusion mutuelle. Nous présentons quelques tactiques de preuve pour ces propriétés plus riches.
33
Cachera, David. "Validation formelle des langages à parallélisme de données." Phd thesis, École normale supérieure de Lyon - ENS Lyon, 1998. http://tel.archives-ouvertes.fr/tel-00425390.
Full textAbstract:
Le calcul massivement parallèle a connu durant ces deux dernières décennies un fort développement. Les efforts dans ce domaine ont d'abord surtout été orientés vers les machines, plutôt qu'à la définition de langages adaptés au parallélisme massif. Par la suite, deux principaux modèles de programmation ont émergé : le parallélisme de contrôle et le parallélisme de données. Le premier a connu un vif succès. Dans ce modèle cependant, les applications massivement parallèles s'avèrent difficiles à concevoir et peu fiables, compte tenu du grand nombre de processus envisagés. En revanche, le parallélisme de données paraît aujourd'hui être un bon compromis entre les besoins des utilisateurs et les contraintes imposées par les architectures parallèles. Dans cette thèse, nous nous sommes intéressé à la validation formelle des langages à parallélisme de données. L'idée est de tirer parti de la relative simplicité de ce modèle de programmation pour développer des méthodes semblables à celles déjà éprouvées dans le cadre des langages scalaires classiques. La première partie du travail effectué concerne un langage data-parallèle simple, de type impératif. Nous avons montré qu'il était possible de définir un système de preuve complet pour ce langage, inpiré de la logique de Hoare. L'étude théorique nous a permis en outre de définir une méthodologie pratique de preuve par annotations, semblable à celle utilisée pour les langages scalaires. Nous nous sommes ensuite tourné vers le langage d'équations récurrentes Alpha. Il s'avérait nécessaire de définir pour ce langage un cadre formel de validation, plus riche que le système de transformations existant ne permettant que des preuves par équivalence. Nous avons défini un modèle d'exécution par l'intermédiaire d'une sémantique opérationnelle, et une méthodologie de preuve. Celle-ci utilise des invariants qui sont raffinés à partir d'une traduction du programme dans un langage logique jusqu'à l'obtention de la propriété voulue.
34
Gascon, Régis. "Spécification et vérification de propriétés quantitatives sur des automates à contraintes." Phd thesis, École normale supérieure de Cachan - ENS Cachan, 2007. http://tel.archives-ouvertes.fr/tel-00441504.
Full textAbstract:
L'utilisation omniprésente des systèmes informatiques impose de s'assurer de leur bon fonctionnement. Dans ce but, les méthodes de vérification formelle permettent de suppléer les simulations qui ne peuvent être complètement exhaustives du fait de la complexité croissante des systèmes. Le model checking fait partie de ces méthodes et présente l'avantage d'être complètement automatisée. Cette méthode consiste à développer des algorithmes pour vérifier qu'une spécification exprimée la plupart du temps sous la forme d'une formule logique est satisfaite par un modèle du système. Les langages historiques de spécification utilisent comme formules atomiques des variables propositionnelles qui permettent d'exprimer principalement des propriétés portant sur les états de contrôle du modèle. Le but de cette thèse est de vérifier des propriétés plus riches portant sur diverses données manipulées par les modèles: des compteurs, des horloges ou des queues. Ces données peuvent prendre une infinité de valeurs et induisent donc des modèles avec un nombre infini d'états. Nous définissons un cadre général pour l'extension des logiques temporelles avec des contraintes permettant de comparer la valeur des variables a différents états de l'exécution. Nous établissons des résultats de décidabilité et complexité pour des problèmes de model checking impliquant diverses instances de ces extensions. Nous privilégions pour cela l'approche à base d'automates en combinant des constructions connues pour les logiques propositionnelles classiques avec des méthodes d'abstraction des modèles dont les variables sont interprétées dans des domaines infinis.
35
Diab, Hassan. "Évaluation de méthodes formelles de spécification." Thesis, National Library of Canada = Bibliothèque nationale du Canada, 1999. http://www.collectionscanada.ca/obj/s4/f2/dsk1/tape7/PQDD_0020/MQ56896.pdf.
Full text
36
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 textAbstract:
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.
37
Hamon-Keromen, Arnaud. "Définition d'un langage et d'une méthode pour la description et la spécification d'IHM post-W. I. M. P. Pour les cockpits interactifs." Toulouse 3, 2014. http://thesesups.ups-tlse.fr/2590/.
Full textAbstract:
Avec l'apparition de nouvelles technologies comme l'iPad, etc. , nous rencontrons dans les logiciels grand public des interfaces de plus en plus riches et innovantes. Ces innovations portent à la fois sur la gestion des entrées (e. G. écrans multi-touch) et sur la gestion des sorties (e. G. Affichage). Ces interfaces sont catégorisées de type post-WIMP et permettent d'accroitre la bande passante entre l'utilisateur et le système qu'il manipule. Plus précisément elles permettent à l'utilisateur de fournir plus rapidement des commandes au système et au système de présenter plus d'informations à l'utilisateur lui permettant par là-même de superviser des systèmes de complexité accrue. L'adoption par le grand public et le niveau de maturité de ces technos permet d'envisager leur intégration dans les systèmes critiques (comme les cockpits ou de façon plus générale les systèmes de commande et contrôle). Toutefois les aspects logiciels liés à ces technologies sont loin d'être maîtrisés comme le démontrent les nombreux dysfonctionnements rencontrés par leurs utilisateurs. Alors que ces derniers peuvent être tolérés pour des applications de jeux ou de divertissement elles ne sont pas acceptables dans le domaine des systèmes critiques présentés précédemment. La problématique de cette thèse porte précisément sur le développement de méthodes, langages, techniques et outils pour la conception et le développement de systèmes interactifs innovants et fiables. La contribution de cette thèse porte sur l'extension d'une notation formelle : ICO (Objets Coopératifs Interactifs) pour décrire de manières exhaustive et non ambiguë les techniques d'interactions multi-touch et la démonstrabilité de son application dans le cadre des applications multi-touch civils. Nous proposons en plus de cette notation, une méthode pour la conception et la validation de systèmes interactifs offrants des interactions multi-touch à leurs utilisateurs. Le fonctionnement de ces systèmes interactifs est basé sur une architecture générique permettant une structuration des modèles allant de la partie matérielle des périphériques d'entrées jusqu' à la partie applicative pour la commande et le contrôle de ces systèmes. Cet ensemble de contribution est appliqué sur un ensemble d'étude de ca dont la plus significative est une application de gestion météo pour un avion civil<br>With the advent of new technologies such as the iPad, general public software feature richer and more innovative interfaces. These innovations are both on the input layer (e. G. Multi-touch screens) and on the output layer (e. G. Display). These interfaces are categorized as post-W. I. M. P. Type and allow to increase the bandwidth between the user and the system he manipulates. Specifically it allows the user to more quickly deliver commands to the system and the system to present more information to the user enabling him managing increasingly complex systems. The large use in the general public and the level of maturity of these technologies allows to consider their integration in critical systems (such as cockpits or more generally control and command systems). However, the software issues related to these technologies are far from being resolved judging by the many problems encountered by users. While the latter may be tolerated for gaming applications and entertainment, it is not acceptable in the field of critical systems described above. The problem of this thesis focuses specifically on the development of methods, languages, techniques and tools for the design and development of innovative and reliable interactive systems. The contribution of this thesis is the extension of a formal notation: ICO (Interactive Cooperative Object) to describe in a complete and unambiguous way multi-touch interaction techniques and is applied in the context of multi-touch applications for civilians aircrafts. We provide in addition to this notation, a method for the design and validation of interactive systems featuring multi-touch interactions. The mechanisms of these interactive systems are based on a generic architecture structuring models from the hardware part of the input devices up to the application part for the control and monitoring of these systems. This set of contribution is applied on a set of case studies, the most significant being an application for weather management in civilian aircrafts
38
Tripakis, Stavros. "L'analyse formelle des systèmes temporisés en pratique." Phd thesis, Université Joseph Fourier (Grenoble), 1998. http://tel.archives-ouvertes.fr/tel-00004907.
Full textAbstract:
Dans cette thèse nous proposons un cadre formel complet pour l'analyse des systèmes temporisés, avec l'accent mis sur la valeur pratique de l'approche. Nous décrivons des systèmes comme des automates temporisés et nous exprimons les propriétés en logiques temps-réel. Nous considérons deux types d'analyse. Vérification : étant donnés un système et une propriété, vérifier que le système satisfait la propriété. Synthèse de contrôleurs : étant donnés un système et une propriété, restreindre le système pour qu'il satisfasse la propriété. Pour rendre l'approche possible malgré la difficulté théorique des problèmes, nous proposons : Des abstractions pour réduire l'espace d'états concret en un espace abstrait beaucoup plus petit qui, pourtant, préserve toutes les propriétés qui nous intéressent. Des techniques efficaces pour calculer et explorer l'espace d'états abstrait. Nous définissons des bisimulations et simulations faisant abstraction du temps et nous étudions les propriétés qu'elles préservent. Pour les bisimulations, l'analyse consiste à générer d'abord l'espace abstrait, et ensuite l'utiliser pour vérifier des propriétés sur l'espace concret. Pour les simulations, la génération et la vérification se font en même temps (à-la-volée). Un algorithme à-la-volée est aussi développé pour la synthèse de contrôleurs. Pour aider l'utilisateur à sa compréhension du système, nous produisons des séquences diagnostiques concrètes. Nous avons implanté nos méthodes dans Kronos, l'outil d'analyse temps-réel de Verimag, et nous avons traité un nombre d'études de cas réalistes parmi lesquelles le protocole FRP-DT de réservation rapide de débit pour les réseaux ATM (dans le cadre d'une coopération scientifique avec le CNET), le protocole de détection de collisions dans un réseaux à accès multiple de Band&Olufsen, l'ordonnancement de tâches temps-réel périodiques, la cohérence et l'ordonnancement des documents multimédia, ainsi qu'un nombre d'études de cas benchmarks, telles que le protocole d'exclusion mutuelle de Fischer, les protocoles de communication CSMA/CD et FDDI.
39
Defossez, François. "Modélisation discrète et formelle des exigences temporelles pour la validation et l’évaluation de la sécurité ferroviaire." Thesis, Ecole centrale de Lille, 2010. http://www.theses.fr/2010ECLI0004/document.
Full textAbstract:
Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit<br>The introduction of new European standards for railway safety, coupled with an increasing use of software technology changes the method of development of critical railway systems. Indeed, new systems have to be at least as good as the previous ones. Therefore the appropriate safety level of critical systems has to be proved in order to obtain the necessary approval from the authorities. Accordingly a high level of reliability and correctness must be reached by the use of mathematical proofs and then formal methods. We focus on the treatment of the temporal requirements in the level crossing case study which is modelled with p-time Petri nets, and on the translation of this model in a more formal way by using the B method. This paper introduces a methodology to analyse the safety of timed discrete event systems. First, our goal is to take out the forbidden state highlighted by a p-time Petri net modelling. This model deals with the requirements of the considered system and has to contain all the constraints that have to be respected. Then we aim at describing a process identified as a solution of the system functioning. This method consists in exploring all the possible behaviours of the system by means of the construction of state classes. Finally, we check if the proposed process corresponds to the requirements model previously built.Our case-study is the level crossing, a critical component for the safety of railway systems
40
Matoussi, Abderrahman. "Construction de spécifications formelles abstraites dirigée par les buts." Thesis, Paris Est, 2011. http://www.theses.fr/2011PEST1036/document.
Full textAbstract:
Avec la plupart des méthodes formelles, un premier modèle peut être raffiné formellement en plusieurs étapes, jusqu'à ce que le raffinement final contienne assez de détails pour une implémentation. Ce premier modèle est généralement construit à partir de la description des besoins obtenue dans la phase d'analyse des exigences. Cette transition de la phase des exigences à la phase de spécification formelle est l'une des étapes les plus délicates dans la chaîne de développement formel. En fait, la construction de ce modèle initial exige un niveau élevé de compétence et beaucoup de pratique, d'autant qu'il n'existe pas de processus bien défini pour aider les concepteurs. Parallèlement à ce problème, il s'avère également que les exigences non-fonctionnelles sont largement marginalisées dans le processus de développement logiciel. Les pratiques industrielles actuelles consistent généralement à spécifier seulement les exigences fonctionnelles durant les premières phases de ce processus et à laisser la prise en compte des exigences non-fonctionnelles au niveau de l'implémentation. Pour surmonter ces problèmes, la thèse vise à définir un couplage entre un modèle d'exigences exprimé en SysML/KAOS et des spécifications formelles abstraites, tout en garantissant une distinction entre les exigences fonctionnelles et non-fonctionnelles dès la phase d'analyse des exigences. Pour cela, la thèse propose tout d'abord deux approches différentes (l'une dédiée au B classique et l'autre à Event-B) dans lesquelles des modèles formels abstraits sont construits progressivement à partir du modèle de buts fonctionnels SysML/KAOS. La thèse se focalise par la suite sur l'approche dédiée à Event-B afin de la compléter et l'enrichir en se servant de deux autres modèles SysML/KAOS qui décrivent les buts non-fonctionnels et leurs impacts sur les buts fonctionnels. Nous présentons différentes manières permettant d'injecter ces buts non-fonctionnels et leurs impacts dans les modèles abstraits Event-B déjà obtenus. Des liens de correspondance entre les buts non-fonctionnels et les différents éléments Event-B sont également établis afin de faciliter la gestion de l'évolution de ces buts. Les différentes approches proposées dans cette thèse ont été appliquées pour la spécification du composant de localisation qui est une partie critique d'un système de transport terrestre. L'approche dédiée à Event-B est implémentée dans l'outil SysKAOS2EventB, permettant ainsi de générer une architecture de raffinement Event-B à partir d'un modèle de buts fonctionnels SysML/KAOS. Cette mise en œuvre s'appuie principalement sur les technologies de transformation de modèles à modèles<br>With most of formal methods, an initial formal model can be refined in multiple steps, until the final refinement contains enough details for an implementation. Most of the time, this initial model is built from the description obtained by the requirements analysis. Unfortunately, this transition from the requirements phase to the formal specification phase is one of the most painful steps in the formal development chain. In fact, building this initial model requires a high level of competence and a lot of practice, especially as there is no well-defined process to assist designers. Parallel to this problem, it appears that non-functional requirements are largely marginalized in the software development process. The current industrial practices consist generally in specifying only functional requirements during the first levels of this process and in leaving the consideration of non-functional requirements in the implementation level. To overcome these problems, this thesis aims to define a coupling between a requirement model expressed in SysML/KAOS and an abstract formal specification, while ensuring a distinction between functional and non-functional requirements from the requirements analysis phase. For that purpose, this thesis proposes firstly two different approaches (one dedicated to the classical B and the other to Event-B) in which abstract formal models are built incrementally from the SysML/KAOS functional goal model. Afterwards, the thesis focuses on the approach dedicated to Event-B in order to complete it and enrich it by using the two other SysML/KAOS models describing the non-functional goals and their impact on functional goals. We present different ways to inject these non-functional goals and their impact into the obtained abstract Event-B models. Links of correspondance between the non-functional goals and the different Event-B elements are also defined in order to improve the management of the evolution of these goals. The different approaches proposed in this thesis have been applied to the specification of a localization component which is a critical part of a land transportation system. The approach dedicated to Event-B is implemented in the SysKAOS2EventB tool, allowing hence the generation of an Event-B refinement architecture from a SysML/KAOS functional goal model. This implementation is mainly based on the model-to-model transformation technologies
41
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 textAbstract:
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<br>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
42
Bourdier, Tony. "Méthodes algébriques pour la formalisation et l'analyse de politiques de sécurité." Phd thesis, Université Henri Poincaré - Nancy I, 2011. http://tel.archives-ouvertes.fr/tel-00646401.
Full textAbstract:
Concevoir et mettre en œuvre des méthodes pour la spécification, l'analyse et la vérification de logiciels et de systèmes sont les principaux moteurs des activités de recherche présentées dans ce manuscrit. Dans ce cadre, nos travaux se positionnent dans la catégorie dite des méthodes formelles appartenant à la communauté plus large du génie logiciel. A l'interface des travaux théoriques et applicatifs, notre objectif est de contribuer aux méthodes permettant d'assurer la correction et la sûreté des systèmes (fonctionnalité, sécurité, fiabilité, ...) en développant ou en améliorant des langages de spécification, des techniques et des outils permettant leur analyse formelle. Dans ce but, nous nous sommes attaché dans cette thèse à proposer et à étudier un cadre formel permettant la définition de politiques de sécurité et la vérification de leurs propriétés. A cet effet, nous avons proposé un cadre pour la spécification de politiques de sécurité basé sur une approche modulaire dans laquelle une politique est vue comme la composition d'un modèle de sécurité et d'une configuration. Nous avons investigué les possibilités offertes par de telles spécifications lorsque les modèles sont exprimés au moyen de contraintes du premier ordre et les configurations au moyen de programmes logiques. En particulier, nous avons proposé un algorithme permettant de transformer une politique exprimée dans un modèle donné vers une autre politique équivalente (au sens où elle engendre les mêmes autorisations) exprimée dans un autre modèle. Dans un second temps, nous nous sommes proposé de tenir compte des aspects dynamiques de la configuration d'une politique vue comme un état du système sur lequel la politique est mise en œuvre et où chaque action est associée à une procédure de modification des états. Nous avons proposé un langage formel simple pour spécifier séparément les systèmes et les politiques de sécurité puis avons donné une sémantique des spécifications exprimées dans ce cadre sous la forme de systèmes de réécriture. Nous nous sommes ensuite attachés à montrer que les systèmes de réécriture obtenus permettent l'étude de propriétés de sécurité. Dans une troisième partie, nous nous sommes focalisé sur les mécanismes permettant la mise en œuvre de politiques de sécurité dans les réseaux. Dans ce cadre, nous avons proposé une spécification des firewalls et de leurs compositions basée sur les automates d'arbres et les systèmes de réécriture puis avons montré en quoi ces spécifications nous permettent d'analyser de façon automatique les politiques de sécurité sous-jacentes.
43
Raclet, Jean-Baptiste. "Quotient de spécifications pour la réutilisation de composants." Rennes 1, 2007. ftp://ftp.irisa.fr/techreports/theses/2007/raclet.pdf.
Full textAbstract:
Nous étudions la réutilisation d'un composant à un niveau comportemental plutôt qu’au niveau de sa signature grâce à une opération de quotient de spécifications. Partant des spécifications des comportements du composant à réutiliser et du système global désiré, cette opération calcule la spécification résiduelle caractérisant les systèmes qui, lorsqu'ils sont composés avec la composant de départ, satisfont la spécification globale. Nous définissons le quotient des spécifications modales lorsque la composition est le produit synchrone. Ce travail est étendu aux spécifications à ensembles d'acceptation afin de pouvoir exprimer certaines propriétés de vivacité locale. On définit aussi une opération de quotient lorsque la composition est le produit de mixage avec internalisation d'événements. Ainsi, le système synthétisé peut restreindre le comportement du composant réutilisé mais aussi contribuer à la réalisation de la spécification globale<br>The problem of component reuse is studied at a behavioral level rather than at a signature level. We address the behavioral reuse of a component by describing a quotient operation. Starting from the specifications of the behaviors of the component and of the desired overall system, this operation computes the residual specification characteristic of the systems that, when composed with the given component, satisfy the overall specification. We first define a quotient operation when behaviors are given by modal specifications and when the composition is the synchronous product. This work is then extended to acceptance specifications to deal with weak form of liveness properties. We also define a quotient operation when composition allows mixed product and internalization of events. As a result the synthesized system may restrict the behavior of the reused component and also directly contribute to the realization of the global specification
44
Konopacki, Pierre. "Modélisation de politiques de sécurité à l'aide de méthode de spécifications formelles." Phd thesis, Université Paris-Est, 2012. http://tel.archives-ouvertes.fr/tel-00786926.
Full textAbstract:
Le contrôle d'accès permet de spécifier une partie de la politique de sécurité d'un SI (système d'informations). Une politique de CA (Contrôle d'accès) permet de définir qui a accès à quoi et sous quelles conditions. Les concepts fondamentaux utilisés en CA sont : les permissions, les interdictions (ou prohibitions), les obligations et la SoD (séparation des devoirs). Les permissions permettent d'autoriser une personne à accéder à des ressources. Au contraire les prohibitions interdisent à une personne d'accéder à certaines ressources. Les obligations lient plusieurs actions. Elles permettent d'exprimer le fait qu'une action doit être réalisée en réponse à une première action. La SoD permet de sécuriser une procédure en confiant la réalisation des actions composant cette procédure à des agents différents. Différentes méthodes de modélisation de politiques de contrôle d'accès existent. L'originalité de la méthode EB3Sec issue de nos travaux repose sur deux points :- permettre d'exprimer tous les types de contraintes utilisées en CA dans un même modèle,- proposer une approche de modélisation basée sur les événements. En effet, aucune des méthodes actuelles ne présente ces deux caractéristiques, au contraire de la méthode EB3Sec. Nous avons défini un ensemble de patrons, chacun des patrons correspond à un type de contraintes de CA. Un modèle réalisé à l'aide de la méthode EB3Sec peut avoir différentes utilisations :- vérification et simulation,- implémentation. La vérification consiste à s'assurer que le modèle satisfait bien certaines propriétés, dont nous avons défini différents types. Principalement, les blocages doivent être détectés. Ils correspondent à des situations où une action n'est plus exécutable ou à des situations où plus aucune action n'est exécutable. Les méthodes actuelles des techniques de preuves par vérification de modèles ne permettent pas de vérifier les règles dynamiques de CA. Elles sont alors combinées à des méthodes de simulation. Une fois qu'un modèle a été vérifié, il peut être utilisé pour implémenter un filtre ou noyau de sécurité. Deux manières différentes ont été proposées pour réaliser cette implémentation : transformer le modèle EB3Sec vers un autre langage, tel XACML, possédant une implémentation ayant déjà atteint la maturité ou réaliser un noyau de sécurité utilisant le langage EB3Sec comme langage d'entrée
45
Mashkoor, Atif. "Ingénierie Formelle de Domaine: Des Spécifications à la Validation." Phd thesis, Université Nancy II, 2011. http://tel.archives-ouvertes.fr/tel-00614269.
Full textAbstract:
Le thème principal de cette recherche est d'étudier et développer des techniques pour la modélisation des systèmes où la sécurité est critique. Cette thèse est focalisé sur l'étape de la spécification du domaine où de tels systèmes vont fonctionner, et de sa validation. La contribution de cette thèse est double. D'abord, nous modélisons le domaine des transports terrestres, un bon candidat pour cette étude en raison de sa nature critique vis-à-vis de la sécurité, dans le cadre formel de B événementiel et proposent quelques directives pour cette activité. Ensuite, nous présentons une approche, basée sur les techniques de l'animation et des transformations, pour la validation par étapes des spécifications formelles.
46
Le, Guennec Alain. "Génie logiciel et méthodes formelles avec UML : : spécification, validation et génération de tests." Rennes 1, 2001. http://www.theses.fr/2001REN10156.
Full text
47
Boin, Clément. "Une méthode de sélection de tests à partir de spécifications algébriques." Phd thesis, Université d'Evry-Val d'Essonne, 2007. http://tel.archives-ouvertes.fr/tel-00419730.
Full textAbstract:
Les travaux de cette thèse s'inscrivent dans le cadre de la vérification des logiciels et plus particulièrement du test à partir de spécifications algébriques. La soumission d'un jeu de tests exhaustif pour trouver toutes les erreurs d'un programme est généralement impossible. Il faut donc sélectionner un jeu de tests le plus judicieusement possible. Nous avons donc donné une méthode de sélection de tests par dépliage des axiomes de spécifications conditionnelles positives (clauses de Horn pour la logique équationnelle). Celle-ci permet de partitionner le jeu exhaustif des tests. Nous utilisons pour cela un critère de sélection qui utilise les axiomes de la spécification et qui peut être appliqué plusieurs fois de suite. Pour garantir de bonnes propriétés sur ce critère de sélection, nous avons également donné un cadre général pour la normalisation d'arbre de preuve. Il fonctionne pour n'importe quel système formel, et permet d'unifier un grand nombre de résultats en logique.
48
Siala, Badr. "Décomposition formelle des spécifications centralisées Event-B : application aux systèmes distribués BIP." Thesis, Toulouse 3, 2017. http://www.theses.fr/2017TOU30268/document.
Full textAbstract:
Cette thèse a pour cadre scientifique la décomposition formelle des spécifications centrali- sées Event-B appliquée aux systèmes distribués BIP. Elle propose une démarche descendante de développement des systèmes distribués corrects par construction en combinant judicieu- sement Event-B et BIP. La démarche proposée comporte trois étapes : Fragmentation, Dis- tribution et Génération de code BIP. Les deux concepts clefs Fragmentation et Distribution, considérés comme deux sortes de raffinement automatique Event-B paramétrées à l'aide de deux DSL appropriés, sont introduits par cette thèse. Cette thèse apporte également une contribution au problème de la génération de code à partir d'un modèle Event-B issu de l'étape de distribution. Nous traitons aussi bien les aspects architecturaux que comportemen- taux. Un soin particulier a été accordé à l'outillage et l'expérimentation de cette démarche. Pour y parvenir, nous avons utilisé l'approche IDM pour l'outillage et l'application Hôtel à clés électroniques pour l'expérimentation<br>The scientific framework of this thesis is the formal decomposition of the centralized specifications Event-B applied to distributed systems based on the BIP (Behavior, Interaction, Priority) component framework. It suggets a top-down approach to the development of correct by construction distributed systems by judiciously combining Event-B and BIP. The proposed approach consists in three steps : Fragmentation, Distribution and Generation of BIP code. We introduce two key concepts, Fragmentation and Distribution, which are considered as two kinds of automatic refinement of Event-B models. They are parameterized using two appropriate DSL. This thesis also contributes to the problem of code generation from Event- B models resulting from the Distribution step. Accordingly, we deal with both architectural and behavioral aspects. A special care has been devoted to the implementation and the experimentation of this approach. To achieve this, we have used the IDM approach for tooling and the Electronic Hotel Key System for experimentation
49
Yazid, Sidi Mohamed. "Spécification formelle de commande numérique de machine-outil." Limoges, 1997. http://www.theses.fr/1997LIMO0014.
Full textAbstract:
La these vise a aborder, avec l'aide de methodes de genie logiciel, les specificites des commandes numeriques de machines-outils presentes dans l'industrie. Le premier chapitre est consacre a l'etablissement de la pre-specification d'une commande numerique, c'est a dire le decoupage du flux d'informations qui fait que l'on passe d'une donnee du programme piece au deplacement de l'outil. Le second chapitre presente les possibilites de la methode z a l'aide de deux exemples de nature informatique. Il presente ensuite les regles de passage de la pre-specification, etablie dans le premier chapitre, a une specification en z. Le troisieme chapitre utilise le decoupage obtenu en i pour donner une description formelle originale, a l'aide de schemas, de l'enchainement des operations executees pour une commande numerique elementaire. Sur cette description nous construisons de maniere progressive des operations plus complexes. La se voit l'interet des regles presentees dans le second chapitre pour la construction des modeles formels des differentes variantes du fonctionnement de la commande numerique. Dans le quatrieme chapitre, on montre l'interet de z pour la verification des specifications presentees dans le chapitre precedent. On fournit une methode permettant de reconnaitre l'execution par la machine (specifiee prealablement) d'une suite d'operations qui pourraient etre regroupees dans un cycle d'usinage. Le cinquieme chapitre introduit l'usage d'une extension de z permettant une traduction des schemas de z en langage objet. Il pallie au probleme de la structuration de la specification en z, et fournit un modele a la fois formel et modulaire du fonctionnement de la commande numerique.
50
Nebut, Mirabelle. "Réactions synchrones : spécification et analyse." Rennes 1, 2002. http://www.theses.fr/2002REN10061.
Full text