Verifying the Precedence Property Pattern Using the B Method

This paper presents an approach to proving a temporal property pattern of the form Prec(P₁, P₂) that expresses that if a state, presented by predicate P₂, is reached then there should exist a state, in the past, that verifies P₁. Such a property pattern is very useful in the specification of various systems such as Information Systems (IS) and security policies. To this aim, we define sufficient and necessary proof obligations that allow to establish such a property.