AMBA - Atualização de Modelos Baseada em Ações

• Processo: 09/07039-4
• Modalidade de apoio: Bolsas no Brasil - Mestrado
• Data de Início da vigência: 01 de agosto de 2009
• Data de Término da vigência: 31 de agosto de 2010
• Área de conhecimento: Ciências Exatas e da Terra - Ciência da Computação - Teoria da Computação
• Pesquisador responsável: Leliane Nunes de Barros
• Beneficiário: Maria Viviane de Menezes
• Instituição Sede: Instituto de Matemática e Estatística (IME). Universidade de São Paulo (USP). São Paulo , SP, Brasil
• Palavra(s)-Chave do Pesquisador: Atualização de Modelos | Ctl | Verificação de Modelos | Métodos Formais

Resumo

Durante o projeto de desenvolvimento de sistemas de hardware ou software é muito comum ocorrerem inconsistências entre a especificação formal do sistema e algumas propriedades desejadas. Há ferramentas computacionais que verificam se uma dada propriedade é válida ou não em um modelo formal (Model Checkers), mas não informam como o sistema deve adaptar-se para satisfazer esta propriedade. Assim, foi introduzido o conceito de Atualização de Modelos (Model Update) que além de verificar se um modelo formal não satisfaz uma dada propriedade, é capaz de sugerir pequenas correções no modelo (mudanças minimais) para que a propriedade passe a ser satisfeita. A maioria das propostas de Model Update encontradas na literatura é baseada na lógica temporal CTL, que não leva em consideração as ações que rotulam as transições entre estados. Este projeto se propõe a desenvolver um sistema de Atualização de Modelos baseado em uma extensão da lógica CTL: a lógica ±-CTL, cuja semântica é definida sobre ações. Desta forma, espera-se realizar novas modificações minimais no modelo tais como Eliminação ou Adição de uma Ação, o que não é possível nos atualizadores de modelos CTL.