Abstract: Model checking is one of the most practical techniques of automatic formal verification to ensure the correctness of design specifications. Statecharts that extends traditional finite state machines is a visual language for specifying the behavior of complex reactive system. The paper gives an approach of model checking Statecharts based on EHA for verifying whether Statecharts model satisfies the required properties. Firstly, it converts the system model Statecharts into the Büchi automaton ASC by EHA operation semantics, and builds the Büchi automaton A?φ. for LTL formula φ. Secondly, constructs the product automaton ASC ?A?φ. Finally, checks whether the product automaton generates the empty languages, and verifies whether Statecharts satisfies the required properties.

Key words: Model checking; Statecharts; EHA; Operation semantics

摘要： 模型检验是一种重要的形式化自动验证技术。Statecharts 是一种用以规约复杂反应式系统行为的可视化语言。为了验证Statecharts模型是否满足所期望的性质，该文给出了一种基于EHA 模型检验Statecharts 的方法，首先把Statecharts 转换为EHA，通过其操作语义得到Büchi 自动机，然后与LTL 公式所得的Büchi 自动机相乘，最后检查该乘积自动机所能接受的语言是否为空，来判断是否满足所期望的性质。

关键词: 模型检验；Statecharts；EHA；操作语义