Specification Mining with Active Automata Learning

Constant fast-paced technological advancements are a major catalyst for software complexity, which becomes concerning as software systems spread to all areas of society and become safety- critical. Formal methods provide tools to mitigate this issue by targeting bugs and faults, however they require formal specifications for determining the intended behaviour of the system. This is problematic as specification-making is a time-consuming, laborious, and error-prone process, and is often avoided unless strictly necessary. This thesis addresses this problem by introducing a new approach to specification creation based on formal inference of system behaviour alongside user-based manual adjustments. Active automata learning is used to learn the behaviour of the target system in the form of deterministic finite automata (DFA) and register automata (RA). Then through an extension of the automata learning framework C3AL, the generated specification can be manually refined through user-provided counterexamples. A proof-of-concept specification mining tool is also implemented which showcases the ability to generate a specification of the Java Iterator interface tailored to the user’s preference. This work lays the foundations for a more reliable and efficient specification creation process that aims to make formal methods more accessible to real-world systems.