基于EHA模型检验Statecharts

摘要：

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

关键词：模型检验、Statecharts、EHA、操作语义

所属期刊栏目：32

分类号：TP301(计算技术、计算机技术)

资助基金：国家预研基金;广西新世纪十百千人才工程基金0141046

在线出版日期：2006-03-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：19-21