基于EHA模型检验Statecharts

作     者：钱俊彦 古天龙 赵岭忠 QIAN Junyan;GU Tianlong;ZHAO Lingzhong

作者机构：桂林电子工业学院计算机系桂林541004 

出 版 物：《计算机工程》 (Computer Engineering)

年 卷 期：2006年第32卷第3期

页      面：19-21页

核心收录：

学科分类：0810[工学-信息与通信工程] 0808[工学-电气工程] 0839[工学-网络空间安全] 08[工学] 0835[工学-软件工程] 0701[理学-数学] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金："十五"国防预研基金资助项目 广西自然科学基金资助项目(0141046) 

主　　题：模型检验 Statecharts EHA 操作语义 

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