Submitted by Automação e Estatística (sst@bczm.ufrn.br) on 2018-07-02T18:48:21Z No. of bitstreams: 1 DiegoDeAzevedoOliveira_DISSERT.pdf: 1039192 bytes, checksum: a387d372d3c8da2d66010f294542538a (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2018-07-04T13:18:52Z (GMT) No. of bitstreams: 1 DiegoDeAzevedoOliveira_DISSERT.pdf: 1039192 bytes, checksum: a387d372d3c8da2d66010f294542538a (MD5) / Made available in DSpace on 2018-07-04T13:18:53Z (GMT). No. of bitstreams: 1 DiegoDeAzevedoOliveira_DISSERT.pdf: 1039192 bytes, checksum: a387d372d3c8da2d66010f294542538a (MD5) Previous issue date: 2018-02-05 / Softwares precisam ser seguros e corretos. Partindo desse pressuposto, novas tecnologias e técnicas são desenvolvidas para comprovar as competências de um programa. Essa necessidade de segurança se torna mais relevante ao tratar de softwares que atuam em sistemas críticos, como os sistemas ferroviário e aeroviário. A utilização de métodos formais na construção de software busca solucionar o problema. Ao utilizar o método formal B através da plataforma Atelier-B, e após provar os componentes de um projeto é necessária a tradução para a linguagem desejada. Essa tradução ocorre por meio de tradutores e compiladores B. Habitualmente, o processo de compilação em compiladores maduros é seguro, porém não estão completamente livres de falhas e eventualmente erros são encontrados. Ao expandir essa afirmação para tradutores B é necessário cautela, uma vez que esses não são tão comuns e utilizados quanto compiladores que circulam há mais tempo no mercado. Testes de software podem ser utilizados para realizar a análise da tradução. Através de critérios de cobertura é possível inferir o nível de qualidade do software e facilitar a detecção de falhas. Realizar a checagem da cobertura e testes em software pode exigir bastante esforço e tempo, principalmente ao serem realizados manualmente. Para sanar essa demanda, a ferramenta BTestBox visa analisar, de maneira automática, a cobertura atingida por implementações B desenvolvidas através do Atelier-B. BTestBox também testa automaticamente as traduções feitas a partir de implementações B. Para isso, BTestBox utiliza os casos de teste gerados para a verificação de cobertura e compara os valores esperados de saída com os encontrados após a tradução. O processo feito por BTestBox é todo automático e pode ser utilizado a partir do Atelier-B via instalação de plugin com uma interface simples. Essa dissertação apresenta a ferramenta BTestBox. BTestBox foi testado através de pequenas implementações B com os elementos gramaticais possíveis da linguagem B. BTestBox apresenta funcionalidade e vantagens para programadores que utilizam o método formal B. / Software needs to be safe and run smoothly. From that assumption, new technologies and techniques are developed to test the quality of a program. This is more relevant when developing critical systems, such as railways and avionics control systems. Formal methods try to adress this need. When using B in Atelier-B, after proving the components of a project is necessary to translate to the desired language, a translation is made by using B translators and compilers. Usually, the process of compilation is safe when perfomed by mature compilers although they are not free of errors and bugs often crop up. The same reliability is not always observed in B translators since they have been on the market for less time. Software testing may solve and be used to perform the analyses of the translated code. From coverage criteria, it is possible to infer quality of a piece of software and detect bugs. This process is hard and time-consuming, mainly if it is perfomed manually. To address this problem, the BTestBox tool aims to analyze automatically the coverage of B implementations built through Atelier-B. BTestBox also automatically tests the translation from B implementations. For this, BTestBox uses the same test case generated to verify the coverage and compare the output expected values with the values found in the translation. This process is fully automatic and may be started from Atelier-B with a plugin. This thesis presents the tool BTestBox. The tool is a solution to the problems exposed in the previous paragraph. BTestBox was tested with small B implementations and all gramatical elements from B language. It offers various functionalities and advantages to developers that use the B-Method.

Cette thèse porte sur la vérification des règles ajoutées de l'Atelier B en utilisant une plate-forme appelée BCARe qui repose sur un plongement de la théorie sous-jacente à la méthode B (théorie de B) dans l'assistant à la preuve Coq. En particulier, nous proposons trois approches pour prouver la validité d'une règle, ce qui revient à prouver une formule exprimée dans la théorie de B. Ces trois approches ont été évaluées sur les règles de la base de règles de SIEMENS IC-MOL. La première approche dite autarcique est développée avec le langage de tactiques de Coq Ltac.  Elle repose sur une première étape qui consiste à déplier tous les opérateurs ensemblistes pour obtenir une formule de la logique du premier ordre. Puis nous appliquons une procédure de décision qui met en oeuvre une heuristique naïve en ce qui concerne les instanciations. La deuxième approche, dite sceptique,appelle le prouveur automatique de théorèmes Zenon après avoir effectué l'étape de normalisation précédente. Nous vérifions ensuite les preuves trouvées par Zenon dans le plongement profond de B en Coq.  La troisième approche évite l'étape de normalisation précédente grâce à une extension de Zenon utilisant des règles d'inférence spécifiques à la théorie de B. Ces règles sont obtenues grâce à la technique de superdéduction. Cette dernière approche est généralisée en une extension de Zenon à toute théorie grâce à un calcul dynamique des règles de superdéduction. Ce nouvel outil, appelé Super Zenon, peut par exemple prouver des problèmes issus de la bibliothèque de problèmes TPTP. / The purpose of this thesis is the verification of Atelier B added rules using the framework named BCARe which relies on a deep embedding of the B theory within the logic of the Coq proof assistant. We propose especially three approaches in order to prove the validity of a rule, which amounts to prove a formula expressed in the B theory. These three approaches have been assessed on the rules coming from the rule database maintained by Siemens IC-MOL.  To do so, the first approach, so-called autarkic approach, is developed thanks to the Coq tactic language, Ltac. It rests upon a first step which consists in unfolding the set operators so as to obtain a first order formula.  A decision procedure which implements an heuristic is applied afterwards to deal with instantiation.  We propose a second approach, so-called skeptic approach, which uses the automated first order theorem prover Zenon, after the previous normalization step has been applied.  Then we verify the Zenon proofs in the deep embedding of B in Coq. A third approach consists in using anextension of Zenon to the B method thanks to the superdeduction. Superdeduction allows us to add the axioms of the B theory by means of deduction rules in the proof mechanism of Zenon. This last approach is generalized in an extension of Zenon to every theory thanks to a dynamic calculus of the superdeduction rules. This new tool, named Super Zenon, is able to prove problems coming from the problem library TPTP, for example.