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

作     者：陈志远 黄少滨 白玉 纪明宇 CHEN Zhiyuan;HUANG Shaobin;BAI Yu;JI Mingyu

作者机构：哈尔滨工程大学计算机科学与技术学院黑龙江哈尔滨150001 

出 版 物：《哈尔滨工程大学学报》 (Journal of Harbin Engineering University)

年 卷 期：2013年第34卷第4期

页      面：483-487页

核心收录：

学科分类：08[工学] 0817[工学-化学工程与技术] 0807[工学-动力工程及工程热物理] 0827[工学-核科学与技术] 0802[工学-机械工程] 0703[理学-化学] 0825[工学-航空宇航科学与技术] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 0801[工学-力学（可授工学、理学学位）] 

基　　金：国家自然科学基金资助项目(71272216 60903080) 国家科技支撑计划课题资助项目(2009BAH42B02 2012BAH08B02) 中央高校基本科研业务专项资金资助项目(HEUCF100603 HEUCFZ1212) 

主　　题：模型检测 形式化描述 SPS Prospec CTL 模板 

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