Método de refinamento machina

by Abdanur Stefani, Italo Giovani

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.