Estendendo CRefine para o Suporte de Táticas de Refinamento
Métodos Formais, Circus, Táticas de Refinamento, ferramenta
Devido à necessidade da utilização de aplicações de software cada vez mais complexas, existe uma grande preocupação no que diz respeito em garantir uma melhor qualidade no processo de desenvolvimento de software. Assim, tanto profissionais quanto pesquisadores estão utilizando novas técnicas em conjunto com as já existentes na área de Engenharia de Software para tornar o desenvolvimento dos sistemas cada vez mais correto. Uma dessas abordagens são os Métodos formais, que utilizam linguagens formais que têm sua base fundamentada na matemática, apresentando uma semântica e sintaxe bem definidas. Uma destas linguagens é Circus, a qual possibilita a modelagem de sistemas concorrentes. Ela foi desenvolvida com a união dos conceitos de outras duas linguagens de especificação, Z, que especifica a modelagem de dados complexos, com CSP, para a modelagem de sistemas concorrentes. Circus também possibilita realizar o processo de cálculo de refinamentos de programas, na qual leis de refinamento são aplicadas à uma especificação formal. A ferramenta CRefine foi desenvolvida para realizar o suporte a este cálculo de refinamentos de programas em Circus.
Cada etapa é justificada pela aplicação de uma lei de refinamento (possivelmente com o prova de certas condições chamadas de obrigações de prova). Às vezes, as mesmas leis podem ser aplicadas da mesma forma em diferentes desdobramentos ou mesmo em partes diferentes de um único desenvolvimento. Uma estratégia para otimizar esse cálculo é formalizar estas aplicações como táticas de refinamento, que podem ser usadas como uma regra única de transformação.
Antes desta dissertação, CRefine não fornecia suporte para as táticas de refinamento. Este trabalho apresenta um novo módulo no CRefine, que automatiza o processo de definição e aplicação de táticas de refinamento que são formalizadas na linguagem tática ArcAngelC. Além disso, validamos a extensão aplicando o novo módulo em um estudo de caso, que consiste em uma estratégia de refinamento para verificação de implementações SPARK Ada de sistemas de controle.