Verificação formal na indústria
Carregando...
Data
Autor(es)
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal de Minas Gerais
Descrição
Tipo
Monografia de especialização
Título alternativo
Primeiro orientador
Membros da banca
Mariza Andrade da Silva Bigonha
Resumo
Os métodos formais consistem em uma família de técnicas de elaboração de sistemas em que é aplicado o formalismo matemático na assistência às fases de especificação, desenvolvimento e verificação. A abordagem é capaz de reduzir ambiguidades e inconsistências da especificação, proporcionar geração automática de código e automatizar tarefas de verificação, se apresentando como uma alternativa para se alcançar sistemas com maior correção, especialmente em situações em que falhas podem causar grandes perdas financeiras e humanas. Este estudo consiste na avaliação dos métodos formais na indústria com a apresentação de um caso real de software de verificação formal utilizado na indústria de circuitos integrados. Para isso, são expostos os conceitos relativos ao tema, os principais métodos de especificação e verificação formal, os obstáculos enfrentados pela metodologia para se estabelecer no mercado e propostas para que esses desafios sejam vencidos. Por fim, é apresentado o software de verificação formal JasperGold Apps da Cadence Design Systems, sua estrutura e técnicas aplicadas, bem como a importância e os benefícios da abordagem formal na indústria de hardware.
Abstract
Formal Methods is a group of system design techniques that use mathematics formalism to assist specification, development and verification steps. The approach can reduce specifications ambiguities and inconsistences, provide automatic automated code generation and automate verifying tasks, showing up as an alternative to achieve systems with higher correctness levels, especially in cases that failures can lead to major material and human losses. This study consists of an evaluation of formal methods in industry with a real case presentation of a formal verification software used in integrated circuits industry. Seeing that, are shown the concepts related to the field, the main specification and verification formal methods, the challenges faced by the methodology for establishing in the market and suggestions to overcome them. Finally, it is shown the Cadence Design Systemss formal verification software JasperGold Apps, its structure and implemented techniques, as well as the formal approach significance and benefits in hardware industry.
Assunto
Demonstração automatica de teoremas, Computação, Engenharia de software, Programas de computador Verificação
Palavras-chave
Model check, Theorem proving, Métodos formais, Especificação formal, Verificação formal