Especificação formal de restrições de projeto para frameworks orientados a objetos

Abstract

Um dos desafios encontrados para a concepção de sistemas a partir de frameworks orientados a objetos é a sua adequada utilização. Utilizar um framework adequadamente para constituir um sistema implica em obedecer às suas restrições, definidas em seu projeto. Dentre as restrições que o desenvolvedor da aplicação sob um framework precisa observar, está a correta ordem de execução de métodos dos objetos disponibilizados pelo framework. Nesse contexto, esse trabalho propõe uma maneira de especificar formalmente as restrições que um framework impõe em termos da ordem em que seus métodos podem ser invocados. A partir da especificação formal, gera-se automaticamente código, baseado no paradigma de desenvolvimento orientado a aspectos, capaz de verificar se as restrições formalmente especificadas estão sendo observadas em tempo de execução. De forma transparente ao usuário do framework e ao desenvolvedor da aplicação final, o código automaticamente gerado instancia uma rede de Petri, a qual será responsável pelo controle do estado de cada objeto especificado e o controle do estado do sistema. Ambos os desenvolvedores são beneficiados: o desenvolvedor do framework não precisa escrever código que testa as restrições do framework e o desenvolvedor da aplicação final será notificado se ele estiver fazendo invocações indevidas a um método. A abordagem formal proposta neste trabalho é aplicada ao TAF, um framework desenvolvido pela Motorola para a criação de casos de teste automatizados para telefones celulares.