Parametric model checking for concurrent periodic EFSMs and an efficient simplification method of parameter conditions

摘要

In this paper, we develop a parametric model checking method for concurrent periodic EFSMs and a property described in a real-time extension of CTL (RPCTL). The periodic EFSM is a kind of a real-time extension of the EFSM model that after some constant period T ahs elapsed, it returns to its initial state. In the proposed method, the concurrent periodic EFSMs are translated into a single periodic EFSM on-the-fly, and the parameter condition is derived. The parameter condition WPC(s, f), in order that the state s satisfies the property f, is derived by recursively computing the subconditions WPC(s{sub}i, f{sub}i) for its next states s{sub}i and their derived properties f{sub}i. We also introduce some optimization heuristics, such as the quantifier elimination of the derived formula.