Refinement Preserves PLTL Properties

摘要

We are interested in verifying dynamic properties of reactive systems. The reactive systems are specified by B event systems in a refinement development. We use labelled transition systems to express the semantics of these event systems on which we define a refinement relation. The main advantage is that the user does not need to express a variant and a loop invariant to obtain automatic proofs of dynamic properties, at least for finite state event systems. Another advantage is that the model-checking is done on an abstraction with few states and the property is preserved in the following refinements of the system. The originality of this work concerns the proof that this refinement relation preserves the properties expressed with propositional linear temporal logic.