Reformulate Dynamic Properties during B Refinement and Forget Variants and Loop Invariants

摘要

We propose a way to introduce dynamic properties into a B refinement design which differs from the approach used by J.R. Abrial and L. Mussat. First, the properties are expressed in the Propositional Linear Temporal Logic PLTL. Second, the user directs the evolution of properties through the refinement, so that a property P expressed by a formula F{sub}1 in the abstract system, is expressed again by a formula F{sub}2 in the refined system. Third, the verification combines proof and model-checking. In particular, F{sub}1 is model-checked, and, then, to ensure F{sub}2 it suffices to prove some propositions depending on the shapes of F{sub}1 and F{sub}2. In this paper, we show how to obtain these "sufficient propositions" from a refinement relation and the semantics of PLTL formulae. The main advantage is that the user does not need a variant or a loop invariant to achieve an automatic proof for finite state event systems. Our approach is illustrated on a protocol between a chip card and a card reader, called protocol T=1.