Object Models with Temporal Constraints

Flaws in requirements often have a negative impact on the subsequent development phases. In this paper, we propose a novel formalism for the formal representation and validation of requirements. The formalism allows us to represent and reason about object models and their temporal evolution. The key ingredients are class diagrams to represent the objects in the scenarios, fragments of first order logic to deal with the relationships between their attributes and with rich data, and elements of temporal logic operators to deal with the dynamic evolution of the scenario.Formal validation is carried out by means of satisfiability checking, for which we propose a novel procedure based on the reduction to checking the language non-emptiness of a fair transition system.