CAJ | 학술논문

针对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(specification pattern system)화Prospec(property specification)불능장조합명제형식화위모형검측기가이접수적CTL(computation tree logic)공식문제,통과연구SPS화Prospec산생계통성질묘술적형식화방법,병대비CTL여FIL(future interval logic)적표체능력이급CTL여LTL(linear temporal logic)량자지간적관계,구조료일류구유교강묘술능력적CTL공식모판,병통과중신정의합취라집운산부래간화공식.해류모판간길차역우리해.모판류적정학성증명표시해류모판가이유효지묘술계통성질.이용해모판득도적CTL공식가이직접응용도모형검측기중,리우계통성질험증.