A COMPARATIVE ANALYSIS OF FORMAL METHODS TOOLS: EDUCATIONAL SUITABILITY, VERIFICATION CAPABILITIES, AND INDUSTRIAL RELEVANCE
Keywords:
Formal methods, Software verification, Undergraduate education, TLA+, Alloy, Dafny, Theorem proving, Model checking, Artificial Intelligence, Software engineering education.Abstract
The use of formal methods is an important way of enhancing software reliability, because it allows software systems to be specified mathematically, verified and validated. It is difficult to choose the right software tools for undergraduate formal methods education, however, as there are a variety of tools with varying capabilities in terms of verification, usability, level of automation support, learning curve, and relevance for industry. This paper compares a variety of software used in undergraduate formal methods courses such as TLA+, Isabelle/HOL, Coq, Z3, Event-B, Alloy, Frama-C, and Dafny. The study is carried out based on the systematic literature review and focuses on each tool from the point of view of its educational suitability, its verification techniques, its level of automation and its applicability in software engineering practice. Analysis indicates that Dafny along with Alloy best meets the needs of ease of use, automated feedback, and programming-oriented verification in introductory undergraduate courses. In order to analyze the various model and refinement-based verification tools, TLA+ and Event-B were found to be efficient pedagogical tools for system modeling, refinement-based verification; Frama-C and Z3 are very useful tools in software analysis and verification. This still proves useful for a mathematically rigorous verification and advanced theorem proving, and Coq and Isabelle/HOL remain useful. Additionally, the study reveals the new trends of using Artificial Intelligence and Large Language Models in formal methods teaching such as specification generation, assisting proofs, supporting proofs, etc. The results indicate that undergraduate formal methods courses should use a balanced assortment of tools for the beginners and more advanced verification environments as appropriate for the course goals. Moreover, using AI-powered verification tools could help make access to mathematics more accessible and engaging for learners, while also complementing rather than supplanting formal mathematics reasoning. This research helps to understand the selection of tools in formal methods education and gives some recommendations to teachers who are planning a course on verification for undergraduate students.
