Atualização de modelos baseada em ações

Resumo

Erros são comuns durante o desenvolvimento de sistemas, sendo que sua detecção e correção 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 CTL , a qual não leva em consideração as ações que rotulam as transições de estados. Em trabalhos anteriores propomos uma nova abordagem para atualização de modelos, que pode ser utilizada para sugerir automaticamente modificações em um sistema considerando as ações. Para isso, o modelo é representado 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 de CTL que possui a semântica baseada em ações. Nessa proposta de doutorado direto queremos estender essa abordagem de atualização de modelos baseada em ações para também sugerir modificações na própria especificação de ações. Essa ideia amplia o conceito anterior de atualização de modelos para que possa ser aplicado também na área de modelagem de domínios de planejamento, isto é, modelagem de ações de agentes de planejamento que interagem com um ambiente. Nesse contexto, as ações induzem os modelos no qual se deseja verificar propriedades e efetuar atualizações. (AU)