Resumo

Erros são comuns durante o desenvolvimento de sistemas de software e
hardware,
sendo que sua detecção e correção na maioria das vezes envolve um processo
de
alto custo. Este custo, no entanto, pode ser reduzido se o projetista for
capaz
de corrigir erros ainda na fase de especificação do sistema. Atualização
de
Modelos é uma abordagem formal utilizada para corrigir automaticamente um
modelo
de um sistema que não satisfaz uma dada propriedade. A maioria das abordagens
de
atualização de modelos é baseada na lógica temporal de tempo ramificado
CTL, a
qual não leva em consideração as ações que rotulam as transições de
estados.
Nesta proposta apresentamos um arcabouço de atualização de modelos baseada
em
ações, que pode ser utilizado para sugerir automaticamente modificações em
um
sistema considerando as ações que rotulam as transições de estados, bem
como
sugerir modificações na própria especificação de ações. Neste contexto,
a
especificação de um sistema é representada por um sistema de transições
rotuladas e as propriedades a serem verificadas são especificadas na lógica
temporal alpha-CTL : uma extensão da CTL que possui a semântica baseada em ações.