%0 Journal Article
%T 模型检测中的CTL形式化描述模板
%A 陈志远
%A 黄少滨
%A 白玉
%A 纪明宇
%J 哈尔滨工程大学学报
%P 484-487
%D 2013
%R 10.3969/j.issn.1006？7043.201210015
%X 针对SPS（specificationpatternsystem）和Prospec（propertyspecification）不能将组合命题形式化为模型检测器可以接受的CTL（computationtreelogic）公式问题，通过研究SPS和Prospec产生系统性质描述的形式化方法，并对比CTL与FIL（futureintervallogic）的表达能力以及CTL与LTL（lineartemporallogic）两者之间的关系，构造了一类具有较强描述能力的CTL公式模板，并通过重新定义合取逻辑运算符来简化公式.该类模板简洁且易于理解.模板类的正确性证明表示该类模板可以有效地描述系统性质.利用该模板得到的CTL公式可以直接应用到模型检测器中，利于系统性质验证.
%K 模型检测
%K 形式化描述
%K SPS
%K Prospec
%K CTL模板
%U http://heuxb.hrbeu.edu.cn/oa/darticle.aspx?type=view&id=201210015