On Invariance of Dynamic CTL Model Checking in Iterative Design of Moore Machine-based System

Model checking is a promising approach to verifying safety properties of trusted computing systems in the design phase of system-level. Dynamic model checking is the model checking in which the model changes frequently along the design process. A serious problem for dynamic model checking is that the cost of re-checking is too expensive due to model being changed trivially, so a key issue of the problem is to seek invariance in order to avoid the checking repeatedly. An invariance is a true predicate that will remain true throughout a sequence of model checking. In this paper, a formal framework of dynamic model checking is constructed, and an invariance theory is proposed based on an iterative design process of flow control oriented systems described by Moore machines. It is proved that some non-trivial computation tree logic (CTL) properties can be preserved in the iteration.