2000 | OriginalPaper | Buchkapitel
Modular Verification for a Class of PLTL Properties
verfasst von : Pierre-Alain Masson, Hassan Mountassir, Jacques Julliand
Erschienen in: Integrated Formal Methods
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 glo- bal 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 mo- dular 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), where p is a proposition and Q is a simple temporal formula, such as ◯q,◊q, 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 Büchi automata. These conditions define a larger class which contains other patterns such as □(p⇒ ◯(qUr)). Finally, we show through the example of an industrial Robot that this method is valid in a practical way.