1 |
Beta: a B based testing approach / BETA: uma abordagem de testes baseada em BMatos, Ernesto Cid Brasil de 14 April 2016 (has links)
Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-10-11T20:48:07Z
No. of bitstreams: 1
ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-10-14T00:17:49Z (GMT) No. of bitstreams: 1
ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5) / Made available in DSpace on 2016-10-14T00:17:49Z (GMT). No. of bitstreams: 1
ErnestoCidBrasilDeMatos_TESE.pdf: 4062332 bytes, checksum: 09e4f284f102ad1088f37213e8e53d6f (MD5)
Previous issue date: 2016-04-14 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior (CAPES) / Sistemas de software esta?o presentes em grande parte das nossas vidas atualmente e, mais do que nunca, eles requerem um alto ni?vel de confiabilidade. Existem va?rias te?cnicas de Ver- ificac?a?o e Validac?a?o (V&V) de software que se preocupam com controle de qualidade, segu- ranc?a, robustez e confiabilidade; as mais conhecidas sa?o Testes de Software e Me?todos For- mais. Me?todos formais e testes sa?o te?cnicas que podem se complementar. Enquanto me?to- dos formais prove?em mecanismos confia?veis para raciocinar sobre o sistema em um ni?vel mais abstrato, te?cnicas de teste ainda sa?o necessa?rias para uma validac?a?o mais profunda e sa?o frenquentemente requeridas por orga?os de certificac?a?o. Levando isto em considerac?a?o, BETA prove? uma abordagem de testes baseada em modelos para o Me?todo B, suportada por uma ferramenta, que e? capaz de gerar testes de unidade a partir de ma?quinas abstratas B. Nesta tese de doutorado apresentamos melhorias realizadas em BETA e novos estudos de caso realizados para avalia?-la. Dentre as melhorias, integramos crite?rios de cobertura lo?gicos a? abordagem, revisamos os crite?rios de cobertura baseados em espac?o de entrada que ja? eram suportados e aperfeic?oamos as u?ltimas etapas do processo de gerac?a?o de testes. A abordagem agora suporta a gerac?a?o automa?tica de dados para os ora?culos e prea?mbulos para os casos de teste; ela tambe?m possui uma funcionalidade para concretizac?a?o dos da- dos de teste e um mo?dulo para gerar scripts de teste executa?veis automaticamente. Outro objetivo desta tese foi realizar estudos de caso mais complexos utilizando BETA e avaliar a qualidade dos casos de teste que a abordagem produz. Estes estudos de caso foram os primeiros a avaliar o processo de gerac?a?o de testes por completo, desde a especificac?a?o dos casos de teste ate? a sua implementac?a?o e execuc?a?o. Em nossos u?ltimos experimentos, analisamos a qualidade dos casos de teste gerados por BETA, considerando cada crite?rio de cobertura suportado, utilizando me?tricas de cobertuda de co?digo como cobertura de in- struc?o?es e ramificac?o?es. Tambe?m utilizamos testes de mutac?a?o para avaliar a capacidade dos casos de teste de detectar faltas na implementac?a?o dos modelos. O resultados obtidos foram promissores mostrando que BETA e? capaz de detectar faltas introduzidas por progra- madores ou geradores de co?digo e que a abordagem pode obter bons resultados de cobertura para a implementac?a?o de um sistema baseado em modelos B. / Software systems are a big part of our lives and, more than ever, they require a high level of
reliability. There are many software Verification and Validation (V&V) techniques that are
concerned with quality control, security, robustness, and reliability; the most widely known
are Software Testing and Formal Methods. Formal methods and testing are techniques that
can complement each other. While formal methods provide sound mechanisms to reason
about the system at a more abstract level, testing techniques are still necessary for a more
in-depth validation of the system and are often required by certification standards. Taking
this into consideration, BETA provides a tool-supported, model-based testing approach for
the B Method that is capable of generating unit tests from abstract B machines. In this thesis,
we present improvements made in the BETA approach and tool, and new cases studies
used to evaluate them. Among these improvements, we integrated logical coverage criteria
into the approach, reviewed the input space criteria that was already supported, and enhanced
the final steps of the test generation process. The approach now has support for
automatic generation of oracle data and test case preambles, it has a feature for test data
concretization, and a module that automatically generates executable test scripts. Another
objective of this thesis was to perform more complex case studies using BETA and assess the
quality of the test cases it produces. These case studies were the first to evaluate the test
generation process as a whole, from test case design to implementation and execution. In
our last experiments, we assessed the quality of the test cases generated by BETA, considering
each coverage criteria it supports, using code coverage metrics such as statement and
branch coverage. We also used mutation testing to evaluate the ability of the generated test
cases to identify faults in the model?s implementation. The results obtained were promising,
showing that BETA is capable of detecting faults introduced by a programmer or code
generation tool and that it can achieve good coverage results for a system?s implementation
based on a B model.
|
2 |
JCML - Java Card Modeling Language: Defini??o e Implementa??oSouza Neto, Pl?cido Ant?nio de 06 September 2007 (has links)
Made available in DSpace on 2014-12-17T15:47:43Z (GMT). No. of bitstreams: 1
PlacidoASN.pdf: 652214 bytes, checksum: b7912104bf8e3ec91262c75b9ef5d36b (MD5)
Previous issue date: 2007-09-06 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Formal methods should be used to specify and verify on-card software in Java Card applications. Furthermore, Java Card programming style requires runtime verification of all input conditions for all on-card methods, where the main goal is to preserve the data in the card. Design by contract, and in particular, the JML language, are an option for this kind of development and verification, as runtime verification is part of the Design by contract method implemented by JML. However, JML and its currently available tools for runtime verification were not designed with Java Card limitations in mind and are not Java Card compliant. In this thesis, we analyze how much of this situation is really intrinsic of
Java Card limitations and how much is just a matter of a complete re-design of JML and its tools. We propose the requirements for a new language which is Java Card compliant
and indicate the lines on which a compiler for this language should be built. JCML strips from JML non-Java Card aspects such as concurrency and unsupported types. This would
not be enough, however, without a great effort in optimization of the verification code generated by its compiler, as this verification code must run on the card. The JCML compiler, although being much more restricted than the one for JML, is able to generate Java Card compliant verification code for some lightweight specifications. As conclusion, we present a Java Card compliant variant of JML, JCML (Java Card Modeling Language), with a preliminary version of its compiler / M?todos formais poderiam ser usados para especificar e verificar software on-card em aplica??es Java Card. O estilo de programa??o para smart cards requer verifica??o
em tempo de execu??o para condi??es de entrada em todos os m?todos Java Card, onde o objetivo principal ? preservar os dados do cart?o. Projeto por Contrato, em particular, a
linguagem JML, ? uma op??o para este tipo de desenvolvimento e verifica??o, pelo fato da verifica??o em tempo de execu??o ser parte da implementa??o pela JML. Contudo, JML e suas respectivas ferramentas para verifica??o em tempo de execu??o n?o foram projetadas com o foco nas limita??es Java Card, sendo, dessa forma, n?o compat?veis com Java Card. Nesta disserta??o, analisamos o quanto esta situa??o ? realmente intr?nseca ?s limita??es Java Card e, se ? poss?vel re-definir a JML e suas ferramentas. Propomos
requisitos para uma nova linguagem, a qual ? compat?vel com Java Card e apresentamos como o compilador desta linguagem pode ser constru?do. JCML retira da JML aspectos n?o definidos em Java Card, como por exemplo, concorr?ncia e tipos n?o suportados. Isto pode n?o ser o bastante, contudo, sem o esfor?o em otimiza??o de c?digo de verifica??o
gerado pelo compilador, n?o ? poss?vel gerar c?digo de verifica??o para rodar no cart?o. O compilador JCML, apesar de ser bem mais restrito em rela??o ao compilador JML,
est? habilitado a gerar c?digo de verifica??o compat?vel com Java Card, para algumas especifica??es lightweight. Como conclus?o, apresentamos uma variante da JML compat?vel
com Java Card, JCML (Java Card Modeling Language), com uma vers?o de seu compilador
|
3 |
BSmart: desenvolvimento rigoroso de aplica??es Java Card com base no m?todo formal BGomes, Bruno Emerson Gurgel 19 November 2007 (has links)
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
|
4 |
Estendendo CRefine para o suporte de t?ticas de refinamentoConserva Filho, Madiel de Souza 07 October 2011 (has links)
Made available in DSpace on 2014-12-17T15:47:59Z (GMT). No. of bitstreams: 1
MadielSCF_DISSERT.pdf: 1874479 bytes, checksum: dc22e7d8884791a523682f62c1e8c32c (MD5)
Previous issue date: 2011-10-07 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / The use of increasingly complex software applications is demanding greater investment
in the development of such systems to ensure applications with better quality. Therefore,
new techniques are being used in Software Engineering, thus making the development
process more effective. Among these new approaches, we highlight Formal
Methods, which use formal languages that are strongly based on mathematics and have a
well-defined semantics and syntax. One of these languages is Circus, which can be used
to model concurrent systems. It was developed from the union of concepts from two other
specification languages: Z, which specifies systems with complex data, and CSP, which
is normally used to model concurrent systems. Circus has an associated refinement calculus,
which can be used to develop software in a precise and stepwise fashion. Each step
is justified by the application of a refinement law (possibly with the discharge of proof
obligations). Sometimes, the same laws can be applied in the same manner in different
developments or even in different parts of a single development. A strategy to optimize
this calculus is to formalise these application as a refinement tactic, which can then be
used as a single transformation rule. CRefine was developed to support the Circus refinement
calculus. However, before the work presented here, it did not provide support for
refinement tactics. The aim of this work is to provide tool support for refinement tactics.
For that, we develop a new module in CRefine, which automates the process of defining
and applying refinement tactics that are formalised in the tactic language ArcAngelC. Finally,
we validate the extension by applying the new module in a case study, which used
the refinement tactics in a refinement strategy for verification of SPARK Ada implementations
of control systems. In this work, we apply our module in the first two phases of
this strategy / A utiliza??o de aplica??es de software cada vez mais complexas est? exigindo um
maior investimento no desenvolvimento de sistemas, garantindo uma melhor qualidade
das aplica??es. Diante desse contexto, novas t?cnicas est?o sendo utilizadas na ?rea de
Engenharia de Software, tornado o processo de desenvolvimento mais eficaz. Destacam-
se, como exemplo dessas novas abordagens, os M?todos Formais. Estes m?todos utilizam
linguagens formais que t?m sua base fundamentada na matem?tica, apresentando uma
sem?ntica e sintaxe bem definidas. Uma dessas linguagens ? Circus, que possibilita a mo-
delagem de sistemas concorrentes. Esta linguagem foi desenvolvida a partir da uni?o dos
conceitos das linguagens formais Z (que permitem a modelagem de dados complexos) e
CSP Communicating Sequential Processes (que permitem a modelagem de sistemas con-
correntes). Adicionalmente, Circus tamb?m possui um c?lculo de refinamento associado,
que pode ser utilizado para desenvolver software de forma precisa e gradual. Cada etapa
deste c?lculo ? justificada pela aplica??o de uma lei de refinamento (possivelmente com a
prova de certas condi??es chamadas de obriga??es de prova). Algumas vezes, as mesmas
leis podem ser aplicadas da mesma forma em diferentes desenvolvimentos ou mesmo em
partes diferentes de um ?nico desenvolvimento. Uma estrat?gia para otimizar esse c?l-
culo ? formalizar estas aplica??es como t?ticas de refinamento, que podem ser utilizadas
como uma simples regra de transforma??o. A ferramenta CRefine foi desenvolvida para
realizar o suporte a este c?lculo de refinamento de Circus. Entretanto, antes deste traba-
lho, essa ferramenta n?o fornecia suporte para as t?ticas. A proposta desta disserta??o ?
oferecer um suporte ferramental para a utiliza??o das t?ticas no c?lculo de refinamento de
programas Circus. Para tanto, foi desenvolvido um novo m?dulo em CRefine, que auto-
matiza o processo de defini??o e aplica??o das t?ticas de refinamento. Nesta extens?o as
t?ticas s?o formalizadas na linguagem de t?ticas para sistemas concorrentes, ArcAngelC.
Por fim, validamos a extens?o, aplicando o novo m?dulo a um estudo de caso, que utiliza
as t?ticas em uma estrat?gia de refinamento para verifica??o de implementa??es SPARK
Ada de sistemas de controle. Nesta disserta??o, aplicamos o novo modulo ?s duas fases
iniciais desta estrat?gia.
|
5 |
Gera??o autom?tica de hardware a partir de especifica??es formais: estendendo uma abordagem de tradu??oMedeiros Junior, Ivan Soares de 27 April 2012 (has links)
Made available in DSpace on 2014-12-17T15:48:02Z (GMT). No. of bitstreams: 1
IvanSMJ_DISSERT.pdf: 2894212 bytes, checksum: 3acb921ac87239ee36be60cb2e15b0e6 (MD5)
Previous issue date: 2012-04-27 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Removing inconsistencies in a project is a less expensive activity when done in the
early steps of design. The use of formal methods improves the understanding of systems.
They have various techniques such as formal specification and verification to identify
these problems in the initial stages of a project. However, the transformation from a
formal specification into a programming language is a non-trivial task and error prone,
specially when done manually. The aid of tools at this stage can bring great benefits to
the final product to be developed.
This paper proposes the extension of a tool whose focus is the automatic translation of
specifications written in CSPM into Handel-C. CSP is a formal description language suitable
for concurrent systems, and CSPM is the notation used in tools support. Handel-C is a
programming language whose result can be compiled directly into FPGA s. Our extension
increases the number of CSPM operators accepted by the tool, allowing the user to define
local processes, to rename channels in a process and to use Boolean guards on external
choices. In addition, we also propose the implementation of a communication protocol
that eliminates some restrictions on parallel composition of processes in the translation
into Handel-C, allowing communication in a same channel between multiple processes to
be mapped in a consistent manner and that improper communication in a channel does
not ocurr in the generated code, ie, communications that are not allowed in the system
specification / A remo??o de inconsist?ncias em um projeto ? menos custosa quando realizada nas
etapas iniciais da sua concep??o. A utiliza??o de M?todos Formais melhora a compreens?o
dos sistemas al?m de possuir diversas t?cnicas, como a especifica??o e verifica??o
formal, para identificar essas inconsist?ncias nas etapas iniciais de um projeto. Por?m, a
transforma??o de uma especifica??o formal para uma linguagem de programa??o ? uma
tarefa n?o trivial. Quando feita manualmente, ? uma tarefa pass?vel da inser??o de erros.
O uso de ferramentas que auxiliem esta etapa pode proporcionar grandes benef?cios ao
produto final que ser? desenvolvido.
Este trabalho prop?e a extens?o de uma ferramenta cujo foco ? a tradu??o autom?tica
de especifica??es em CSPM para Handel-C. CSP ? uma linguagem de descri??o formal
adequada para trabalhar com sistemas concorrentes, CSPM ? a nota??o utilizada pelas
ferramentas de apoio da linguagem. Handel-C ? uma linguagem de programa??o cujo
resultado pode ser compilado diretamente para FPGA s. A extens?o consiste no aumento
no n?mero de operadores CSPM aceitos pela ferramenta, permitindo ao usu?rio definir
processos locais, renomear canais e utilizar guarda booleana em escolhas externas. Al?m
disto, propomos tamb?m a implementa??o de um protocolo de comunica??o que elimina
algumas restri??es da composi??o paralela de processos na tradu??o para Handel-C, permitindo
que a comunica??o em um mesmo canal entre m?ltiplos processos possa ser mapeada
de maneira consistente e que no c?digo gerado n?o ocorra comunica??es indevidas
em um canal, ou seja, comunica??es que n?o s?o permitidas na especifica??o do sistema
|
6 |
BTS:uma ferramenta de suporte ao desenvolvimento sistem?tico de sistemas confi?veis baseados em componentesSilva, Sarah Raquel da Rocha 13 December 2013 (has links)
Made available in DSpace on 2014-12-17T15:48:09Z (GMT). No. of bitstreams: 1
SarahRRS_DISSERT.pdf: 1954614 bytes, checksum: ba3eee36fc3f3f1030a71fa2ad2f605a (MD5)
Previous issue date: 2013-12-13 / Universidade Federal do Rio Grande do Norte / The component-based development of systems revolutionized the software development
process, facilitating the maintenance, providing more confiability and reuse. Nevertheless,
even with all the advantages of the development of components, their composition is an
important concern. The verification through informal tests is not enough to achieve a
safe composition, because they are not based on formal semantic models with which we
are able to describe precisally a system s behaviour. In this context, formal methods
provide ways to accurately specify systems through mathematical notations providing,
among other benefits, more safety. The formal method CSP enables the specification
of concurrent systems and verification of properties intrinsic to them, as well as the
refinement among different models. Some approaches apply constraints using CSP,
to check the behavior of composition between components, assisting in the verification
of those components in advance. Hence, aiming to assist this process, considering
that the software market increasingly requires more automation, reducing work and
providing agility in business, this work presents a tool that automatizes the verification
of composition among components, in which all complexity of formal language is kept
hidden from users. Thus, through a simple interface, the tool BST (BRIC-Tool-Suport)
helps to create and compose components, predicting, in advance, undesirable behaviors in
the system, such as deadlocks / O desenvolvimento de sistemas baseados em componentes revolucionou o processo de
desenvolvimento de software, facilitando a manuten??o, trazendo mais confiabilidade e
reutiliza??o. Por?m, mesmo com todas as vantagens atribu?das ao componente, ? necess?rio
uma an?lise detalhada de sua composi??o. Realizar verifica??o a partir de testes
de software n?o ? o suficiente para se ter uma composi??o segura, pois esses n?o s?o
baseados em modelos sem?nticos formais nos quais podemos descrever precisamente o
comportamento do sistema. Nesse contexto, os m?todos formais oferecem a possibilidade
de especificarmos sistemas de forma precisa, atrav?s de nota??es com forte base
matem?tica, trazendo, entre outros benef?cios, mais seguran?a. O m?todo formal CSP
possibilita a especifica??o de sistemas concorrentes e verifica??o de propriedades inerentes
a tais sistemas, bem como refinamento entre diferentes modelos. Existem abordagens que
aplicam restri??es usando CSP, para verificar o comportamento da composi??o entre componentes,
auxiliando a verifica??o desses componentes antecipadamente. Visando auxiliar
esse processo, tendo em vista que o mercado de software busca cada vez mais automa??o,
minimizando trabalhos e trazendo agilidade nos neg?cios, este trabalho apresenta uma ferramenta
que automatiza a verifica??o da composi??o entre componentes, onde o conjunto
de verifica??es CSP impostas ? gerado e verificado internamente, oculto para o usu?rio.
Dessa forma, atrav?s de uma interface simples, a ferramenta BTS (BRIC-Tool-Suport)
ajuda a criar e compor componentes, prevendo, com anteced?ncia, comportamentos indesej?veis
no sistema, como deadlocks
|
7 |
M?todo B e a s?ntese verificada para c?digo de montagemMedeiros J?nior, Val?rio Gutemberg de 08 March 2016 (has links)
Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-10-11T20:48:08Z
No. of bitstreams: 1
ValerioGutembergDeMedeirosJunior_TESE.pdf: 1793475 bytes, checksum: 151ab0c6b194c17a043978ff9682034b (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-10-14T20:28:32Z (GMT) No. of bitstreams: 1
ValerioGutembergDeMedeirosJunior_TESE.pdf: 1793475 bytes, checksum: 151ab0c6b194c17a043978ff9682034b (MD5) / Made available in DSpace on 2016-10-14T20:28:33Z (GMT). No. of bitstreams: 1
ValerioGutembergDeMedeirosJunior_TESE.pdf: 1793475 bytes, checksum: 151ab0c6b194c17a043978ff9682034b (MD5)
Previous issue date: 2016-03-08 / A s?ntese de c?digo de montagem ? um processo que exige um cuidado rigoroso. Normalmente, esse processo nos tradutores e nos compiladores mais maduros ? relativamente seguro, apesar de que, esporadicamente, erros s?o identificados neles. Em um contexto mais restrito, os tradutores utilizados em comunidades menores e em constante desenvolvimento s?o mais suscet?veis a erros. Considerando esse contexto, duas abordagens de tradu??o e de verifica??o usando o m?todo B s?o apresentadas. A primeira abordagem prop?e a tradu??o do componente B para o c?digo de montagem de uma plataforma espec?fica, usando um modelo formal do conjunto de instru??es, o qual possibilita tamb?m depurar e verificar as propriedades de programas. Essa abordagem ? capaz de garantir formalmente a coer?ncia sem?ntica da tradu??o, apesar de ser um processo de verifica??o ?rduo e lento. Tal esfor?o de verifica??o foi aliviado atrav?s de uma ferramenta desenvolvida (BEval), que aproveitou melhor as t?cnicas de verifica??o. Ap?s o processo de prova autom?tica usando uma ferramenta B robusta (Atelier B), BEval ainda foi capaz de resolver em certos modelos muitas das obriga??es de prova remanescentes, chegando a at? 88% do total de obriga??es. Contudo, o processo de verifica??o da abordagem de tradu??o continuou complexo, exigindo v?rias intera??es manuais. Afim de viabilizar uma tradu??o mais eficiente e tamb?m segura, uma segunda abordagem de tradu??o de B para o c?digo de m?quina virtual foi desenvolvida. A segunda abordagem utilizou o tradutor desenvolvido B2LLVM e aplicou a gera??o autom?tica de testes para verificar a coer?ncia entre a especifica??o do programa e o seu respectivo c?digo de montagem. Esse tradutor tamb?m suporta a avalia??o de cobertura do c?digo e a inser??o de anota??es de rastreabilidade. Dessa forma, o trabalho contribuiu significativamente na tradu??o de B para o c?digo de montagem, oferecendo um suporte rigoroso para a verifica??o da tradu??o. Atualmente, o B2LLVM j? ? capaz de gerar c?digo para 84% dos exemplos de teste baseados na gram?tica que s?o traduz?veis por um relevante tradutor industrial (C4B). Ademais, o c?digo gerado por B2LLVM apresenta vantagens importantes na ampla capacidade de verifica??o, de integra??o e de otimiza??o. / Assembly code synthesis is a process that requires rigorous care. Typically, this
process in mature translators and compilers is relatively safe, though some errors
have occasionally been identified. In a more restricted context, the translators used
in the smaller communities and developed constantly have been more susceptible
to these kind of errors. Considering this context, two translation and verification
approaches using the B method have been presented. The first approach considers
the B component translation to assembly code for a specific platform by using
a formal model of the instruction set, which also allows to debug and to check
program properties. This approach can formally ensure the semantic consistency of
the translation, although the verification process is difficult and time-consuming.
This verification effort was somewhat relieved by the development of BEval, a
tool which has made better use of the verification techniques. After applying the
automatic verification process using the Atelier B tool, BEval was still able to
solve, in the certain models, many of the remaining proof obligations, reaching up
to 88 % of total obligations. However, the verification process of this translation
approach is still complex, requiring several manual interactions. In order to make
a translation more efficient and also safe, a second approach for the translating B
to virtual machine code was developed. This second approach used the developed
translator B2LLVM and applied the automatic generation of tests to check the
consistency of the program specifications and their respective assembly code.
This translator also supported the code coverage evaluation and the insertion
of the traceability annotations. Thus, this study has significantly contributed
to developing B translation to assembly code, providing rigorous support for
the verification of the translation. Currently, the B2LLVM outweighs 20,9% the
percentage of translatable test samples based on grammar compared to the C4B
industrial translator. Furthermore, the generated code by B2LLVM has important
advantages in the ample capacity of verification, integration and optimization.
|
8 |
Aplica??o do m?todo B ao projeto formal de software embarcadoMedeiros J?nior, Val?rio Gutemberg de 09 September 2009 (has links)
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
|
9 |
Local livelock analysis of component-based modelsConserva Filho, Madiel de Souza 12 August 2016 (has links)
Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-03-09T18:47:46Z
No. of bitstreams: 1
MadielDeSouzaConservaFilho_TESE.pdf: 1314650 bytes, checksum: ea38672191d7c35f5274cb1360bcfef1 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-03-10T21:13:38Z (GMT) No. of bitstreams: 1
MadielDeSouzaConservaFilho_TESE.pdf: 1314650 bytes, checksum: ea38672191d7c35f5274cb1360bcfef1 (MD5) / Made available in DSpace on 2017-03-10T21:13:38Z (GMT). No. of bitstreams: 1
MadielDeSouzaConservaFilho_TESE.pdf: 1314650 bytes, checksum: ea38672191d7c35f5274cb1360bcfef1 (MD5)
Previous issue date: 2016-08-12 / O uso crescente de sistemas complexos exige cada vez mais um maior investimento
de recursos no desenvolvimento de software para garantir a confiabilidade dos mesmos.
Para lidar com esta complexidade, abordagens composicionais podem ser utilizadas no
desenvolvimento de sistemas de software, possibilitando a integra??o e a reutiliza??o
de componentes existentes. Entretanto, a fim de garantir o sucesso desta abordagem, ?
essencial confiar no comportamento dos componentes e, al?m disso, nos sistemas que s?o
desenvolvidos utilizando essa estrat?gia, uma vez que falhas podem ser introduzidas se a
composi??o n?o assegurar propriedades importantes. Problemas podem surgir quando dois
ou mais componentes s?o integrados pela primeira vez. Esta situa??o ? ainda mais relevante
quando um grupo de componentes trabalha em conjunto a fim de executar determinadas
tarefas, especialmente em aplica??es cr?ticas, onde podem surgir problemas cl?ssicos, como
livelock. Esta tese de doutorado apresenta uma estrat?gia local para garantir aus?ncia de
livelock, por constru??o, em sistemas s?ncronos modelados com a nota??o padr?o de CSP.
A nossa t?cnica ? baseada na an?lise local das m?nimas sequ?ncias que levam o processo
CSP ao seu estado inicial. O uso de t?cnicas locais evita a explos?o do espa?o de estados
gerado pela integra??o dos componentes. A verifica??o destas condi??es locais utilizam
metadados que permitem armazenar resultados parciais das verifica??es, reduzindo o
esfor?o durante a an?lise. A abordagem proposta tamb?m pode ser aplicada para verificar
aus?ncia de livelock em modelos que realizam comunica??es ass?ncronas. Neste caso,
analisamos o modelo de componentes BR IC, cujo comportamento dos componentes
? representado por um processo CSP. A fim de realizar esta verifica??o, consideramos
duas vers?es para BR IC: BR IC , o qual realiza composi??es ass?ncronas atrav?s de
buffers finitos, e BR IC? no qual a assincronicidade ? realizada atrav?s de buffers infinitos.
Estas duas abordagens foram analisadas porque a possibilidade de introduzir livelock em
sistemas ass?ncronos depende diretamente da finitude do buffer. As t?cnicas propostas para
garantir aus?ncia de livelock em CSP e BR IC foram avaliadas atrav?s de tr?s estudos
de caso: o escalonador de Milner e duas varia??es do jantar dos fil?sofos. Uma vers?o
apresenta um sistema livre de livelock, e a outra apresenta um sistema com livelock. Neste
estudo, avaliamos a nossa abordagem em compara??o com outras duas t?cnicas para
verifica??o de aus?ncia de livelock, a an?lise global tradicional do FDR e a an?lise est?tica
de livelock do SLAP. Este estudo comparativo demonstra que a nossa estrat?gia pode
ser aplicada como uma alternativa para a verifica??o de aus?ncia de livelock em grandes
sistemas. / The use of increasingly complex applications is demanding a greater investment of
resources in software development to ensure that applications are safe. For mastering
this complexity, compositional approaches can be used in the development of software
by integrating and reusing existing reliable components. The correct application of such
strategies, however, relies on the trust in the behaviour of the components and in the emergent
behaviour of the composed components because failures may arise if the composition
does not preserve essential properties. Problems may be introduced when two or more
error-free components are integrated for the first time. This concern is even more relevant
when a group of components is put together in order to perform certain tasks, especially in
safety-critical applications, during which classical problems can arise, such as livelock. In this thesis, we present a local strategy that guarantees, by construction, the absence
of livelock in synchronous systems as modelled using the standard CSP notation. Our
method is based solely on the local analysis of the minimum sequences that lead the CSP
model back to its initial state. Locality provides an alternative to circumvent the state
explosion generated by the interaction of components and allows us to identify livelock
before composition. The verification of these conditions use metadata that allow us to
record partial results of verification, decreasing the overall analysis effort. In addition, our
work can also be applied to check livelock freedom in models that perform asynchronous
communications. In this case, we carry out livelock analysis in the context of a component
model, BR IC, whose behaviour of the components is described as a CSP process. Finally,
we introduce three case studies to evaluate our livelock analysis technique in practice: the
Milner?s scheduler and two variations of the dining philosophers, a livelock-free version
and a version in which we have deliberately included livelock. For each case study, we
also present a comparative analysis of the performance of our strategy with two other
techniques for livelock freedom verification, the traditional global analysis of FDR and the
static livelock analysis of SLAP. This comparative study demonstrates that our strategy
can be used in practice and that it might be a useful alternative for establishing livelock
freedom in large systems.
|
10 |
Joker: um realizador de desenhos animados para linguagens formaisSouza, Diego Henrique Oliveira de 31 August 2011 (has links)
Made available in DSpace on 2014-12-17T15:47:56Z (GMT). No. of bitstreams: 1
DiegoHOS_DISSERT.pdf: 2899752 bytes, checksum: d3160b774efd6749eced9bb34d4a74cf (MD5)
Previous issue date: 2011-08-31 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Using formal methods, the developer can increase software s trustiness and correctness.
Furthermore, the developer can concentrate in the functional requirements of the
software. However, there are many resistance in adopting this software development
approach. The main reason is the scarcity of adequate, easy to use, and useful tools.
Developers typically write code and test it. These tests usually consist of executing the
program and checking its output against its requirements. This, however, is not always
an exhaustive discipline. On the other side, using formal methods one might be able
to investigate the system s properties further. Unfortunately, specification languages do
not always have tools like animators or simulators, and sometimes there are no friendly
Graphical User Interfaces. On the other hand, specification languages usually have a compiler
which normally generates a Labeled Transition System (LTS). This work proposes
an application that provides graphical animation for formal specifications using the LTS
as input. The application initially supports the languages B, CSP, and Z. However, using a
LTS in a specified XML format, it is possible to animate further languages. Additionally,
the tool provides traces visualization, the choices the user did, in a graphical tree. The
intention is to improve the comprehension of a specification by providing information
about errors and animating it, as the developers do for programming languages, such as
Java and C++. / Usando m?todos formais, o desenvolvedor pode aumentar a confiabilidade e corretude
do software. Al?m disso, o desenvolvedor pode concentrar-se mais nos requisitos
funcionais. Por?m h? muita resist?ncia em se adotar essa abordagem de desenvolvimento
de software. A raz?o principal e a escassez de suporte ferramental adequado, ?til e de f?cil
utiliza??o. Os desenvolvedores normalmente escrevem o c?digo e o testam. Estes testes
geralmente consistem em checar se as sa?das est?o de acordo com os requisitos. Isto, contudo,
nem sempre e poss?vel de maneira exaustiva. Por outro lado, usando M?todos Formais
um desenvolvedor e capaz de investigar profundamente as propriedades do sistema.
Infelizmente, linguagens de especifica??o formal nem sempre possuem ferramentas como
animador ou simulador e ?s vezes n?o h? interfaces gr?ficas amig?veis. Por?m, algumas
dessas ferramentas possuem um compilador, que gera um Sistema de Transi??es Rotuladas
(LTS). A proposta deste trabalho ? desenvolver um aplicativo que fornece anima??o gr?fica para especifica??es formais usando o LTS como entrada. O aplicativo inicialmente
suporta as as linguagens B, CSP e Z. Usando o LTS em um formato XML especificado
? poss?vel animar outras linguagens formais. Adicionalmente a ferramenta disponibiliza
visualiza??o de traces, escolhas feitas pelo usu?rio, em um formato de ?rvore gr?fica. A
inten??o ? melhorar a compreens?o de uma especifica??o, fornecendo informa??es sobre
erros e animando-a, como os desenvolvedores fazem com linguagens de programa??o
como Java e C++.
|
Page generated in 0.06 seconds