Formalizing requirements with object models and temporal constraints

Flaws in requirements often have a negative impact on the subsequent development phases. In this paper, we present a novel approach for the formal representation and validation of requirements, which we used in an industrial project. The formalism allows us to represent and reason about object models and their temporal evolution. The key ingredients are class diagrams to represent classes of objects, their relationships and their attributes, fragments of first order logic to constrain the possible configurations of such objects, and temporal logic operators to deal with the dynamic evolution of the configurations. The approach to formal validation allows to check whether the requirements are consistent, if they are compatible with some scenarios, and if they guarantee some implicit properties. The validation procedure is based on satisfiability checking, which is carried out by means of finite instantiation and model checking techniques.