Método de refinamento machina
Carregando...
Data
Autor(es)
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal de Minas Gerais
Descrição
Tipo
Dissertação de mestrado
Título alternativo
Primeiro orientador
Membros da banca
Elaine Gouvea Pimentel
Mariza Andrade da Silva Bigonha
Vladimir Oliveira Di Iorio
Mariza Andrade da Silva Bigonha
Vladimir Oliveira Di Iorio
Resumo
O modelo de Máquina de Estado Abstrata (ASM - Abstract State Machine) vem sendo amplamente utilizado para especificação formal de diversos tipos de sistemas devido ao seu alto grau de abstração e rigor matemático, o que facilita compreender o sistema modelado e verificar formalmente suas propriedades. Pode-se utilizar uma linguagem baseada no modelo ASM para escrever uma especificação em alto nível, conhecida como Modelo Básico, e posteriormente submetê-la a um processo de transformação baseado no Método de Refinamento ASM para obter a implementação validada e verificada.O principal objetivo do trabalho Método de Refinamento Machina (MRM) é propor um método de especificação em alto nível que represente aspectos de ASM e com a possibilidade de validar e verificar o modelo construído independente da implementação. O processo de refinamento permite obter, automaticamente, o código executável em Machina e realizar a verificação utilizando a ferramenta NuSMV. Assim, pode-se verificar automaticamente a implementação de acordo com a especificação.
Abstract
The Abstract State Machine (ASM) has been used as language for formal specification to various systems due to the high level of abstraction and the mathematical rigor. It facilitates to understand the modeled system and to formally verify properties. Using an ASM language, is possible to make a high level specification, called Ground Model, to be transformed, based on The ASM Refinement Method, in an executable code, validated and verified.The main goal of The Machina Refinement Method is to propose a high level specification method that represents aspects of ASM with the possibility to validate and to verify the builded model independent of the implementation. The refinement process automatically generates the executable Machina code and to carry through the verification using the NuSMV tool. Thus, the implementation can be automatically verified in accordance with the specification.
Assunto
Processamento eletronico de dados, Computação, Teoria dos autômatos, Programas de computador Verificação
Palavras-chave
machina, linguagens de programação