Modular verification for a class of PLTL properties

Abstract

The verification of dynamic properties of a reactive systems by model-checking leads to a potential combinatorial explosion of the state space that has to be checked. In order to deal with this problem, we define a strategy based on local verifications rather than on a global verification. The idea is to split the system into subsystems called modules, and to verify the properties on each module in separation. We prove for a class of PLTL properties that if a property is satisfied on each module, then it is globally satisfied. We call such properties modular properties. We propose a modular decomposition based on the B refinement process. We present in this paper an usual class of dynamic properties in the shape of □ (p => Q)1 where p is a proposition and Q is a simple temporal formula, such as Qqy Qq} or qUr (with q and r being propositions). We prove that these dynamic properties are modular. For these specific patterns, we have exhibited some syntactic conditions of modularity on their corresponding Biichi automata. These conditions define a larger class which contains other patterns such as □ (p => Q(qUr)). Finally, we show through the example of an industrial Robot that this method is valid in a practical way. © Springer-Verlag Berlin Heidelberg 2000.