No description available.

<p> Earley's parsing algorithm is an O(n^3) algorithm for parsing according to any context-free grammar. Its theoretical importance stems from the fact that it was one of the first algorithms to achieve this time bound, but it has also seen success in compiler-compilers, theorem provers and natural language processing. It has an elegant structure, and its time complexity on restricted classes of grammars is often as good as specialized algorithms. Grammars with ϵ-productions, however, require special consideration, and have historically lead to inefficient and inelegant implementations.</p> <p> In this thesis, we develop the algorithm from specification using the B-Method. Through refinement steps, we arrive at a list-processing formulation, in which the problems with ϵ-productions emerge and can be understood. The development highlights the essential properties of the algorithm, and has also lead to the discovery of an implementation optimization. We end by giving a concept-test of the algorithm as a literate Pascal program.</p> / Thesis / Master of Computer Science (MCS)

Les propriétés que l’on souhaite exprimer sur les applications système d’information ne peuvent se restreindre aux propriétés statiques, dites propriétés d’invariance, qui portent sur des états du système pris au même moment. En effet, certaines propriétés, dites propriétés dynamiques, peuvent faire référence à l’état passé ou futur du système. Les travaux existants sur la vérification de telles propriétés utilisent généralement le model checking dont l’efficacité pour le domaine des systèmes d’information est plutôt réduite à cause de l’explosion combinatoire de l’espace des états. Aussi, les techniques, fondées sur la preuve, requièrent des connaissances assez avancées en termes de raisonnement mathématique et sont donc difficiles à mettre en œuvre d’autant plus que ces dernières ne sont pas outillées. Pour palier ces limites, nous proposons dans cette thèse des méthodes de vérification de propriétés dynamiques basées sur la preuve en utilisant la méthode formelle B. Nous nous intéressons principalement aux propriétés d’atteignabilité et de précédence pour lesquelles nous avons défini des méthodes de génération d’obligations de preuve permettant de les prouver. Une propriété d’atteignabilité permet d’exprimer qu’il existe au moins une exécution du système qui permet d’atteindre un état cible à partir d’un état initial donné. Par contre, la propriété de précédence permet de s’assurer qu’un état donné du système est toujours précédé par un autre état. Afin de rendre ces différentes approches opérationnelles, nous avons développé un outil support qui permet de décharger l’utilisateur de la tâche de génération d’obligations de preuve qui peut être longue et fastidieuse / The properties that we would like to express on data-intensive applications cannot be limited to static properties, called invariance properties, which depend on states taken at the same time. Indeed, some properties, called dynamic properties, may refer to the past or the future states of the system. Existing work on the verification of such properties typically use model checking whose effectiveness for data-intensive applications is rather limited due to the combinatorial explosion of the state space. In addition, the techniques, based on the proof, require fairly advanced knowledge and mathematical reasoning especially that they are not always supported by tools. To overcome these limitations, we propose in this thesis proof-based verification approaches that use the B formal method. We are mainly interested in reachability and precedence properties for which we defined formal rules to generate proof obligations that permit to discharge them. A reachability property expresses that there is at least one execution scenario that permits to reach a target state from a given initial state while a precedence property ensures that a given system state is always preceded by another state. To make these different approaches workable, we have developed a support tool that permits to discharge the users from tedious and error-prone tasks

Made available in DSpace on 2014-12-17T15:47:55Z (GMT). No. of bitstreams: 1 StephennsonSLG_DISSERT.pdf: 4909051 bytes, checksum: 2a9f94a42d9fc75bb16a1ff239148437 (MD5) Previous issue date: 2011-08-16 / This paper presents a contribution to the international Verified Software Repository effort through the formal specification of the microkernel FreeRTOS real-time system. Such specification was made in abstract level making use of the B method . For thus, properties of the microkernel were chosen and selected as specification requisites, which was constructed centered at the functionalities responsible for the utilization of these properties. This properties weres setting as specification requirements. The specification was constructed modeling the function of microkernel that implement this properties. This work intended to encourage the formal verification of FreeRTOS and also contribute to the formal creation of a microkernel real-time systems, based in FreeRTOS. Furthermore, this model brings a formal documentation point view of the microkernel, demonstrating features and how this internal states is changing. Finally, this work could be an example of specification of the actual system by the B method. / Este trabalho apresenta uma contribui??o para o esfor?o internacional do Verified Software Repository atrav?s da especifica??o formal da biblioteca de sistema de tempo real FreeRTOS. Tal especifica??o foi realizada de forma abstrata utilizando o m?todo B. Para isso, propriedades disponibilizadas por essa biblioteca foram elencadas e selecionadas como requisitos da especifica??o, a qual foi constru?da centrada nas funcionalidades respons?veis pela utiliza??o dessas propriedades. Com a modelagem desenvolvida pretende-se incentivar a verifica??o formal do FreeRTOS e tamb?m contribuir para a cria??o formal de uma biblioteca de sistemas de tempo real baseada na FreeRTOS. Al?m disso, tal modelagem traz uma documenta??o do ponto de vista formal do sistema, demonstrando como ocorrer internamente o seu funcionamento e serve como um exemplo da especifica??o de um sistema real pelo m?todo B.

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

Le travail de thèse présente une méthode de développement de systèmes automatisés basée sur les méthodes formelles B et TLA+. Le développement par raffinement est au cœur de la méthode proposée. Un système automatisé est modélisé par deux composants, un contrôlé formé par le dispositif physique et son environnement et un contrôleur pilotant ce dernier. Il est exprimé par un produit synchronisé sur les actions de ces deux composants. La première contribution de la thèse concerne la proposition d'une approche qui combine le B événementiel et le langage de modélisation TLA+ pour la vérification des propriétés de vivacité. Nous définissons une extension syntaxique et sémantique du B événementiel permettant d'exprimer des propriétés de vivacité. Nous développons un prototype pour la transformation d'un modèle B en un module TLA+ sur lequel nous effectuons la preuve des propriétés de vivacité avec le model checker TLC. Pour la vérification de ce type de propriétés sur des systèmes infinis, nous proposons l'utilisation des diagrammes de prédicats qui sont des abstractions des systèmes modélisés en TLA+. La deuxième contribution est la proposition d'une technique pour représenter explicitement le temps en B événementiel. Cette technique s'appuie sur la réalisation d'un entrelacement entre un processus qui gère le temps avec les autres processus du système. Le temps modélisé est discret et son écoulement est modélisé par des événements. Cette approche est assez différente des systèmes temporisés où l'on considère que le temps s'écoule indépendamment du système. Dans la troisième contribution, nous proposons une approche de développement des systèmes automatisés en utilisant la technique de composition où il s'agit de développer conjointement le contrôleur et le composant physique qu'il contrôle et appliquer le raffinement aussi bien sur le contrôleur que le contrôlé. Le raffinement est une technique de base des méthodes que nous proposons et si notre objectif est de construire des contrôleurs corrects, le critère de correction porte sur le comportement du système automatisé qui résulte de la composition du contrôleur et du contrôlé. Nous présentons également un théorème de compositionnalité qui indique sous quelles conditions il est possible de déduire que le composé des raffinements des contrôleur et contrôlé est un raffinement du composé des contrôleur et contrôlé abstraits. La dernière contribution porte sur la définition, la preuve et l'utilisation d'un patron de raffinement pour les processus continus dans des systèmes de production manufacturière. Ce type de patron prouvé permet d'utiliser l'abstraction discrète de l'effet d'un processus continu agissant pendant un certain temps / This thesis deals with the development of automated systems while following the formal methods B and TLA+. We propose a formal methodology based on the refinement paradigm to specify and verify the system that we model by two components: the controlled system representing the physical device and its environment, and the controller that controls the system. A synchronised product on the actions of these two components is applied to specify the automated system. As a first contribution, we propose an approach combining the event B method and the language TLA+ in order to verify liveness properties defined in user requirements. Inspired by the temporal logic of actions TLA, we first extend the event B notation to specify liveness properties and we give semantics of this extended syntax over traces. Second, we give transformation rules from a temporal B model into a TLA+ module. We present, in particular, our prototype system called B2TLA+, that we have developed to support this transformation. To consider infinite systems, we use predicate diagrams as abstractions of systems modelled with TLA+. To consider the real-time concept in automated systems, we propose as a second contribution a technique explicitly representing time in B event systems. This technique is based on an interleaving between any event handling time and the other system events. By considering the well known co-design technique, we propose as a third contribution a refinement-based composition technique keeping a separation between controller and controlled systems in order to build correct automated systems satisfying user requirements. We prove a compositionality theorem with respect to refinement to get an efficient approach to verify the refinement of a synchronized composition between components. We verify the refinement of a synchronized composition by verifying separately the refinement of each component. Finally, we define, prove and use in a case study as a fourth contribution the concept of a refinement pattern for continuous processes in manufacturing systems. Such proven pattern allows us to use the discrete abstraction of the effect of continuous processes operating for a while

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 / 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

Made available in DSpace on 2014-12-17T15:47:44Z (GMT). No. of bitstreams: 1 BrunoEGG.pdf: 1320681 bytes, checksum: 897ca75ef7f0e564e8588d949fcc67d5 (MD5) Previous issue date: 2007-11-19 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures / A tecnologia Java Card permite o desenvolvimento e execu??o de pequenas aplica??es embutidas em smart cards. Uma aplica??o Java Card ? composta por um cliente, externo ao cart?o, e por uma aplica??o contida no cart?o que implementa os servi?os dispon?veis ao cliente por meio de uma Application Programming Interface (API). Usualmente, essas aplica??es manipulam e armazenam informa??es importantes, tais como valores monet?rios ou dados confidenciais do seu portador. Sendo assim, faz-se necess?rio adotar um maior rigor no processo de desenvolvimento de uma aplica??o smart card, visando melhorar a sua qualidade e confiabilidade. O emprego de m?todos formais como parte desse processo ? um meio de se alcan?ar esses requisitos de qualidade. O m?todo formal B ?e um dentre os diversos m?todos formais para a especifica??o de sistemas. O desenvolvimento em B tem in?cio com a especifica??o funcional do sistema, continua com a aplica??o opcional de refinamentos ? especifica??o e, a partir do ?ltimo n?vel de refinamento, ? poss?vel a gera??o de c?digo para alguma linguagem de programa??o. O formalismo B conta com bom suporte de ferramentas e a sua aplica??o a Java Card mostra-se bastante adequada, uma vez que a especifica??o e desenvolvimento de APIs ?e o ponto forte de B. O m?todo BSmart aqui proposto visa promover o desenvolvimento rigoroso de aplica??es Java Card a partir da gera??o de c?digo da aplica??o com base em refinamentos da sua especifica??o formal descrita na nota??o B. O processo de desenvolvimento descrito no m?todo ? apoiado pela ferramenta BSmart, a qual constitui-se por alguns programas que automatizam cada etapa do m?todo; e por uma biblioteca de m?dulos B e classes Java Card que modelam tipos primitivos, classes essenciais da API Java Card e estruturas de dados reutiliz?veis

Made available in DSpace on 2014-12-17T15:48:00Z (GMT). No. of bitstreams: 1 SimoneOS_DISSERT_capa_ate_pag44.pdf: 4276014 bytes, checksum: c178262769ab9981c0bbfc10faf1c633 (MD5) Previous issue date: 2012-02-10 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers / O desenvolvimento de aplica??es para smart cards requer um alto grau de confiabilidade. M?todos formais fornecem meios para que esta confiabilidade seja alcan?ada. O m?todo e a ferramenta BSmart fornecem uma contribui??o para que o desenvolvimento para smart cards seja feito com o aux?lio do m?todo formal B, gerando c?digo Java Card a partir de especifica??es B. Para que o desenvolvimento com o BSmart seja efetivamente rigoroso sem sobrecarregar o usu?rio do m?todo ? importante que haja uma biblioteca de componentes reutiliz?veis feitos em B. O KitSmart tem como objetivo prover esse aux?lio. Um primeiro estudo sobre a composi??o dessa biblioteca foi tema de uma monografia de gradua??o do curso de Bacharelado em Ci?ncia da Computa??o da Universidade Federal do Rio Grande do Norte, feita por Thiago Dutra em 2006. Esta primeira vers?o do kit resultou na especifica??o dos tipos primitivos permitidos em Java Card (byte, short e boolean) em B e a cria??o de componentes reutiliz?veis para o desenvolvimento de aplica??es. Esta disserta??o prov? o aperfei?oamento do KitSmart com o acr?scimo da especifica??o da API Java Card em B, e um guia para o desenvolvimento de novos componentes. A API Java Card especificada em B, al?m de estar dispon?vel para ser usada no desenvolvimento de projetos, serve como documenta??o ao especificar restri??es de uso para cada classe da API. Os componentes reutiliz?veis correspondem a m?dulos para manipula??o de estruturas espec?ficas, como data e hora, por exemplo. Estes tipos de estruturas n?o est?o dispon?veis em B ou Java Card. Os componentes reutiliz?veis para Java Card s?o gerados a partir das especifica??es verificadas formalmente em B. O guia cont?m informa??es de consulta r?pida para especifica??o de diversas estruturas e como algumas situa??es foram contornadas para adaptar a orienta??o a objetos ao M?todo B. Este trabalho foi avaliado atrav?s de um estudo de caso feito com a ferramenta BSmart que faz uso da biblioteca KitSmart. Neste estudo de caso, ? poss?vel ver a contribui??o dos componentes em uma especifica??o B. Este kit dever? ser ?til tanto para usu?rios do m?todo B como para desenvolvedores de aplica??es Java Card em geral

Made available in DSpace on 2015-03-03T15:47:45Z (GMT). No. of bitstreams: 1 ValerioGMJpdf.pdf: 1265506 bytes, checksum: f1fe3ef975bfeb2fce1dad3319a33f34 (MD5) Previous issue date: 2009-09-09 / This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler. Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry / Este trabalho apresenta um m?todo de projeto proposta para veri ca??o formal do modelo funcional do software at? o n?vel da linguagem assembly. Esse m?todo ? fundamentada no m?todo B, o qual foi desenvolvido com o apoio e interesse da multinacional do setor de petr?leo e g?s British Petroleum (BP). A evolu??o dessa metodologia tem como objetivo contribuir na resposta de um importante problema, que pertence aos grandes desa os da computa??o, conhecido como The Verifying Compiler . Nesse contexto, o presente trabalho descreve um modelo formal do microcontrolador Z80 e um sistema real da ?rea de petr?leo. O modelo formal do Z80 foi desenvolvido e documentado, por ser um pr?-requisito para a veri ca??o at? n?vel de assembly. A m de validar e desenvolver a metodologia citada, ela foi aplicada em um sistema de teste de produ??o de po?os de petr?leo, o qual ? apresentado neste trabalho. Atualmente, algumas atividades s?o realizadas manualmente. No entanto, uma parte signifi cativa dessas atividades pode ser automatizada atrav?s de um compilador espec?fi co. Para esse m, a modelagem formal do microcontrolador e a modelagem do sistema de teste de produ??o fornecem conhecimentos e experi?ncias importantes para o projeto de um novo compilador. Em suma, esse trabalho deve melhorar a viabilidade de um dos mais rigorosos crit?rios de veri ca??o formal: acelerando o processo de verifica??o, reduzindo o tempo de projeto e aumentando a qualidade e con fian?a do produto de software final. Todas essas qualidades s?o bastante relevantes para sistemas que envolvem s?rios riscos ou exigem alta confian?a, os quais s?o muito comuns na ind?stria do petr?leo