可能性测度下的CTL符号化模型检测
|
摘要
随着系统复杂性的增加,系统中的不确定信息亟待处理,状态爆炸问题也越来越严峻,现有的模型检测技术已不能完全适用于复杂系统的验证。对可能性测度下CTL符号化模型检测进行了研究。首先用多终端二值决策图和布尔公式分别描述系统模型和待验证性质,然后再对系统模型进行归一化和简化,最后利用不动点计算完成系统验证。该研究是对可能性测度下的模型检测技术和符号化模型检测技术的整合,不但能处理系统的不确定信息,而且保持了符号化模型检测对计算时空要求低的优点,对于复杂系统模型检测具有重要意义。
With the increasing complexity of systems,it is urgent to deal with the uncertain information in the systems.Besides,the state explosion problem is getting more and more serious.Existing model checking techniques are no longer suitable for the verification of such complex systems.We study symbolic CTL model checking based on possibility measure.Firstly,multi-terminal binary decision trees(MTBDDs)and Boolean formula are respectively used to describe system models and properties to be verified.Secondly,the system models are normalized and simplified.Finally,system verification is completed by fixed point calculation.Our work is an integration of symbolic model checking and CTL model checking based on possibility measure,which can not only handle uncertain information in systems,but also maintain symbolic model checking's advantage of low demand for computation time and storage space.It is thus significant for the verification of complex systems.
With the increasing complexity of systems,it is urgent to deal with the uncertain information in the systems.Besides,the state explosion problem is getting more and more serious.Existing model checking techniques are no longer suitable for the verification of such complex systems.We study symbolic CTL model checking based on possibility measure.Firstly,multi-terminal binary decision trees(MTBDDs)and Boolean formula are respectively used to describe system models and properties to be verified.Secondly,the system models are normalized and simplified.Finally,system verification is completed by fixed point calculation.Our work is an integration of symbolic model checking and CTL model checking based on possibility measure,which can not only handle uncertain information in systems,but also maintain symbolic model checking's advantage of low demand for computation time and storage space.It is thus significant for the verification of complex systems.
引文
[1]Wang Fei-ming,Hu Yuan-chang,Dong Rong-sheng.Research progress on model checking[J].Journal of Guangxi Academy of Sciences,2008,24(4):320-324.(in Chinese)
[2]Guo Chen-kai,Xu Jing,Si Guan-nan,et al.Model checking for software information leakage in mobile application[J].Chinese Journal of Computers,2016,39(11):2324-2343.(in Chinese)
[3]Zhu Wei-jun,Zhou Qing-lei,Zhang Qin-xian.A LTL model checking approach based on DNA computing[J].Chinese Journal of Computers,2016,39(12):2578-2597.(in Chinese)
[4]Fisher J,Piterman N.Model checking in biology[M].Netherlands:Springer,2014.
[5]Clarke E,Gupta A,Jain H,et al.Model checking:Back and forth between hardware and software[M].Berlin:Springer Berlin Heidelberg,2008.
[6]Hart S,Sharir M.Probabilistic propositional temporal logics*[J].Information&Control,1986,70(2):97-155.
[7]PRISM[EB/OL].[2010-05-18].http://www.prismmodelchecker.org.
[8]Baier C,Katoen J P.Principles of model checking[M].Cambridge:MIT Press,2007.
[9]Li Li-jun.LTL model checking based on possibility measure[D].Xi'an:Shaanxi Normal University,2012.(in Chinese)
[10]Xue Yan,Lei Hong-xuan,Li Yong-ming.Computation tree logic based on possibility measure[J].Computer Engineering&Science,2011,33(9):70-75.(in Chinese)
[11]Ma Zhan-you,Li Yong-ming.Model checking of accessibility problem based on generalized possibility measure[J].Fuzzy Systems and Mathematics,2014,28(6):88-97.(in Chinese)
[12]Ma Zhan-you,Li Yong-ming.Computation tree logic model checking for generalized possibilistic decision processes[J].Computer Engineering&Science,2015,37(11):2162-2168.(in Chinese)
[13]Deng Hui.Computation tree logic CTL based on possibility measure and possibilistic bisimulation[D].Xi'an:Shaanxi Normal University,2013.(in Chinese)
[14]Ji Ming-yu,Wang Hai-tao,Chen Zhi-yuan,et al.Symmetry reduction method for complicated system model based on decision diagrams[J].Computer Engineering and Design,2013,34(10):3685-3689.(in Chinese)
[15]Li Yong-ming,Li Ya-li,Ma Zhan-you.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,262:44-59.
[16]Li Y,Li L.Model checking of linear-time properties based on possibility measure[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
[17]Clarke E,Fujita M,Zhao X.Applications of multi-terminal binary decision diagrams[C]∥Proc of IFIP WG 10.5Workshop on Applications of the Reed-Muller Expansion in Circuit Design,1995:21-27.
[18]LüYi.Research on formal verification method of sequential logic circuit[D].Beijing:Institute of Computing Technology,Chinese Academy of Sciences,2000.(in Chinese)
[19]Zhang Yan-zhi.Research on symbolic model-checking algorithms[D].Jilin:Jilin University,2009.(in Chinese)
[20]Wei Xiao-yong.Research of symbol model checking[D].Xi'an:Xi'an University of Technology,2008.(in Chinese)
[21]Duan Zhen-hua,Feng Tao,Tian Cong,et al.PPTL symbol model detection method:CN102663190 A[P].2012.(in Chinese)
[1]王飞明,胡元闯,董荣胜.模型检测研究进展[J].广西科学院学报,2008,24(4):320-324.
[2]过辰楷,许静,司冠南,等.面向移动应用软件信息泄露的模型检测研究[J].计算机学报,2016,39(11):2324-2343.
[3]朱维军,周清雷,张钦宪.基于DNA计算的线性时序逻辑模型检测方法[J].计算机学报,2016,39(12):2578-2597.
[9]李丽君.基于可能性测度的LTL模型检测[D].西安:陕西师范大学,2012.
[10]薛艳,雷红轩,李永明.基于可能性测度的计算树逻辑[J].计算机工程与科学,2011,33(9):70-75.
[11]马占有,李永明.基于广义可能性测度的可达性问题的模型检测[J].模糊系统与数学,2014,28(6):88-97.
[12]马占有,李永明.广义可能性决策过程的计算树逻辑模型检测[J].计算机工程与科学,2015,37(11):2162-2168.
[13]邓辉.基于可能性测度的计算树逻辑与可能性互模拟[D].西安:陕西师范大学,2013.
[14]纪明宇,王海涛,陈志远,等.基于决策图的复杂系统模型对称约减方法[J].计算机工程与设计,2013,34(10):3685-3689.
[18]吕毅.时序逻辑电路的形式验证方法研究[D].北京:中国科学院计算技术研究所,2000.
[19]张衍志.符号化模型检测算法的研究[D].吉林:吉林大学,2009.
[20]魏小勇.符号模型检测的研究[D].西安:西安理工大学,2008.
[21]段振华,逄涛,田聪,等.PPTL符号模型检测方法:中国,CN102663190A[P].2012.
[2]Guo Chen-kai,Xu Jing,Si Guan-nan,et al.Model checking for software information leakage in mobile application[J].Chinese Journal of Computers,2016,39(11):2324-2343.(in Chinese)
[3]Zhu Wei-jun,Zhou Qing-lei,Zhang Qin-xian.A LTL model checking approach based on DNA computing[J].Chinese Journal of Computers,2016,39(12):2578-2597.(in Chinese)
[4]Fisher J,Piterman N.Model checking in biology[M].Netherlands:Springer,2014.
[5]Clarke E,Gupta A,Jain H,et al.Model checking:Back and forth between hardware and software[M].Berlin:Springer Berlin Heidelberg,2008.
[6]Hart S,Sharir M.Probabilistic propositional temporal logics*[J].Information&Control,1986,70(2):97-155.
[7]PRISM[EB/OL].[2010-05-18].http://www.prismmodelchecker.org.
[8]Baier C,Katoen J P.Principles of model checking[M].Cambridge:MIT Press,2007.
[9]Li Li-jun.LTL model checking based on possibility measure[D].Xi'an:Shaanxi Normal University,2012.(in Chinese)
[10]Xue Yan,Lei Hong-xuan,Li Yong-ming.Computation tree logic based on possibility measure[J].Computer Engineering&Science,2011,33(9):70-75.(in Chinese)
[11]Ma Zhan-you,Li Yong-ming.Model checking of accessibility problem based on generalized possibility measure[J].Fuzzy Systems and Mathematics,2014,28(6):88-97.(in Chinese)
[12]Ma Zhan-you,Li Yong-ming.Computation tree logic model checking for generalized possibilistic decision processes[J].Computer Engineering&Science,2015,37(11):2162-2168.(in Chinese)
[13]Deng Hui.Computation tree logic CTL based on possibility measure and possibilistic bisimulation[D].Xi'an:Shaanxi Normal University,2013.(in Chinese)
[14]Ji Ming-yu,Wang Hai-tao,Chen Zhi-yuan,et al.Symmetry reduction method for complicated system model based on decision diagrams[J].Computer Engineering and Design,2013,34(10):3685-3689.(in Chinese)
[15]Li Yong-ming,Li Ya-li,Ma Zhan-you.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,262:44-59.
[16]Li Y,Li L.Model checking of linear-time properties based on possibility measure[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.
[17]Clarke E,Fujita M,Zhao X.Applications of multi-terminal binary decision diagrams[C]∥Proc of IFIP WG 10.5Workshop on Applications of the Reed-Muller Expansion in Circuit Design,1995:21-27.
[18]LüYi.Research on formal verification method of sequential logic circuit[D].Beijing:Institute of Computing Technology,Chinese Academy of Sciences,2000.(in Chinese)
[19]Zhang Yan-zhi.Research on symbolic model-checking algorithms[D].Jilin:Jilin University,2009.(in Chinese)
[20]Wei Xiao-yong.Research of symbol model checking[D].Xi'an:Xi'an University of Technology,2008.(in Chinese)
[21]Duan Zhen-hua,Feng Tao,Tian Cong,et al.PPTL symbol model detection method:CN102663190 A[P].2012.(in Chinese)
[1]王飞明,胡元闯,董荣胜.模型检测研究进展[J].广西科学院学报,2008,24(4):320-324.
[2]过辰楷,许静,司冠南,等.面向移动应用软件信息泄露的模型检测研究[J].计算机学报,2016,39(11):2324-2343.
[3]朱维军,周清雷,张钦宪.基于DNA计算的线性时序逻辑模型检测方法[J].计算机学报,2016,39(12):2578-2597.
[9]李丽君.基于可能性测度的LTL模型检测[D].西安:陕西师范大学,2012.
[10]薛艳,雷红轩,李永明.基于可能性测度的计算树逻辑[J].计算机工程与科学,2011,33(9):70-75.
[11]马占有,李永明.基于广义可能性测度的可达性问题的模型检测[J].模糊系统与数学,2014,28(6):88-97.
[12]马占有,李永明.广义可能性决策过程的计算树逻辑模型检测[J].计算机工程与科学,2015,37(11):2162-2168.
[13]邓辉.基于可能性测度的计算树逻辑与可能性互模拟[D].西安:陕西师范大学,2013.
[14]纪明宇,王海涛,陈志远,等.基于决策图的复杂系统模型对称约减方法[J].计算机工程与设计,2013,34(10):3685-3689.
[18]吕毅.时序逻辑电路的形式验证方法研究[D].北京:中国科学院计算技术研究所,2000.
[19]张衍志.符号化模型检测算法的研究[D].吉林:吉林大学,2009.
[20]魏小勇.符号模型检测的研究[D].西安:西安理工大学,2008.
[21]段振华,逄涛,田聪,等.PPTL符号模型检测方法:中国,CN102663190A[P].2012.