Classical Formal Verification Driven by Formal Requirements

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

Method description A detailed description of the method

Traditional formal methods (such as model checking and theorem proving) exhaustively check and prove that a description of the system exhibits some properties. One problem lies in ensuring that the properties adequately reflect the system’s actual requirements. This link between requirements and formal methods is easier to make if the requirements themselves are formalised. However, requirements are often expressed in natural language, and often at a level of detail that is not suitable for direct formalisation, hence this combination of methods.

Eliciting the system’s requirements and formalising them is a task best completed by a collaboration between those knowledgeable about the system and those knowledgeable about formalisation. But using a formal language during this process can slow down progress, as the systems engineers are taught the intricacies of the formal method, and the formalists try to formalise too much detail too quickly. Thus, in the Part Method ‘Formal Requirements-Driven Verification’, a semi-formal language is used as an intermediate between natural and formal languages. This frees up the requirements elicitation process, but still provides enough formalisation to both reduce ambiguities and make the requirements easier to formalise later on. Our approach uses NASA’s Formal Requirements Elicitation Tool (FRET) for requirements elicitation and formalisation in the FRETISH language [SFM+ MCH/TPS2].

Once the requirements elicitation and formalisation phase are done, the requirements can be translated into the relevant input language for the formal method(s) chosen for the verification phase. This translation could be automatic or described by a set of systematic translation rules to apply manually. Again, this depends on the formal method(s) that have been chosen and the available tool support. If the design is described in a Simulink diagram, existing tool-support can take formalised requirements and produce contracts compatible with Simulink, such as CoCoSim SFM+ MCH/TPS3]. Where the design has not been described using Simulink, or where the verification efforts would benefit from other formal approaches, we can build a formal model of the system from the available descriptions (the requirements, other models, documentation, etc.) and check the properties (formal encodings of the requirements) against the model.

There are three phases of this method and each is made up of steps. Phases 2-A and 2-B can be run in parallel.

Phase 1: Formalise Requirements

Step 1: Requirements Elicitation

Input: Natural-Language Requirements
Processing: An informal process of discussing the natural-language requirements to clarify and reduce ambiguity; this also may uncover new requirements.
Output: Natural-Language Requirements

Step 2: Requirements Formalisation

Input: Natural-Language Requirements
Processing: A manual process of converting the natural-language requirements into FRETISH.
Output: Semi-Formal Requirements, LTL Specification of Requirements

Phase 2-A: FRET-Supported Verification

Step 1: Attach Simulink Model

Input: Semi-Formal Requirements, Simulink Diagram
Processing: Attach Simulink diagram to the requirements project
Output: N/A

Step 2: Generate Verification Conditions

Input: Semi-Formal Requirements,
Processing: Add variable types to match the Simulink diagram, then automatically produce contracts.
Output: CoCoSpec Contracts

Step 3: Formal Verification

Input: Simulink Diagram, CoCoSpec Contracts
Processing: Incorporate the CoCoSpec Contracts into the Simulink diagram, then the formal verification occurs during the simulation runs.
Output: Formal Verification Results

Step 4: Evaluate Results

Input: Formal Verification Results
Processing: Manually check that the verification passes or fails, if the latter then why?
Output: Evaluation Report

Phase 2-B: FRET-Guided Verification

Step 1: Translate to Verification Conditions

Input: Semi-Formal Requirements
Processing: Translate the Semi-Formal requirements into the chosen formalism
Output: Formal Verification Properties

Step 2: Build Formal System Model

Input: Formal Verification Properties, Natural-Language Requirements
Processing: Build a formal model of the system using the available information about its behaviour. Validate formal system model as an adequate representation of the system.
Output: Formal System Model

Step 3: Formal Verification

Input: Formal Verification Properties, Formal System Model
Processing: Verify that the formal system model preserves the properties.
Output: Formal Verification Results

Step 4: Evaluate Results

Input: Formal Verification Results
Processing: Manually check that the verification passes or fails, and if the latter then why?
Output: Evaluation Report

Phase 3: Generate Verification Report

Method Strengths A listof the strengths of the method

Leveraging the strengths of multiple formal methods.
Reducing or removing ambiguities in the requirements
Building a connection between modelling tools (e.g. Simulink) and verification tools (e.g. Model checkers)
Traceability from natural language requirements to formally verified artifacts.
Facilitating communication between formal and non-formal methods practitioners
Formal verification of requirements at an early stage in the development process where requirements are analysed and formalised with formal methods in mind from the beginning.
Provides a process for the formal verification of software models.

Method Limitations The limitations of the method

Manual requirements engineering still required
Possible inconsistencies between requirements formalisation and property specification in distinct tools/formalisms.
Possible inconsistencies between formal models if multiple formal models are developed, potentially at varying levels of abstraction.
Lack of formalised/systematic translation rules between requirements and formal models

Method References Bibliography references to papers about the method.

[SFM+ MCH/TPS1] Rozier, Kristin Yvonne, "Specification: The Biggest Bottleneck in Formal Methods and Autonomy" (2016). Verified Software. Theories, Tools, and Experiments (pp. 8-26). Springer. https://doi.org/10.1007/978-3-319-48869-1_2
[SFM+ MCH/TPS2] Giannakopoulou, D., Pressburger, T., Mavridou, A., & Schumann, J. (2020). Generation of formal requirements from structured natural language. In International Working Conference on Requirements Engineering: Foundation for Software Quality (pp. 19-35). Springer. https://doi.org/10.1007/978-3-030-44429-7_2
[SFM+ MCH/TPS3] Bourbouh, H., Garoche, P. L., Loquen, T., Noulard, É., & Pagetti, C. (2020). CoCoSim, a code generation framework for control/command applications An overview of CoCoSim for multi-periodic discrete Simulink models. European Congress on Embedded Real Time Software and Systems.

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.