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. Para otimizar esse cálculo, esta dissertação apresenta as táticas de refinamento. Que são estratégias que agrupa as leis de refinamento que se repetem ao longo deste processo de refinamento. Este trabalho apresenta o desenvolvimento de um módulo dentro do CRefine para automatizar também esse processo de aplicação das táticas de refinamento. A linguagem de táticas de refinamento utilizada é a ArcAngelC. Outro objetivo desta dissertação é a implementação de um Parser de táticas. Com isso, essa nova extensão irá possibilitar que táticas de refinamento sejam criadas e utilizadas na ferramenta.