Tool Support for Validation of Formal System Models: Interactive Visualization and Requirements Traceability
This work addresses the problem of ensuring model adequacy for certification agencies and stakeholders in engineering disciplines like railway systems, but it is incremental as it builds on existing concepts from requirements engineering.
The paper tackles the challenge of validating formal system models for safety-critical systems by proposing that model validation is a form of requirements engineering, and it introduces the VisualisierbaR tool, which uses interactive visualization and requirements traceability to reduce cognitive burden in validating formal models of railway operations.
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.