Design And Implementation Of Model Detector GPoCheck Based On Generalized Probability Measure

With the development of technology, especially computer technology has come into our life. While as the size of software and hardware become bigger and more complex, which leads to the cost of traditional testing become higher. But some mistakes even can not be checked by traditional testing. Model checking, as a kind of formal automatic verification technology, can effectively solve the problems.Model checking is a useful approach to verify system properties. The biggest difference between model checking and traditional testing is the time when to check. Model checking do it before the system implement, while traditional testing do it after the system implement. According to Myers’s testing theory, model checking can find the problems before system implement,which can save cost. Model checking can already verify many problems effectively in our work and life through about thirty years’study. Such as software, protocol, and so on. As model checking is automatic, we use different kinds of model ckeckers to verify many specific problems, for example, Spin can verify multithreading effectively.The biggest advantage of model checking is automation, which makes easier to solve hand computation. Hence, we designed and implemented a simple model checker based on generalized possibility measures. The process of model checker is first, model the system and desired properties; second, input these into the model checker; at last, the model checker will output the results.The main contributation of this paper is:1. Quantative computation tree logic model checking based on generalized possibility measures has been studied, while its fixed-point semantics has not been researched systematically. Fixed-point semantics of generalized possibilistic compu-tation tree logic is presented, which refined the model checking algorithms and lay the foundation of model checker’s accomplish.2. According to the current computation tree logic model checking based on generalized possibility measures, a model checker GPocheck based on generalized possibility measures has been realized preliminary, which is convenient for users to verify the properties automatically.