Seminário do LIAMF dia 20/5

---------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------

Título: Atualização de Modelos Baseada em Ações
Palestrante: Maria Viviane de Menezes

Data:  20/5/2010, 14hs
Local: Sala 254-A

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.


Todos são bem-vindos.