Scenario Generation and Verification of Real-Time Systems

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

Method description A detailed description of the method

The verification of real-time systems with many concurrent tasks easily becomes infeasible due to the large number of possible states that must be covered [MBT-MCF1]. The usual approach to mitigate this problem is to abstract away implementation details up to a level of complexity that makes verification feasible, while still preserving enough implementation details to be useful.

This method aims at reducing the number of possible states by restricting the set of interactions with external components to a set of predefined scenarios i.e., it assumes specific contexts with a predefined behaviour, instead of assuming that any message can be sent to the system being modelled.

The challenge of this approach becomes how to select the right scenarios such that:

most relevant cases are covered, and
a minimal number of scenarios is used.

The behaviour model of the system under evaluation is processed by two different core methods:

a high-level description of the behaviour model is used to produce test cases, i.e., traces of interactions with external components that maximize coverage of the state space of the behaviour model [MBT-MCF3]; and

a more refined description of the behaviour model is used to model check requirements, enriched with the scenarios derived from the test cases and enriched with alternative parameters following a software product lines engineering approach [MBT-MCF2].

Process

Workflow for the combined method on Scenario Generation and Verification of Real-Time Systems

Step 1: Build High-Level Behaviour Model

Input: Informal Behaviour and Timing Requirements.
Processing: Build high-level behaviour model.
Output: High-Level Behaviour Model.

Step 2: Generate Test Cases

Input: Behaviour Model from Step 1, Generation Parameters.
Processing: Generate a test suite for the behaviour model following the generation parameters, using the method Model-Based Testing.
Output: Test Cases.

Step 3: Assemble Scenarios

Input: Informal Behaviour and Timing Requirements, Test Cases from Step 2.
Processing: Build a scenario from the input actions used in the test cases, and for each include the applicable logical properties to be verified from the set of informal requirements.
Output: Abstract Test Cases, Formal Timing Requirements

Step 4: Build/Adapt Refined Behaviour Model

Input: Implementation Details, Real-Time Parameters, High-Level Behaviour Model from Step 1.
Processing: Enrich the high-level behaviour model with more details of the implemented system and with real-time behaviour.
Output: Refined Behaviour Model, Functional and Real-Time Parameters of the behaviour model.

Step 5: Model checking

Input: Refined Behaviour Model, and Parameters from Step 4, Abstract Test Cases and Requirements from Step 3.
Processing: Verify if the requirements hold for their associated scenarios in the given behaviour model, using the method Model Checking Families of Real-Time Specifications.
Output: Real-Time Verification Report for each scenario; Real-Time Specifications and their Configurations.

Step 6: Adapt Models, Scenarios, and Parameters

Input: Real-Time Verification Report and their corresponding Real-Time Specifications from Step 5.
Processing: If errors are found when verifying requirements, iterate and modify the refined behaviour model, the parameters that guide the test suite generation, and the requirements used when assembling scenarios. Otherwise end the workflow and return the verification report.
Output: Fine-tuned generation parameters, final Real-Time Verification Report.

Method Strengths A listof the strengths of the method

Compared to typical model checking of complex specifications with many implementation details, this method requires less states.
Compared to test-based approaches, this method provides stronger guarantees of safety.

Method Limitations The limitations of the method

Model checking complex systems is still memory and computationally expensive, and requires manual fine-tuning of the abstractions until it becomes feasible.
No guarantee can be given that all relevant scenarios are covered.

Method References Bibliography references to papers about the method.

[MBT-MCF1] Christel Baier, Joost-Pieter Katoen: Principles of model checking. MIT Press 2008, ISBN 978-0-262-02649-9, pp. I-XVII, 1-975
[MBT-MCF2] Classen, A., Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A., Raskin, J.F.: Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking. IEEE Trans. Softw. Eng. 39(8), 1069-1089, doi: 10.1109/TSE.2012.86 (2013).
[MBT-MCF3] Software Testing, Verification and Reliability 22(5), 297–312 (2012)

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.