Please use this identifier to cite or link to this item:
http://hdl.handle.net/1843/RVMR-794P7N| Type: | Dissertação de Mestrado |
| Title: | Método de refinamento machina |
| Authors: | Italo Giovani Abdanur Stefani |
| First Advisor: | Roberto da Silva Bigonha |
| First Referee: | Elaine Gouvea Pimentel |
| Second Referee: | Mariza Andrade da Silva Bigonha |
| Third Referee: | Vladimir Oliveira Di Iorio |
| Abstract: | 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. |
| Subject: | Processamento eletronico de dados Computação Teoria dos autômatos Programas de computador Verificação |
| language: | Português |
| Publisher: | Universidade Federal de Minas Gerais |
| Publisher Initials: | UFMG |
| Rights: | Acesso Aberto |
| URI: | http://hdl.handle.net/1843/RVMR-794P7N |
| Issue Date: | 13-Mar-2007 |
| Appears in Collections: | Dissertações de Mestrado |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| italogiovaniabdanurstefani.pdf | 3.12 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.