N的LTL属性分解方法研究.pdfVIP

第３１卷第７期　　　 计算机应用与软件 Ｖｏｌ３１Ｎｏ．７ ２０１４年７月　　 ＣｏｍｐｕｔｅｒＡｐｐｌｉｃａｔｉｏｎｓａｎｄＳｏｆｔｗａｒｅ Ｊｕｌ．２０１４ 基于ＳＰＩＮ的ＬＴＬ属性分解方法研究 贺志宏　曾庆凯 （南京大学计算机软件新技术国家重点实验室　江苏南京２１００４６） （南京大学计算机科学与技术系　江苏南京２１００４６） 摘　要　　提出一种基于模型检测工具ＳＰＩＮ的ＬＴＬ属性分解方法以解决状态空间爆炸问题。根据逻辑和时序操作符常见的组合 情况，讨论不同的属性分解模式，根据子属性构建的切片准则进行程序切片，利用ＳＰＩＮ对切片后的等价简化模型进行检测，从而将 对原模型上属性的检测转化成对复杂度较低的子模型上各子属性的分别检测。实验结果表明，该方法具有一定的有效性。 关键词　　线性时序逻辑属性　模型检测　属性分解　静态程序切片 中图分类号　ＴＰ３０９　　　　文献标识码　Ａ　　　　ＤＯＩ：１０．３９６９／ｊ．ｉｓｓｎ．１０００３８６ｘ．２０１４．０７．０１２ ＳＴＵＤＹＯＮＳＰＩＮＢＡＳＥＤＬＴＬＰＲＯＰＥＲＴＹＤＥＣＯＭＰＯＳＩＴＩＯＮ ＨｅＺｈｉｈｏｎｇ　ＺｅｎｇＱｉｎｇｋａｉ （ＳｔａｔｅＫｅｙＬａｂｏｒａｔｏｒｙｏｆＮｏｖｅｌＳｏｆｔｗａｒｅＴｅｃｈｎｏｌｏｇｙ，ＮａｎｊｉｎｇＵｎｉｖｅｒｓｉｔｙ，Ｎａｎｊｉｎｇ２１００４６，Ｊｉａｎｇｓｕ，Ｃｈｉｎａ） （ＤｅｐａｒｔｍｅｎｔｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅａｎｄＴｅｃｈｎｏｌｏｇｙ，ＮａｎｊｉｎｇＵｎｉｖｅｒｓｉｔｙ，Ｎａｎｊｉｎｇ２１００４６，Ｊｉａｎｇｓｕ，Ｃｈｉｎａ） Ａｂｓｔｒａｃｔ　　Ｔｏｓｏｌｖｅｔｈｅｓｔａｔｅｓｐａｃｅｅｘｐｌｏｓｉｏｎｐｒｏｂｌｅｍ，ｗｅｐｒｏｐｏｓｅａｌｉｎｅａｒｔｅｍｐｏｒａｌｌｏｇｉｃ（ＬＴＬ）ｐｒｏｐｅｒｔｙｄｅｃｏｍｐｏｓｉｔｉｏｎｍｅｔｈｏｄｗｈｉｃｈｉｓ ｂａｓｅｄｏｎｍｏｄｅｌｃｈｅｃｋｔｏｏｌＳＰＩＮ．Ａｃｃｏｒｄｉｎｇｔｏｔｈｅｃｏｍｍｏｎｃｏｍｂｉｎａｔｉｏｎｓｏｆｌｏｇｉｃａｎｄｔｅｍｐｏｒａｌｏｐｅｒａｔｏｒｓ，ｗｅｄｉｓｃｕｓｓｄｉｆｆｅｒｅｎｔｐｒｏｐｅｒｔｙ ｄｅｃｏｍｐｏｓｉｔｉｏｎｐａｔｔｅｒｎｓ，ｓｌｉｃｅｔｈｅｐｒｏｇｒａｍｓａｃｃｏｒｄｉｎｇｔｏｔｈｅｓｌｉｃｉｎｇｃｒｉｔｅｒｉａｃｏｎｓｔｒｕｃｔｅｄｂｙｓｕｂｐｒｏｐｅｒｔｙ，ａｎｄｔｈｅｎｅｍｐｌｏｙＳＰＩＮｔｏｃｈｅｃｋｔｈｅ ｓｌｉｃｅｄｅｑｕｉｖａｌｅｎｔｓｉｍｐｌｉｆｉｅｄｍｏｄｅｌｓ，ｓｏｔｈａｔｃｏｎｖｅｒｔｔｈｅｃｈｅｃｋｏｎｔｈｅｐｒｏｐｅｒｔｙｏｆｔｈｅｏｒｉｇｉｎａｌｍｏｄｅｌｔｏｔｈｅｒｅｓｐｅｃｔｉｖｅｃｈｅｃｋｓｏｎｅａｃｈｓｕｂ ｐｒｏｐｅｒｔｙｏｆｓｕｂｍｏｄｅｌｗｉｔｈｌｏｗｅｒｃｏｍｐｌｅｘｉｔｙ．Ｅｘｐｅｒｉｍｅｎｔａｌｒｅｓｕｌｔｓｓｈｏｗｔｈａｔｔｈｅｍｅｔｈｏｄｉｓｖａｌｉｄｔｏｃｅｒｔａｉｎｅｘｔｅｎｔ． Ｋｅｙｗｏｒｄｓ　　Ｌｉｎｅａｒｔｅｍｐｏｒａｌｌｏｇｉｃ（ＬＴＬ）ｐｒｏｐｅｒｔｙ　Ｍｏｄｅｌｃｈｅｃｋｉｎｇ　Ｐｒｏｐｅｒｔｙｄｅｃｏｍｐｏｓｉｔｉｏｎ　Ｓｔａｔｉｃｐｒｏｇｒａｍｓｌｉｃｉｎｇ 简方法虽然有效，然而也存在以下两个问题：首先已有的文献中 ０　引　言 缺少具体简化系统的方法，经常只是作为一种方法论被提出。 其次在待检测属性较为复杂的情况下，仅抛去与原待检测属性 ［１］ 模型检测 是一种很重要的自动验证技术，被广泛应用于 无关的模块和语句后所得系统模型的复杂度仍然较高，无法有 计算机硬件、通信协议、控制系统