PPTL符号模型检测方法专利登记公告

专利名称：PPTL符号模型检测方法

摘要：本发明是一种PPTL符号模型检测方法，属可信计算领域，本发明使用具有完全正则表达能力的规范语言PPTL描述待验证系统期望性质；使用Kripke结构M＝(S，R，L)描述系统模型，借助ROBDD对符号化系统模型M进行搜索，通过构建标记正则图检查期望性质公式是否可满足，节省后续操作时间，提高检测效率。本发明仅需基于时序操作符“○”的检测过程，降低了检测复杂度。本发明提升了模型检测可处理问题的规模，有效缓解状态空间爆炸问题，同时具有描述状态敏感、顺序和闭包性质的能力，可以应用于工业、农业、军事、科研等领域硬件系

专利类型：发明专利

专利号：CN201210102063.9

专利申请（专利权）人：西安电子科技大学

专利发明（设计）人：段振华;逄涛;田聪;王小兵

主权项：一种PPTL符号模型检测方法，其特征在于：使用具有完全正则表达能力的规范语言PPTL描述待验证系统的期望性质；使用Kripke结构M＝(S，R，L)描述待验证系统模型，并将模型M的状态集合S和迁移关系R使用布尔变量进行编码，进而将编码得到的布尔公式使用归约有序二叉决策图表示，借助于归约有序二叉决策图的布尔公式操作机制对被验证系统模型M进行搜索，模型检测步骤包括：步骤1：首先对待验证系统建模，采用Kripke结构描述模型M＝(S，R，L)，并将模型M中的状态集合S和迁移关系R分别编码为形如x1·x2·...

专利地区：陕西