2004/07/16 by Purandar Bhaduri, Bhaduri, Purandar, S. Ramesh +1 · 1 voice
Computer Science · #Formal Methods in Verification #Software Reliability and Analysis Research #Software Testing and Debugging Techniques #cs.SE
paper · pdf · doi:10.48550/arxiv.cs/0407038
arxiv created 2004/07/16 · openalex publication_date 2004/07/16 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.