状态图模型的模型检验：综述与研究方向
Model Checking of Statechart Models: Survey and Research Directions
摘要：
我们调查现有的方法，使用模型检验的状态图的形式化验证。虽然在每种方法中使用的状态图的语义和子集有很大的不同，随着模型检查器和它们的规约语言，大多数方法依赖于将层次结构转换为模型检查器的输入语言的平面表示。这使得模型检验难以扩展到工业模型，因为状态空间随着平坦化呈指数级增长。我们看看目前的方法，模型检验层次结构，发现它们的语义是显着不同的状态图。我们建议使用一种技术组合来解决状态空间爆炸的问题，并将其作为进一步研究的方向。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
