Reformulation: A Way to Combine Dynamic Properties and B Refinement

摘要

We are interested in verifying dynamic properties of reactive systems. The reactive systems are specified by B event systems in a refinement development. The refinement allows us to combine proof and model-checking verification techniques in a novel way. Most of the PLTL dynamic properties are preserved by refinement, but in our approach, the user can also express how a property evolves during the refinement. The preservation of the abstract property, expressed by a PLTL formula F_1, is used as an assumption for proving a PLTL formula F_2 which expresses an enriched property in the refined system. Formula F_1 is verified by model-checking on the abstract system. So, to verify the enriched formula F_2, it is enough to prove some propositions depending on the respective patterns followed by F_1 and F_2. In this paper, we show how to obtain these sufficient propositions from the refinement relation and the semantics of the PLTL formulae. The main advantage is that the user does not need to express a variant or 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.