Model Checking Of Component-based Systems

Component systems are widely used in many areas of industry, the correctness of these systems is important. There exist many model checking methods to analyze the behaviors and stochastic behavior of the systems. These methods are very memory and time consuming due to the sophisticated behaviors. Verifying these system with abstraction may lead to the inconclusive result. To solve these problems, we proposed various techniques for model checking of component systems. The main contributions of this dissertation are as follows:? Based on the transition partition method, a method of variables partition is proposed. This method can partition the variables of transitions into separate valuechanged and value-unchanged variable sets. Then we utilize this information to get memory reduced and runtime improvement during the symbolic model checking of component-based systems.? The effciency of the compositional verification of component-based systems depends on the abstraction, which may lead to verification incompleteness. To solve this problem, the invariant strengthening and state partitioning techniques are proposed in this dissertation. Integrated with these two refinement techniques, a unified compositional verification framework is presented to strengthen the abstraction and find counterexamples.? For analyzing the behavior of the stochastic component system(SBIP) whose semantic models are Discrete time Markov chains(DTMCs), we develop a way of translation, from SBIP models to PRISM DTMC models. We propose a method to generate an approximation model of SBIP model and then do the probabilistic model checking on the approximation models.? For analyzing the expected behaviors of stochastic component system, we use i LTL and ip LTL model checking methods to check the properties of probability mass functions(pmfs) of Markov chains. If the interested property does not hold, these algorithms will provide a counterexample, the initial pmf, for the reveals the violation.