Model Checking Families of Real Time Specifications using Annotations and Configuration Tables

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

Method description A detailed description of the method

Model checking [MCF-AC1, MCF-AC2, MCF-AC3] is a method to verify if a model of the system under verification satisfies its requirements. In complex models verification becomes infeasible due to the large state space, requiring many small variations of the model, one for each set of related requirements. Typically, these variations are built independently, intersecting efforts, and not guaranteeing that they are kept consistent.

This method explores how to define this set of variations and respective requirements based on a single configurable model, leveraging on principles from software product line engineering (SPLE) [MCF-AC4], which are here applied to formal specifications rather than software specifications. It focuses on the UPPAAL real-time model checker [MCF-AC5], and proceeds in two phases: (1) annotation of the specifications, and (2) automatic configuration of these annotated blocks via a product line of specifications.

Annotated Specifications

In many cases, the relation between the abstract model and the implementation is maintained via personal meetings and reports using natural languages. Automatizing this synchronisation involves a large effort and is in many cases impractical (e.g., learning abstract models by running concrete systems [MCF-AC6]). Our approach involves using a set of tables in Microsoft Excel to maintain the key parameters of the formal models, including scenarios and requirements of the system. This set of tables is easy to be read and modified by both developers of the system and by developers of the formal models and is automatically entangled with the models used by the formal analysis tools. On one hand, the system developers can update this table and check which requirements can be verified; on the other hand, the designers of the formal models can adapt the model to either include new details, or to relax aspects that introduce state explosions. By using an intermediate representation of the core parameters of the formal specifications, we reduce the expected knowledge of the system developers over formal models. This includes ranges of estimated time executions of individual components, the number of times certain actions may occur, and sequences of input scenarios. Experts in formal modelling are kept in the loop to refine the models and property specifications as needed.

Product Line of Specifications

A common approach to avoid exploring too many states while trying to verify a property is to bound the state space. Some tools support bounded model checking, limiting the depth of search in the state space. Our approach supports the specification of variants, where the state-space can be reduced by modifying different parameters of the specification. For example, 2 variants could remove 2 independent parts of the specification, allowing the verification of properties for these two variants instead of the full model. Ultimately, the goal is to verify a large-enough set of variants to cover the relevant cases without incurring in state-space explosions.

The method workflow is described in Figure ‎2.4. The informal behavioural description, different parameters, input scenarios, and requirements are provided as input. These are used to manually build: (1) an initial global and annotated real-time specification, and (2) a collection of Excel tables with information on how to populate the annotated blocks of the specifications and with the set of requirements. Our own tool (Uppex) is then used to automatically apply the configurations in the Excel tables to the annotated specifications, producing a set of specification instances. These are also automatically analysed via UPPAAL, with a provided time-out, and a report is produced over which requirements hold in which configuration. The instances can also be manually inspected within UPPAAL, leading to a manual refinement of the annotated specifications and the Excel tables, until all desired requirements are met for a rich enough set of configurations. Early results have been accepted in the proceedings of the conference RSSRail 2022 [MCF-AC-7].

Method Strengths A listof the strengths of the method

More automation - making model checkers easier to use for non-experts who only need to modify a configuration table

Method Limitations The limitations of the method

In addition to the limitations inherited from “Model Checking Families of Real Time Specifications”, this improved method addresses the complexity of the models and the effectiveness to prove properties, with the following remaining limitations:

Each requirement can be proven to hold in specific variations of the model, but it is difficult to quantify how complete are these variations w.r.t. the most complete model.
Finding the set of variations that can satisfy a given requirement without timing out is sometimes difficult.

Method References Bibliography references to papers about the method.

[MCF-AC1] Edmund M. Clarke, Orna Grumberg, Doron A. Peled: Model checking. MIT Press 1999, ISBN 978-0-262-03270-4

[MCF-AC2] Christel Baier, Joost-Pieter Katoen: Principles of model checking. MIT Press 2008, ISBN 978-0-262-02649-9, pp. I-XVII, 1-975

[MCF-AC3] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem: Handbook of Model Checking. Springer 2018, ISBN 978-3-319-10574-1

[MCF-AC4] Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-Oriented Software Product Lines: Concepts and Implementation. Springer (2013).

[MCF-AC5] Gerd Behrmann, Alexandre David, and Kim G. Larsen: A Tutorial on UPPAAL. LNCS 3185, pp 200-236. Springer-Verlag (2004).

[MCF-AC6] Falk Howar and Bernhard Steffen: Active Automata Learning in Practice, LNCS 11026, Springer-Verlag, DOI: 10.1007/978-3-319-96562-8_5 (2018).

[MCF-AC7] José Proença, Sina Borrami, Jorge Sanchez de Nova, David Pereira and Giann Nandi : Verification of multiple models of a safety-critical motor controller in railway systems, in the proceedings of RSSRail2022, to appear (2022)

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.