VERIFAI: Traceability and Verification of natural-language requirements
(2024-2026)
(2024-2026)
VERIFAI is led by Professor Rosemary Monahan and Dr.Diarmuid O'Donoghue in the Dept. of Computer Science and Hamilton Institute at Maynooth University . The project is funded via the ADAPT Research Centre, funding a postdoctoral researcher from August 2024 until January 2026, who will collaborate with members of the Principles of Programming Research Group.
Our overall goal is to provide scalable techniques for software development that guarantee software dependability, even when deep learning techniques are employed by developers. The output of this work will be a methodology which allows us to verify properties of hybrid systems with mixed discrete and continuous dynamics, and associated software tooling to integrate this with existing verification frameworks. A case study will demonstrate the effectiveness of our approach.
To verify the correctness and reliability of safety critical software, we express safety properties of the system as a collection of formal specifications that are unambiguous and that can be reasoned about mathematically. Verification of these formal specifications is achieved through methods such as deductive verification, model checking and runtime verification. A major burden in this process is the generation of the formal specifications. The requirements elicitation process starts with natural language requirements which are often ambiguous, leading to incorrect properties of a system being specified, and systems that are under-specified due to the assumptions of the domain knowledge. Furthermore, traceability from the original system requirements through to the properties of the implemented system is often missing. With the use of machine learning in systems development, requirements traceability becomes even more crucial: as a software system learns, we must ensure that safety properties identified at the design stage are maintained in the final system; as the system evolves we must track the changes to the original software requirements, to give a better understanding of the behaviour of the AI; and we must monitor the impact of the training data used, to direct learning so that safety properties are maintained by the system.
This project will address these challenges through providing support for the automatic generation of the formal specifications, and the traceability of the requirements from the initial software design stage through the systems implementation and verification. In this way we can ensure that when a system is implemented, we not only build the correct system, but we also build the system correctly. In addition, if an error occurs in the expected behaviour of the system, we can trace to where and when the source of the violation occurs. Approaches which will be explored as part of this project include Natural Language Processing, use of ontologies to describe the software systems domain, reuse of existing software artefacts from similar systems (e.g. through similarity –based), and large language models to identify and declare the specification as well as use of artificial intelligence to guide the process.
Funding: This project is funded via ADAPT research centre platform funding (Phase 2). ADAPT, the world-leading SFI Research Centre for AI-Driven Digital Content Technology, brings leading academics, researchers, and industry partners together to deliver excellent science, engage the public, develop novel solutions for business across all sectors and enhance Ireland’s international reputation. Coordinated by Trinity College Dublin and co-hosted by Dublin City University, ADAPT’s partner institutions include University College Dublin, Technological University Dublin, Maynooth University, Munster Technological University, Technological University of the Shannon: Midlands Midwest, and the National University of Ireland Galway.