# Model Checking of Statechart Models: Survey and Research Directions

**Authors:** Purandar Bhaduri, S. Ramesh  
**arXiv:** [cs/0407038](https://arxiv.org/abs/cs/0407038)  
**Date:** 2004-07-16  
**Summary page:** https://www.summarizepaper.com/en/arxiv-id/cs--0407038v1/

## Key points

- Authors conduct a comprehensive survey of existing approaches to formal verification of statecharts using model checking
- Statecharts are widely used in software engineering for modeling reactive systems
- Different approaches to statechart verification vary in terms of semantics, subset of statecharts used, model checkers employed, and specification languages utilized
- Most approaches rely on translating hierarchical structure of statecharts into a flat representation compatible with input language of model checker
- Flattening process hinders scalability when dealing with large industrial models due to exponential growth in state space
- Bhaduri and Ramesh explore current approaches to model checking hierarchical structures
- These approaches often have significantly different semantics compared to statecharts
- Proposed combination of techniques as potential directions for further research to mitigate challenges posed by state space explosion in model checking
- Offer promising avenues for improving scalability and efficiency in verifying complex industrial models represented by statecharts

## Summary

In the paper "Model Checking of Statechart Models: Survey and Research Directions," authors Purandar Bhaduri and S. Ramesh conduct a comprehensive survey of existing approaches to the formal verification of statecharts using model checking. Statecharts are widely used in software engineering for modeling reactive systems, but their hierarchical structure poses challenges for model checking. The authors observe that different approaches to statechart verification vary in terms of semantics, subset of statecharts used, model checkers employed, and specification languages utilized. However, most approaches rely on translating the hierarchical structure of statecharts into a flat representation compatible with the input language of the model checker. This flattening process hinders scalability when dealing with large industrial models because it leads to exponential growth in the state space. To address this problem of state space explosion, Bhaduri and Ramesh explore current approaches to model checking hierarchical structures. They find that these approaches often have significantly different semantics compared to statecharts. As a result, they propose a combination of techniques as potential directions for further research which aim to refine and expand upon existing methods in order to mitigate the challenges posed by state space explosion in model checking and offer promising avenues for improving scalability and efficiency in verifying complex industrial models represented by statecharts. Overall, this paper provides valuable insights into the formal verification of statechart models using model checking. It highlights the need for addressing issues related to hierarchical structures and offers potential research directions for overcoming limitations associated with state space explosion.