Sharper Specs for Smarter Drones: Formalising Requirements with FRET

Sheridan, Oisín; Becker, Leandro Buss; Farrell, Marie; Luckcuck, Matt; Monahan, Rosemary

Abstract

[Context and motivation] Software requirements are commonly expressed in natural-language, which must be formalised if they are to be used by formal methods such as Runtime Verification (RV), where we verify that an implementation obeys its requirements during execution. [Question/problem] This paper reports on our experience of using the Formal Requirements Elicitation Tool (FRET) to formalise requirements for an autonomous tilt-rotor drone in the ProVANT Emergentia research project. Structured, formalised requirements help to refine the meaning of, and discover ambiguities in, a requirements set, which is beneficial for safety-critical systems. FRET generates a temporal logic semantics for each requirement, providing formulas that can be used for RV. [Principal ideas/results] We describe the process of formalising the natural-language requirements using FRET. We present the progress made in each of the four versions of the requirements set as new information was elicited and incorporated. Our two concrete outputs are the formalised requirement set, which we will use in our ongoing development and verification of ProVANT; and metrics about the requirements. [Contribution] From our experience, we present guidance for requirements elicitation and formalisation with FRET. We highlight situations where it was difficult to formalise these requirements and describe potential improvements to FRET to address these difficulties.

Citation

Sheridan, O., Becker, L. B., Farrell, M., Luckcuck, M., & Monahan, R. (2025, April). Sharper Specs for Smarter Drones: Formalising Requirements with FRET. Presented at 31st International Working Conference, REFSQ 2025, Barcelona, Catalunya, Spain

• Presentation Conference Type: Edited Proceedings
• Conference Name: 31st International Working Conference, REFSQ 2025
• Start Date: Apr 7, 2025
• End Date: Apr 10, 2025
• Acceptance Date: Jan 15, 2025
• Online Publication Date: Apr 1, 2025
• Publication Date: Apr 1, 2025
• Deposit Date: May 22, 2025
• Print ISSN: 0302-9743
• Electronic ISSN: 1611-3349
• Peer Reviewed: Peer Reviewed
• Pages: 350-362
• Series Title: Lecture Notes in Computer Science
• Series Number: 15588
• Series ISSN: 1611-3349
• Book Title: Requirements Engineering: Foundation for Software Quality 31st International Working Conference, REFSQ 2025, Barcelona, Spain, April 7–10, 2025: Proceedings
• ISBN: 9783031885303
• DOI: https://doi.org/10.1007/978-3-031-88531-0_25
• Public URL: https://nottingham-repository.worktribe.com/output/48556757
• Publisher URL: https://link.springer.com/chapter/10.1007/978-3-031-88531-0_25