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

CTL formalized specification templates in model checking

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

There have been many problems associated with the specification pattern system(SPS) and property specification(PS) such as: the inability to formalize composite propositions into computation tree logic(CTL) formulas.These composite propositions are typically acceptable by model checkers,through intensive studies focused on the formal description of system property generated by SPS and rospec,and by comparing the expression ability between CTL and future interval logic(FIL) as well as the relationship between CTL and linear temporal logic(LTL).This paper proposes an examination of a class of CTL templates along with powerful description ability and redefined conjunction logic operator in order to simplify the templates.This class of template was found to be concise and easy to understand.The results provide overwhelming proof of the correctness of the templates ability to describe system property effectively,and model checkers can also directly use the CTL formulas generated by the template,thus the findings validate the system property.