Método de refinamento machina

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.