Research On Some Problems Of Time And Space Performance Analysis Based On Model Checking

Model checking refers to the automatic verification of a system model against a specification that is usually given as a logic formula. It can be used to the functional verification and performance analysis before system implementation, which ensure validity and reliability of the system in the process of operation. As the complexity of the system and the diversity of property specifications, there are many problems to be solved in this research field. Meanwhile, the theory and related technology about model checking is still in development and improvement. In this dissertation, the research works are carried out to resolve some important problems of the stochastic model checking about time and space performance analysis, and summarized as follows:(1) Markov decision process can be used to model complex systems with nondeterminism. Schedulers are required to resolve the nondeterministic choices during model analysis. A formal definition and classification method of schedulers for nondeterminism are proposed in this dissertation and then we prove that the reachability probabilities coincide for deterministic and randomized schedulers under time-abstract. Also, it is proved that time-dependent scheduler may yield a higher time-and space-bounded reachability probability than time-abstract scheduler.(2) In order to express the verification of temporal and spatial properties of the complex systems which include nondeterministic choices, Continuous time markov reward process based on state reward is extended by considered spatial properties with impulse reward and are adopted as verification model. The path formulas expressed by traditional path operator are replaced by regular expressions, which can express more comprehensive verification properties. Under deterministic schedulers, the induced markov reward model of product model which is the product of continuous time markov reward process with impulse reward and path formula is proposed. After that we reduce the problem of model checking for product model to the problem of computing the maximum time and space bound reachability probabilities of induced markov reward model and put forward an algorithm to solve this problem.(3) Based on the strong bisimulation, the notions of weak bisimulation and strong(weak) simulation on continuous time markov decision process are proposed. After then the inherent link between these relations is proved. Meanwhile, the relation between the strong bisimulation equivalence and the asCSL logic equivalence is described and the relation between the weak bisimulation equivalence and the CSL logic equivalence is proved.(4) A stochastic model for cloud computing platform is constructed based on a queueing system. Then the relation between energy consumption and scheduling probability is described. In order to reduce the system energy consumption, a scheduling probability optimization algorithm based on genetic algorithm is put forward. Then the DPM model of computing node is constructed and probabilistic model checking tool PRISM is used to analysis the energy consumption of computing nodes.(5) Hybrid Petri net and fluid stochastic Petri are two modeling methods for hybrid systems. Their modeling mechanism and analysis method are different and the two modeling formalisms are still evolving. Through converting for each other, one modeling method can used the other’s modeling primitives and analytical method for analyzing systems. A formal conversion from hybrid Petri net to fluid stochastic Petri net is put forward and a transition mergence method after conversion is proposed. Also, the effectiveness of the proposed conversion and mergence is proofed. Meanwhile, the model checking of fluid stochastic Petri net under CSL logic is also described.