The Design And Implementation Of MvChecker, A Model Checker Based On Multi-value Possibilities

Modern computer technology has always been accompanied by our lives.With the increasing complexity of modern computer software and hardware,the testing of hardware and software has become more and more complex.It not only consumes a lot of manpower and material costs to ensure safety of the system,but also the traditionally detection technology has certain limitations when dealing with the some uncertain conditions,which leads to failure of detection.In 1981,Clarke and Emerson and Quielle and Sifakis proposed model checking theory as a formalized automatic verification technique,which provided a solution for us to solve these detection problems.Compared with the traditional detection technology,the model checking has a series of advantages over detection technology.For example,the system can be verified before the system is implemented,as the problem can be discovered in advance and a large amount of cost can be saved.These tests generally use model checker to verify the properties based on the model checking theory.Most of the traditional model checker are designed based on classical model checking theory.With in-depth research,we have found that there are a lot of uncertain information in real life,that the traditional model checker can not be used.The discovery of multi-valued model checking theory,using lattice theory to deal with uncertainty information,combined with multi-valued computation tree logic,constructing a multi-valued Kripke structure model,effectively solves these problems.In order to achieve the advantage of automatic detection of the characteristics of the model checking.This paper designs the storage structure of multi-value Kripke structure in the computer,the calculation module and so on,implements a multi-value model checker MvChecker based on mutil-valu-ed computation tree logic model checking based on mutil-valued possibility measures,makes the users can automatically verify the properties.The work of this article is as follows:(1)We give the method that change the multi-valued Kripke structure def-ined in the theory to the computer data structure which satify the storage of c-omputer,and the time complexity is analyzed.The state and transfer function are stored with the best data structure as far as possible,so that the model checker can read more data from the storage and calculate more data,which effectively alleviate the problem of state explosion under a certain amount of data.(2)According to the flow chart of the model checking theory,we analyzed the structure of the model checker,and the framework of the model detector is designed.How to deal with the model and properties of the user input,how to convert the model and properties to the computer storage,how to calculate the data after the conversion data,and how to verify the properties of the user input,and how to output the result.We analyze the output of the result and the time complexity.In the end we test the perfomance of model checker which we designed.