Environment Modeling During Model Checking of Cyber-Physical Systems

TL;DR

This paper introduces a domain-independent framework using timed-automata for modeling and refining environments during model checking of Cyber-Physical Systems, making the process more interpretable and accessible to domain experts.

Contribution

A novel framework based on timed-automata that maintains an abstraction tree for environment models, enabling effective and interpretable model checking without requiring formal methods expertise.

Findings

Provides interpretable counter-examples for environment behaviors

Ensures comprehensive coverage of environment variability

Facilitates domain experts' use of model checking

Abstract

Ensuring the safety and efficacy of Cyber-Physical Systems (CPSs) is challenging due to the large variability of their operating environment. Model checking has been proposed for validation of CPSs, but the models of the environment are either too specific to capture the variability of the environment, or too abstract to provide counter-examples interpretable by experts in the application domain. Domain-specific solutions to this problem require expertise in both formal methods and the application domain, which prevents effective application of model checking in CPSs validation. A domain-independent framework based on timed-automata is proposed for abstraction and refinement of environment models during model checking. The framework maintains an abstraction tree of environment models, which provides interpretable counter-examples while ensuring coverage of environment behaviors. With the framework, experts in the application domain can effectively use model checking without expertise in formal methods.