| 模型检测中的CTL形式化描述模板 |
| |
| 引用本文： | 陈志远,黄少滨,白玉,纪明宇.模型检测中的CTL形式化描述模板[J].哈尔滨工程大学学报,2013(4):483-487. |
| |
| 作者姓名： | 陈志远 黄少滨 白玉 纪明宇 |
| |
| 作者单位： | 哈尔滨工程大学计算机科学与技术学院 |
| |
| 基金项目： | 国家自然科学基金资助项目(71272216,60903080);国家科技支撑计划课题资助项目(2009BAH42B02,2012BAH08B02);中央高校基本科研业务专项资金资助项目(HEUCF100603,HEUCFZ1212) |
| |
| 摘 要： | 针对SPS(specification pattern system)和Prospec(property specification)不能将组合命题形式化为模型检测器可以接受的CTL(computation tree logic)公式问题,通过研究SPS和Prospec产生系统性质描述的形式化方法,并对比CTL与FIL(future interval logic)的表达能力以及CTL与LTL(linear temporal logic)两者之间的关系,构造了一类具有较强描述能力的CTL公式模板,并通过重新定义合取逻辑运算符来简化公式.该类模板简洁且易于理解.模板类的正确性证明表示该类模板可以有效地描述系统性质.利用该模板得到的CTL公式可以直接应用到模型检测器中,利于系统性质验证.
|
| 关 键 词： | 模型检测 形式化描述 SPS Prospec CTL模板 |
| 本文献已被 CNKI 等数据库收录！ |
|
