Automatic repair of behavioural specifications

Abstract

Somewhat worryingly, software is becoming increasingly complex with the passing of time. Even though society has become completely dependent on it, there’s still not enough quality teaching and tooling to help software engineers verify the correctness of their solutions. Furthermore, quickly put together solutions are often incentivized over a more rigorous approach. Software is always bound to have bugs. However, formal specification languages allow the modeling of complex systems by specifying the relevant entities, how they interact, and testing the expected guarantees. Hence, helping developers gain valuable understanding of the systems they work with. This approach has the drawbacks of not only being time costly, adding another step in the development process that requires deep understanding of the problem, but also being difficult to learn. The cause is due to the more abstract nature of specification compared to programming, paired with the need to be comfortable working with formal logic concepts. Alloy is a formal specification language capable of structural and behavioral analysis. It is a popular framework for validating and verifying requirements, in part due to its expressiveness and flexibility. This makes it a prime candidate to develop and experiment new automatic repair techniques. They can help experienced developers speed up the process of writing specifications and new developers to learn quicker. With this in mind, some work has been done on repairing flawed structural Alloy models, but none considering behavioral aspects. Thus, this thesis presents an overview of the Alloy language, along with previously proposed automatic repair techniques; it proposes the first mutation-based technique for the automatic repair of first-order temporal logic specifications using Alloy6; also, it describes the integration of an automatic hint generation system for Alloy4Fun, an online platform for teaching Alloy.

De forma preocupante, o software está a tornar-se cada vez mais complexo com a passagem do tempo. A sociedade está completamente dependente dele. No entanto, mesmo nos dias que decorrem, não há ensino nem ferramentas suficientes que permitam aos engenheiros de software verificar a correção das suas soluções. Para além disto, soluções construídas rapidamente e com negligência relativamente à qualidade são incentivadas em contraste a uma abordagem mais rigorosa. Todo o tipo de software terá inevitavelmente defeitos. No entanto, as linguagens de especificação formal permitem modelar sistemas complexos através da especificação das entidades relevantes, como as mesmas interagem, e testes das garantias esperadas. Consequentemente isto auxilia profissionais a compreender mais aprofundadamente os sistemas em que trabalham. Esta abordagem tem algumas desvantagens, como ser custosa temporalmente, sendo que adiciona mais um passo no processo de desenvolvimento, para além de ser difícil de aprender. A causa disto vem da natureza abstrata de especificações quando comparadas a programação, em conjunto da necessidade de estar confortável a trabalhar com conceitos de lógica formal. Alloy é uma linguagem de especificação formal, capaz de análise estrutural e também temporal. É uma framework popular para validar e verificar requisitos, em grande parte por ser bastante expressiva e flexível. Isto torna-a uma excelente candidata para desenvolver e testar novas técnicas de reparação automática. Estas podem ser capazes ajudar estudantes a aprender mais rapidamente, tal como acelerar o desenvolvimento para utilizadores experientes. Com esta finalidade, algum trabalho já foi feito em relação à reparação de modelos estruturais em Alloy; no entanto, nada se encontra feito quando se põe em consideração os aspetos temporais. Sendo assim, este trabalho apresenta um resumo da linguagem Alloy, em conjunto com as técnicas de reparação automática já propostas; propõe a primeira técnica baseada em mutações para reparação automática de especificações de lógica de primeira ordem em Alloy 6; para alem disso, descreve a integração de um sistema de geração automática de dicas para a plataforma Alloy4Fun.