Tool Support for Validation of Formal System Models: Interactive Visualization and Requirements Traceability

TL;DR

This paper introduces the VisualisierbaR tool that leverages interactive visualization and requirements traceability to support the validation of formal system models, particularly in railway operations, reducing cognitive effort.

Contribution

The paper presents a novel tool that applies visualization and traceability concepts to improve formal model validation in safety-critical systems.

Findings

Supports formal modeling of railway operations

Uses interactive visualization for validation

Incorporates requirements traceability concepts

Abstract

Development processes in various engineering disciplines are incorporating formal models to ensure safety properties of critical systems. The use of these formal models requires to reason about their adequacy, i.e., to validate that a model mirrors the structure of the system sufficiently that properties established for the model indeed carry over to the real system. Model validation itself is non-formal, as adequacy is not a formal (i.e., mathematical) property. Instead it must be carried out by the modeler to justify the modeling to the certification agency or other stakeholders. In this paper we argue that model validation can be seen as a special form of requirements engineering, and that interactive visualization and concepts from requirements traceability can help to advance tool support for formal modeling by lowering the cognitive burden needed for validation. We present the VisualisierbaR tool, which supports the formal modeling of railway operations and describe how it uses interactive visualization and requirements traceability concepts to validate a formal model.