欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
针对 Specification Pattern System（SPS）和 Property Specification（Prospec）不能将组合命题形式化为模型检测器可以接受的 Computation tree logic（CTL）公式问题，通过深入研究 SPS 和 Prospec 产生系统性质描述的形式化方法，并对比 CTL 与 Future interval logic（FIL）的表达能力以及 CTL 与 Linear temporallogic（LTL）两者之间的关系，构造了一类具有较强描述能力的 CTL 公式模板，并通过重新定义合取逻辑运算符来简化公式.该类模板简洁且易于理解.模板类的正确性证明表示该类模板可以有效地描述系统性质.利用该模板得到的 CTL 公式可以直接应用到模型检测器中，利于系统性质验证.
同期刊论文项目
同项目期刊论文
期刊信息
位置：