Modular Formal Requirements-Driven Verification

Method Purpose Short description of the method's purpose and main benefits

Method description A detailed description of the method

This method extends the base method, Formal Requirements-Driven Verification, to support refactoring of requirements and hence improve the modularity of requirements. Often, natural-language requirements have a lot of repetition of concepts across different individual requirements. Similar to repeated code in programs, this makes the requirements difficult to update. When translated into formal or semi-formal notations during the requirement engineering process, this can lead to confusion and extra work.

We introduce refactoring steps for specific requirements engineering tool chains that enable practitioners to refactor their requirements so that they are easier to read, understand, and maintain. This is based on requirements refactoring literature like [MFRDV1], and ultimately program refactoring [MFRDV2]. Such refactoring steps allow us to address dependencies amongst requirements and reduce the repetition of definitions. Integrating the refactoring steps into the specific tool chains speeds up refactoring and enables the refactoring steps to be automatically checked – for example to formally prove that they have only altered the form of the requirements, not their function.

Method Strengths A listof the strengths of the method

Quicker Translation to Formal Specifications
Identification of ambiguities in natural language requirements at an early stage in the development process.
Formal specifications are based on formal requirements and linked to the system model.
Intermediate language used to avoid requirements engineers needing to learn a formal language
Modular requirements that are easier to maintain as development progresses
Traceability and explainability are improved because the individual requirements themselves are simplified

Method Limitations The limitations of the method

Additional to the limitations of the base method:

Not all requirements can be formalised, depending on the tool that is used.
Requirements engineers still must understand the intermediate language (though this is a much lower burden than learning a formal language).
Not all requirements can be refactored/modularised effectively.
Not all software refactorings are suitable to apply to FRETISH requirements.

Method References Bibliography references to papers about the method.

[MFRDV1] Ramos, R., Piveta, E. K., Castro, J., Araujo, J., Moreira, A., Guerreiro, P., Pimenta, M. S., Price, R. T. Improving the Quality of Requirements with Refactoring. (2007) Simposio Brasileiro De Qualidade De Software (pp. 141-155). SBC. https://doi.org/10.5753/sbqs.2007.15573
[MFRDV2] Fowler, M. Refactoring: Improving the Design of Existing Code, 2018. Addison-Wesley Professional.

Method Dimensions

Evaluation Environment Type Type of environment where the method is applied. It can be more than one type of environment. (Dimension 1)

Evaluation Type Type of evaluation performed with that method. If a method is hybrid, more than one type can be selected. (Dimension 2)

Type of Component Under Evaluation Type of components that can be evaluated with that method. It can be more than one type. (Dimension 3)

Evaluation Stage The evaluation stage where the method is used. (Dimension 5)

Purpose of the Component Under Evaluation The type of purpose that can be evaluated by a method. It can be more than one type. (Dimension 6)

Type of Requirement Under Evaluation The type of requirements that a method is able to evaluate. It can be more than one type. (Dimension 7)

Evaluation Performance Indicator The type of evaluation criteria or KPI that a method is able to improve. It can be more than one type. (Dimension 8)

Relations

Related Methods A method could be related to other methods.

Tools A method can use zero or more tools.

Part Method A method (when it is a combination: Combination of method artefact that is a specialization of a V&V Method) could be composed of a set of V&V Methods.

Test Case or Verification and Validation activity Test Case or V&V activity performed in a Use Case. We will link to the method to the test cases where the method is used.

Standards A method can be linked with standards.

Context

Workflow

Contents

There are currently no items in this folder.