Requirements Formalization
Meta-Information
Origin: Darren Sexton, Peter Gilhead / RICARDO
Written: November 2014
Purpose: Generate formal requirements based on Natural Language Requirements (NLR), which can subsequently be used for formal analysis and model checking.
Context/Pre-Conditions: Requirements are to be used downstream in formal modelling, verification, or testing tools.
To consider: Learnability of structured requirements and boiler-plates. More rigorous analysis of requirements to reduce ambiguity and increase precision. Forces consideration of timing between requirement conditions and resulting actions.
Used Terms: (Brian Nielsen, Peter Gilhead, Wolfgang Herzner)
NL: Natural Language.
Structured (semi-formal): NL, using predefined structure(s) and patterns (templates).
Formal: written in a machine processable language with underlying formal semantics (e.g. temporal logic).
.
Structure
Participants and Important Artefacts
Requirements Engineer: is responsible for collecing and describing system requirements in collaboration with other domain experts.
Peers: Requirements engineering team (requirements engineer, domain experts, technical V&V experts.
Formal Verification Engineer: Expert in formal methods, formal requirements specification language, and formal verification techniques.
.
Actions / Collaborations
(1) Write NLR (Natural Language Requirements): Requirements are collected and written in a structured way that eases subsequent formalisation; e.g. using appropriate templates (boilerplates).
(2) Peer Review: The drafted structured requirements are reviewed by the „Peers“ (the Requirements engineering team consisting of requirements engineers, domain experts, technical V&V experts) wrt. correct behavior and testability/verifyability, and criteria:
– A requirement may then need to be re-written.
– Not all requirements may be well suited for formalization (eg. complex algorithms). These should be handled informally for using other formalization approaches.
(3) Formalization: The set of requirements are fully formalized and formally consistency checked, and ready to be used for downstream development and (automated) V&V:
(3.1) Requirements are analysed to determine Trigger, Action and Timing conditions.
(3.2) The semi-formal representation of the requirements can be consistency-checked for conflicts (e.g. OFFIS BTC plug-in).
(3.3) Formal requirements generated by associating trigger, action and timing conditions with actual model signals and/or code variables.
(3.4) This step is to review the signal/variable based expressions used for formal requirements triggers/actions/timing, to increase confidence they are correct before trying to use them.
(3.5) Analyse formal requirements – consistency, conflicts, omissions (e.g. Are all output signals used, are all input signals used? Are all requirement actions reachable? Can all trigger conditions be achieved?).
.
Discussion
Benefit: Application of the pattern results in more precise requirements that are less ambiguous, and that are easier to fully formalize.
Comments (from Darren Sexton, edited by Wolfgang Herzner):
The traditional guidance that a requirement must be “testable” should be extended in the context of this pattern to ensure that the requirement can be formalised. In the first instance this means applying standard good requirements writing practice. Then the requirements that are suitable for formalisation must be identified, and for those the specific characteristics relevant to formalising requirements must be considered.
It must be recognised that not all requirements (or more specifically, the underlying functionality they describe) will be suited to formalisation. Typically requirements suited to formalisation are those describing trigger-response behaviour, state-machine type behaviour, logical behaviour, ordering behaviour or invariants. Requirements less suited to formalisation will be those that are highly algorithmic in nature. The limitations of what can sensibly be formalised must be explicitly recognised in order to avoid wasted effort and frustration with the approach.
One aspect is that the formalisation process will often raise detailed questions that are missed in traditional approaches; for example, the time interval between a trigger occurring and the response being initiated is often left unstated for cases where it is effectively “immediate”. Yet formal verification based on the formal requirements will need to know what delay is acceptable or not (for instance).
Similarly, the context of requirements is often assumed from the location in a requirements document; for example, a requirement in a section related to a specific mode is often read by implementers and verification engineers as only applying when in that mode. However, when formalised, that implied context is lost and must instead clearly stated as a pre-condition.
A third aspect relates to assumptions; once again, the precision of later formal verification means that assumptions that are often implied must instead be stated explicitly. These assumptions can then be formalised alongside the requirements and so influence the later activities.
Therefore the original requirements writing process must consider the level of precision stated within the natural language requirements and the degree of freedom given (or not) to the formalisation engineer to make decisions autonomously; such decisions must be documented within the guidance from the start.
One approach is to use a more structured approach when writing the natural language requirements. A light-weight approach to do so is to use “boilerplates” (also called “patterns” or “templates”). These provide a structure of a requirement in which the author can “fill in the blanks”. This promotes consistency across requirements, which by itself reduces the formalisation effort as common formalisations will be identified and re-used. This can be taken further by mapping the boilerplates to suggested formalisations, saving effort and reducing the risk of errors within the formalisation process.
When writing for formalisation it is important not to lose sight of the primary audiences for the requirements; the formalisation engineers are not the only, or even most important, audience for the natural language requirements. Additionally, it will often be the case that other engineers will not be familiar with the formal notation the requirements are translated into. As such, the original natural language requirements will have an important role during later activities. Given this, the natural language requirements must remain in a style convenient for a human audience, rather than one that is rendered unnatural in order reduce the gap for particular formal notation.
.
Application Examples
MBAT Automotive Use Case 1 (Brake by Wire) / Scenario 01 (Create requirement model) and Scenario 02 (Analysis on the analysis model):
Participants:
User: Volvo
Tool provider: Dassault, OFFIS, MDU
Tools (Artefacts):
Enovia Requirement Central (Dassault): NLR
Pattern Editor (OFFIS): NLR
ViTAL (MDU): Formalization of requirements
MBAT Automotive Use Case 5 (Transmission Controller Product Line) / Scenario 03 (Automatic TCG):
Participants/ Artefacts:
Requirements Engineer:
Tools: DOORS, Ricardo (prototype) DOORS infrastructure for boilerplates
Aids: Boilerplates training, guidance and „quick reference card“
Peers:
Tools: none
Aids: Boilerplates training, guidance and „quick reference card“
Note: Largely an existing activity outside the scope of MBAT, but has extra elements related to checking the natural language requirements are suitable for formalisation.
Formal Verification Engineer:
Tools: BTC-EmbeddedSpecifier to formalise requirements
Note: OFFIS ConsistencyAnalyzer to perform conssitency & entailment checks on (semi-)formal requirements.
MBAT Automotive Use Case 8 (Virtual Prototype Airbag ECU) / Scenarios 01-04:
Participants/ Artefacts:
Requirements Engineer: NLR in .xls format
Peers: .xls requirements accessible via Enovia
Formal Verification Engineer: Semi-formalization of requirements in DODT with use of boilerplates (XML, .xls). Formalization of requirements and consistency check through MoMuT::REQs in MBAT requirements meta model format
Description: The first step is to translate the natural language requirements (NLR) into semi-formal requirements using boiler plates in DODT. Those requirements can be analyzed before they are forwarded. The second step is the formalization of the requirement to generate the test and analysis model using MoMuT::REQs. Those formalized requirements are checked for consistency to see if they contradict each other. The final outcome of the analysis is a consistent set of requirements.
MBAT Aerospace Use Case 5 (DeViLa) / Scenario 09 (Usage of Formal Analysis Model):
Participants/ Artefacts:
Requirements Engineer: capture/writes requirements in IBM Rational DOORS as NLRs.
Peers are system engineers, domain experts, technical experts, SW engineers, perform review on these input requirements.
Formal Verification Engineer: semi-formalizes a suitable subset of the NLR requirements making use of BTC Embedded Specifier. For the subset macros and patterns are defined. Finally contracts are defined including assumptions and commitments.
.
Relations to other Patterns
| Pattern Name | Relation* |
| Preserve Requirements across Abstraction Levels | This pattern (Requirement Formalization) eases work of that pattern |
| Support Safety Analysis by Faults Simulation | This pattern (Requirements Formalization) helps that pattern in step Formalize Requirements |
| Model-based Safety Analysis with Fault Injection | This pattern (Requirements Formalization) helps that pattern in step Formalize Requirements |
| Model and Refinement Checking | Both patterns use similar methods |
| Formalized Analysis and Verification | Both patterns use similar approaches |
| Statistical Model Checking | Both patterns use similar approaches |
* “this pattern” denotes the pattern described here, “that pattern” denotes the related pattern