[Context and motivation] The formal verification of safety-critical software requires formal requirements. Software requirements are often written in natural-language, which then needs to be translated into a formal language for use in verification. [Question/problem] As a requirements set becomes larger and more defined over the course of a requirements engineering project, an ever-increasing amount of work is required to ensure consistency, readability and traceability across the set. Often, dependencies and duplication of information between requirements emerges, which then requires additional work from engineers to update all of the afected requirements when changes need to be made. [Principal ideas/results] We propose that this can be improved by applying refactoring to requirements. Refactoring is a software engineering technique where code is reorganized to improve its internal structure without changing its behavior; in the case of requirements, we can reduce duplication of information and improve readability of the requirements without changing the behavior that the requirements specify. [Contribution] This project aims to provide a working implementation of requirements refactoring in Mu-FRET, a fork of the Formal Requirements Elicitation Tool (FRET) which allows for requirements to be written in a structured natural-language, which is then translated automatically into temporal logic. In addition, we will provide a theory of refactoring that can be generalized to other requirements languages.
requirement in FRET, including its fretish text and corresponding Future-Time LTL translation, are shown in Figure 1.
The readability of fretish requirements makes it much easier to maintain and expand a requirements set as a project progresses. However, requirements engineers still face a number of challenges when managing an industrial-scale specification. As more properties of the system are specified, dependencies between requirements emerge, which can lead to duplication of information across multiple requirements and requires additional work to maintain consistency when updates are made. We propose that this problem can be solved by incorporating refactoring into the requirements engineering process. Refactoring is the process of improving the structure of software without altering its external-facing functionality, and we believe that the techniques used in software engineering can be adapted for requirements engineering. In particular, the aim of this PhD project is to incorporate Refactoring techniques into a fork of FRET, called Mu-FRET1, for use on fretish requirements.
The idea of refactoring fretish requirements originated from experience using FRET in collaboration
with an industrial partner as part of the VALU3S project [
We examined existing literature and selected four refactoring techniques that we felt were applicable
to fretish requirements [
As mentioned above, the main focus of this project is the implementation of four refactoring techniques
into Mu-FRET. At the time of writing, three of these techniques have been implemented (Extract
Requirement, Inline Requirement, and Rename Requirement), with development on the fourth (Move
Definition) currently in progress. We have described these refactorings in detail in previous work [
Extract Requirement moves a definition from one or more “source” requirements into a newlycreated requirement, which also defines a new variable that captures the meaning of the extracted “fragment”. This new variable replaces the fragment in the source requirement(s), preserving the underlying meaning while making the requirements easier to understand and maintain.
Inline Requirement is the opposite of Extract Requirement, taking one requirement and merging it into another. The most basic implementation of Inline is as the direct inverse of Extract, operating on source requirements of the form “if CONDITION System shall satisfy RESPONSE”, replacing CONDITION with RESPONSE in any selected destination requirements. However, the applicability of Inline Requirement to requirements of other forms (such as those that include a timing constraint that may-or-may-not align with that of the destination) is an open question that I intend to explore.
Rename Requirement changes a requirement’s name and then updates any references to it to match its new name. FRET already allows a user to rename a requirement, but this existing functionality does not update the ’Parent Requirement ID’ field of any of the target’s child requirements. This leaves those child requirements with a broken reference, forcing manual updates across the set. Mu-FRET’s implementation of the Rename refactoring solves this problem, maintaining consistency.
In addition, robust renaming is very important when considered alongside Extract Requirement, which creates a variable which directly corresponds to the extracted definition. It is important that the names of this requirement and variable stay aligned so that the connection is maintained, and thus Rename Requirement is able to rename both an extracted requirement and it’s corresponding variable in a single user-facing action, with the variable name being updated in every requirement where that variable is used. This ability to rename a variable and have it propagate across multiple requirements is not present in the original build of FRET.
Move Definition takes part of one requirement and moves it to another, focusing a requirement on a single responsibility. It difers from Extract Requirement and Inline Requirement in that it does not alter the number of requirements in the set, it only moves definitions between requirements.
Each of these refactoring techniques will be integrated with formal checks that the behaviour of the requirements before the refactoring is the same as after the refactoring, by checking equivalence of the temporal logic formulae using the NuSMV model checker. The exact nature of this check varies depending on the refactoring in question; for example, Extract Requirement checks that the updated source requirement combined with the newly-extracted requirement matches the original version of the source requirement before refactoring, and the extraction is only performed if this check succeeds.
This work is primarily based on the framework for refactoring natural-language requirements outlined
by Ramos et al. [
As far as we are aware, there is little existing work on applying refactoring to formal or semi-formal
requirements, and there is essentially no tool-support for it. Similar work has been conducted by Xuan
et al. on using refactoring to improve test suites for analysis of source code [
This project seeks to answer the following research questions: • RQ1: To what extent are software refactorings applicable to functional requirements? • RQ2: Under precisely what conditions are requirement refactoring techniques applicable? What elements of the structure of a requirement might allow or prevent the use of one or more refactoring techniques? • RQ3: How can refactoring techniques developed for fretish requirements be generalised for other requirements languages and formalisms?
The first step in answering these questions will be to complete an intitial implementation of the four chosen refactoring methods. By developing support for refactoring in a requirements engineering tool, we will be able to test how it can be applied to real sets of requirements. Also, the process of developing the software forces us to codify exactly how the refactorings behave; this behaviour can be updated as the theory behind the refactoring process matures, but it is valuable to have a concrete implementation to build from.
Once development on the four refactorings is complete, we aim to evaluate the applicability of each
on a number of case studies. This will address Research Question 1. These case studies include the
aforementioned Aircraft Engine Controller requirements from VALU3S, a set of requirements for a
Mechanical Lung Ventilator developed for the ABZ 2024 case study [
In addition, we will examine the efect that refactoring has on the underlying meaning of the requirements, represented by the LTL formulae. At present, the Mu-FRET refactorings are focused primarily on improving the structure of the fretish text of the requirements, with the LTL translations used for checking consistency. However, we want to investigate if a requirement’s logical representation can be used to determine whether a given refactoring can be applied. In doing so, we hope to arrive at a set of well-defined criteria for each refactoring that describes exactly when that technique can be used, and when some part of the requirement prohibits its use, addressing Research Question 2. Also, any results gathered from focusing on the LTL specification should be more easily generalisable to requirements languages other than fretish, as temporal logics are commonly used in requirements engineering and formal methods. This aligns with Research Question 3.
The implementation of refactoring in Mu-FRET is nearing completion, with two tasks remaining: implement Move Definition, and incorporate NuSMV checks into Inline, Rename, and Move. These tasks are the current highest priority for this project.
Although we have described the Move Definition refactoring in previous work, the exact details of the implementation are not entirely clear. Exactly what parts of a requirement can be moved, and which other requirements are valid options for the movement, will need to be decided during the development process. We have also considered a specialised form of Move Definition called Pull-Up Definition , which would move a definition from a child requirement into its parent, representing the idea that the definition is common to all of that requirement’s children. Implementing this in Mu-FRET is being considered.
Implementing model checking with NuSMV into the remaining refactorings should not pose a significant challenge, as the capability has already been demonstrated with Extract Requirement. The dificulty will be in deciding exactly what properties should be checked, and ensuring that the implementation is robust when multiple diferent refactorings are performed on the requirements set over the course of a project.
After all four refactorings have been fully implemented, we will investigate the limitations of the implementation and the conditions that are required to perform refactoring. In essence, our goal is to find the “weakest precondition” for each refactoring, and thus define the widest possible set of requirements that can be refactored. We suspect that the most challenging refactoring to define will be Inline Requirement, because it is often performed with the intention of deleting the source requirement after the inlining has been performed. This means that we need to consider all of the information that a requirement contains across all of its fields, to ensure that none of that information is lost in the refactoring process. Expanding the application of Inline Requirement to arbitrary requirements of a suitable structure, rather than being limited to those generated by Extract Requirement, represents a notable challenge for this project but also a significant result once complete.
After this, as mentioned above, we will investigate how the refactorings change not only the fretish text, but also the equivalent Temporal Logic semantics as well. We will need to examine the temporal logic semantics generated by FRET to find any consistent efects of refactoring the fretish text. Also, there are questions on how exactly our extracted requirements are templated, which arose from the temporal logic translation. We will need to examine what the optimal template is for specifying the extracted definitions, and this requires a deeper understanding of the relationships between the requirements and how refactoring may afect them.
We are underway with an investigation into the application of refactoring on functional requirements. Four refactoring techniques are being implemented in the Mu-FRET tool; three are already implemented and available for use, while the fourth is set to be developed in the near future. The usefulness of these refactorings will be evaluated on at least three case studies, with others from the literature being considered. We will use the temporal logic semantics for the requirements generated by Mu-FRET to draw conclusions about requirements refactoring that can be applied more broadly to other requirements languages.