Mu-FRET: A Catalogue and Tool for Requirement Refactoring

In this paper, we present a catalogue of refactorings for formalised requirements, which improve the structure of requirements without changing their behaviour. As a requirements set evolves and grows in complexity, refactoring is needed to improve clarity, eliminate repetition, and restructure requirements without introducing errors. We integrate our approach with the formal requirement language FRETISH, and we implement the approach in our Mu-FRET tool. Our approach provides a rigorous grounding for refactoring formalised requirements with guarantees of semantic preservation between requirements before and after refactoring. To this end, Mu-FRET uses the Metric Temporal Logic (MTL) semantics that underpins FRETISH requirements to formally verify that refactoring has preserved the underlying meaning of the requirements; which is not possible for natural-language requirements. We demonstrate and evaluate our contributions on a range of complex and industry-scale use cases from safety-critical domains including aerospace and medical devices.