模型检测中的CTL形式化描述模板

• 作者: 白玉 纪明宇 陈志远 黄少滨
• 来源期刊: 哈尔滨工程大学学报
• 学科: 工学
• 关键词: 模型检测 形式化描述 SPS Prospec CTL模板
• 年，卷（期）: 2013,（4）
• 页码范围: 483-487
• 页数: 5页
• 分类号: TP311.5
• 字数: 4808字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-7043.201210015

摘要

针对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公式可以直接应用到模型检测器中,利于系统性质验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄少滨	哈尔滨工程大学计算机科学与技术学院	55	319	10.0	15.0
2	陈志远	哈尔滨工程大学计算机科学与技术学院	12	46	5.0	6.0
3	白玉	哈尔滨工程大学计算机科学与技术学院	11	33	4.0	5.0
4	纪明宇	哈尔滨工程大学计算机科学与技术学院	8	18	2.0	3.0