Model Checking of Statechart Models: Survey and Research Directions

TL;DR

This survey reviews various methods for model checking statecharts, highlighting challenges with hierarchical structures and proposing future research directions to address state space explosion.

Contribution

It provides a comprehensive overview of existing approaches and suggests new research directions to improve scalability in model checking hierarchical statecharts.

Findings

Most approaches rely on flattening hierarchies, leading to state space explosion.

Current semantics of some approaches differ significantly from original statecharts.

Proposes combining techniques to mitigate state space explosion.

Abstract

We survey existing approaches to the formal verification of statecharts using model checking. Although the semantics and subset of statecharts used in each approach varies considerably, along with the model checkers and their specification languages, most approaches rely on translating the hierarchical structure into the flat representation of the input language of the model checker. This makes model checking difficult to scale to industrial models, as the state space grows exponentially with flattening. We look at current approaches to model checking hierarchical structures and find that their semantics is significantly different from statecharts. We propose to address the problem of state space explosion using a combination of techniques, which are proposed as directions for further research.