多值可能性模型检测器的设计与实现
|
摘要
随着现代计算机软件和硬件的复杂性变大,模型检测作为一种形式化自动验证技术,与传统的检测技术相比有着一系列的优势,比如可以在系统实现之前对系统进行验证,可以提前发现问题,节约大量成本。传统的模型检测器大多是基于经典的模型检测技术实现的,而现实生活中存在大量的不确定信息,使用传统的模型检测无法解决这些问题。而多值模型检测理论的出现,结合多值计算树逻辑,构建多值可能性Kripke结构模型,可以很好地解决这些问题。为了实现模型检测自动化特性的最大优势,基于多值可能性定量模型检测的理论,设计了多值Kripke结构在计算机中的存储结构、计算模块等,实现了一个基于多值可能性测度的多值计算树逻辑的模型检测器MvChecker,使得用户可以自动验证系统性质。
With the increasing complexity of modern computer software and hardware,model detection,as a formalized automatic verification technology,has a series of advantages over traditional detection technology. For example,it can verify the system before the system implementation,detect problems in advance,and save a lot of costs. The traditional model checker is mostly based on the classic theory of model checking,but in real life there are a lot of uncertain information,so it cannot solve these problems. For this,we use multi-valued model theory,combined with multi-value computation tree logic to construct multi-value possibilistic Kripke model that can be an effective solution to these problems. In order to achieve the advantage of automatic characteristics of the model checking,based on the theory of multi-valued possibility quantitative model checking,we design the storage structure and calculation module of multi-value Kripke structure in computer,and implements a model detector MvChecker based on multi-valued possibility measure of multi-valued calculation tree logic,so that users can automatically verify the system property
With the increasing complexity of modern computer software and hardware,model detection,as a formalized automatic verification technology,has a series of advantages over traditional detection technology. For example,it can verify the system before the system implementation,detect problems in advance,and save a lot of costs. The traditional model checker is mostly based on the classic theory of model checking,but in real life there are a lot of uncertain information,so it cannot solve these problems. For this,we use multi-valued model theory,combined with multi-value computation tree logic to construct multi-value possibilistic Kripke model that can be an effective solution to these problems. In order to achieve the advantage of automatic characteristics of the model checking,based on the theory of multi-valued possibility quantitative model checking,we design the storage structure and calculation module of multi-value Kripke structure in computer,and implements a model detector MvChecker based on multi-valued possibility measure of multi-valued calculation tree logic,so that users can automatically verify the system property
引文
[1] BAIER C,KATOEN J P.Principles of model checking[M].Cambridge:MIT Press,2008.
[2] BIRKHOFF G.Lattice theory[M].3rd ed.[s.l.]:[s.n.],1973.
[3] LI Yongming.Quantitative model checking of linear-time properties based on generalized possibility measures[J].Fuzzy Sets and Systems,2015,320:17-39.
[4] HOLZMANNN G J.The SPIN model checker:prinmer and reference manual[M].Reading:Addison-Wesley,2004.
[5] CIMATTI A,CLARKE E,GIUNCHIGLIA F,et al.Nu-SMV:a new symbolic model checker[J].International Journal on Software Tools for Technology Transfer,2000,2(4):410-425.
[6] LI Yongming,MA Zhanyou.Quantitative computation tree logic model checking based on generalized possibility measures[J].IEEE Transactions on Fuzzy Systems,2015,23(6):2034-2047.
[7] 陈云霁,马麟,沈海华,等.龙芯2号微处理器浮点除法功能部件的形式验证[J].计算机研究与发展,2006,43(10):1835-1841.
[8] 张良,易江芳,佟冬,等.使用局部建模的微处理器测试程序自动生成方法[J].电子学报,2011,39(7):1639-1644.
[9] 马占有,李永明.基于决策过程的广义可能性计算树逻辑模型检测[J].中国科学:信息科学,2016,46(11):1591-1607.
[10] 邓楠轶.基于广义可能性测度的模型检测器GPoCheck的设计与实现[D].西安:陕西师范大学,2015.
[11] 范艳焕,李永明,潘海玉.不确定型模糊Kripke结构的计算树逻辑模型检测[J].电子学报,2018,46(1):152-159.
[12] LI Yongming,LI Yali,MA Zhanyou.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,262:44-59.
[13] 周从华,邢支虎,刘志锋,等.马尔可夫决策过程的限界模型检测[J].计算机学报,2013,36(12):2587-2600.
[14] 林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,36(12A):1907-1912.
[15] 刘阳,李宣东,马艳,等.随机模型检测研究[J].计算机学报,2015,38(11):2145-2162.
[16] 周从华,刘志锋,王昌达.概率计算树逻辑的限界模型检测[J].软件学报,2012,23(7):1656-1668.
[17] 李永明,李平.模糊计算理论[M].北京:科学出版社,2016.
[18] 严蔚敏,吴伟民.数据结构[M].北京:清华大学出版社,2012.
[2] BIRKHOFF G.Lattice theory[M].3rd ed.[s.l.]:[s.n.],1973.
[3] LI Yongming.Quantitative model checking of linear-time properties based on generalized possibility measures[J].Fuzzy Sets and Systems,2015,320:17-39.
[4] HOLZMANNN G J.The SPIN model checker:prinmer and reference manual[M].Reading:Addison-Wesley,2004.
[5] CIMATTI A,CLARKE E,GIUNCHIGLIA F,et al.Nu-SMV:a new symbolic model checker[J].International Journal on Software Tools for Technology Transfer,2000,2(4):410-425.
[6] LI Yongming,MA Zhanyou.Quantitative computation tree logic model checking based on generalized possibility measures[J].IEEE Transactions on Fuzzy Systems,2015,23(6):2034-2047.
[7] 陈云霁,马麟,沈海华,等.龙芯2号微处理器浮点除法功能部件的形式验证[J].计算机研究与发展,2006,43(10):1835-1841.
[8] 张良,易江芳,佟冬,等.使用局部建模的微处理器测试程序自动生成方法[J].电子学报,2011,39(7):1639-1644.
[9] 马占有,李永明.基于决策过程的广义可能性计算树逻辑模型检测[J].中国科学:信息科学,2016,46(11):1591-1607.
[10] 邓楠轶.基于广义可能性测度的模型检测器GPoCheck的设计与实现[D].西安:陕西师范大学,2015.
[11] 范艳焕,李永明,潘海玉.不确定型模糊Kripke结构的计算树逻辑模型检测[J].电子学报,2018,46(1):152-159.
[12] LI Yongming,LI Yali,MA Zhanyou.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,262:44-59.
[13] 周从华,邢支虎,刘志锋,等.马尔可夫决策过程的限界模型检测[J].计算机学报,2013,36(12):2587-2600.
[14] 林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,36(12A):1907-1912.
[15] 刘阳,李宣东,马艳,等.随机模型检测研究[J].计算机学报,2015,38(11):2145-2162.
[16] 周从华,刘志锋,王昌达.概率计算树逻辑的限界模型检测[J].软件学报,2012,23(7):1656-1668.
[17] 李永明,李平.模糊计算理论[M].北京:科学出版社,2016.
[18] 严蔚敏,吴伟民.数据结构[M].北京:清华大学出版社,2012.