Details

Método de refinamento machina

by Abdanur Stefani, Italo Giovani

Abstract (Summary)
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.
This document abstract is also available in English.
Bibliographical Information:

Advisor:Roberto da Silva Bigonha; Elaine Gouvea Pimentel; Mariza Andrade da Silva Bigonha; Vladimir Oliveira Di Iorio

School:Universidade Federal de Minas Gerais

School Location:Brazil

Source Type:Master's Thesis

Keywords:Programas de computador Verificação Teses. Processamento eletronico dados Teoria dos autômatos

ISBN:

Date of Publication:03/13/2007

© 2009 OpenThesis.org. All Rights Reserved.