Método de refinamento machina

• Ano de defesa: 2007
• Autor(a) principal: Italo Giovani Abdanur Stefani
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal de Minas Gerais; UFMG
• Palavras-chave em Português: machina; linguagens de programação; Processamento eletronico de dados; Computação; Teoria dos autômatos; Programas de computador Verificação
• Link de acesso: http://hdl.handle.net/1843/RVMR-794P7N

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.