Uso de Sistemas de Transições Modais de Kripke para Representacão de Comportamento Parcial no Desenvolvimento incremental e interativo de software

Abstract

O projeto de software na abordagem iterativa e incremental lida com novos requisitos ao longo do desenvolvimento, que implicam em constantes mudanças no projeto, e mecanismos que dêem suporte para o desenvolvimento na presença de informação parcial e incompleta são importantes para reduzir o impacto dessas mudanças. Expressar incertezas a respeito do comportamento pretendido do software ou componente pode evitar a tomada de decisões precipitadas, que poderiam acarretar em erros de projeto. Neste contexto, diversos trabalhos utilizam sistemas de transições modais para especificar um software e/ou seus componentes com informação parcial e utilizam relações e operações sobre estes modelos para dar suporte ao processo de desenvolvimento. Os sistemas de transições modais permitem expressar incerteza deforma explícita através de modalidades em suas transições. Sobre estes modelos, uma relação de refinamento pode ser definida para garantir que modelos criados, nas iterações e incrementos, respeitem as propriedades anteriormente definidas em outros modelos, garantindo a correção dos mesmos ao longo do processo de desenvolvimento. Além disto, operações para unificar diversos modelos de um mesmo componente em um único modelo e operações para representar execução em paralelo de diversos componentes em um nível de sistema, são propostas. Sistema de Transição Modal de Kripke (KMTS) é um tipo de sistema de transições modais que além de expressar modalidades em transições, também permite expressar indefinições em nível de proposições nos estados. A indeterminação nos estados é interessante, pois permite que vários estados sejam representados em um mesmo estado, evitando uma definição prévia de todos os estados do sistema nas fases iniciais do desenvolvimento. Todavia, existem poucos trabalhos que utilizam KMTS como modelos para especificação parcial aplicados no desenvolvimento de software. O presente trabalho estuda o uso de modelos KMTS para explicitar informações parciais durante o desenvolvimento de software, trazendo contribuições na criação, na análise e no reparo destes modelos. Em relação à criação de modelos propomos um algoritmo de síntese de modelos KMST a partir de diagramas de sequências anotados com Object Constraint Language (OCL) que é uma adaptação de um algoritmo proposto na literatura para modelos de transições modais (MTS). Em relação à análise de modelos, definimos as operações de conjunção e de composição paralela bem como a relação de refinamento modal forte para modelos KMTS. O conceito de refinamento para KMTS é também caracterizado nessa dissertação como um jogo e um algoritmo para o jogo do refinamento é proposto, discutido e validado. A contribuição no reparo de modelos se dá através do estudo do problema de reparo do refinamento para KMTS, isto é, como alterar um modelo KMTS para que ele seja um refinamento de outro modelo KMTS. Para este problema, algoritmos são também propostos, discutidos e validados. Entendemos que esta solução poderá trazer contribuições para o reparo automático de modelos e pode ser aplicada em outras áreas, como por exemplo, análise de impacto de mudanças para determinar qual a mudança menos custosa a se fazer em um determinado modelo para que ele possua determinadas propriedades. A partir das contribuições na construção, análise e reparo de modelos KMTS, o presente trabalho define a base para um framework formal que pode ser utilizado na construção e evolução de software.