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_1, P_2) that expresses that if a state, presented by predicate P_2, is reached then there should exist a state, in the past, that verifies P_1. 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.