Behaviour-driven formal model development

Process for model-based, rigorous system development to derive a validated and formally proven behavioural model including test cases for checking some implementation.

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

Method description A detailed description of the method

Behaviour-Driven Formal Model Development aims to address the issue that domain expertise and formal modelling are often not in the skill set of a single person.

The process is shown in Figure ‎3.7. The approach uses scenarios in the sense of Behaviour Driven Development [BFM1, BFM2] to allow the domain expert to specify examples (Manual Scenarios) for the expected operation of the system. Based on the Requirements and the Manual Scenarios, the formal methods expert builds a Safe Model that covers both safety and functional requirements. Using formal methods like refinement proofs and model checking, safety properties of the model are guaranteed. In the next step, Behaviour Verification, the Manual Scenarios are run against the model, thereby ensuring that the Behavioural Verified Model is not only safe but also does what it is expected to do. Next, the scenarios’ coverage of the model is evaluated and additional scenarios to achieve higher coverage are generated. The Generated Scenarios are then reviewed by the domain expert in an Acceptance Testing step by indirectly reviewing any additional behaviour included in the model. The combined set of scenarios can later contribute to ensuring that a specific implementation complies with the model.

The concept of Behaviour-Driven Formal Model Development has been introduced in [BFM3] and applied to a new standard for railway operations in [BFM4].

Figure ‎3.7 Steps of Behaviour-Driven Formal Model Development

Method Strengths A listof the strengths of the method

Allows for verified (functional) safety without neglecting operational soundness/expected functionality.
The process allows to split work between different skill sets. Domain expert and formal methods expert use scenarios as one means of communication. The domain expert does not need to understand the formal method to validate the formal model.
Manually derived and automatically generated scenarios can be used as test cases for the implementation, to ensure that the implementation adheres to the formal model.
Problems found in the implementation through testing can be traced back to top-level and derived requirements.

Method Limitations The limitations of the method

Fits best to event-triggered behaviour, less to continuous or data-driven functionalities.

Method References Bibliography references to papers about the method.

[BFM1] North, D.: Introducing BDD. Better Software Magazine (Mar 2006)
[BFM2] Smart, J.F.: BDD in Action: Behavior-Driven Development for the Whole Software Life cycle. Manning Publications Company (2014)
[BFM3] Snook C. et al. (2018) Behaviour-Driven Formal Model Development. In: Sun J., Sun M. (eds) Formal Methods and Software Engineering. ICFEM 2018. Lecture Notes in Computer Science, vol 11232. Springer, Cham. https://doi.org/10.1007/978-3-030-02450-5_2
[BFM4] M. Butler et al., "Behaviour-Driven Formal Model Development of the ETCS Hybrid Level 3," 2019 24th International Conference on Engineering of Complex Computer Systems (ICECCS), Guangzhou, China, 2019, pp. 97-106, doi: 10.1109/ICECCS.2019.00018.

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.