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.

Object Models with Temporal Constraints

Cimatti, Alessandro;Roveri, Marco;Susi, Angelo;Tonetta, Stefano
2008-01-01

Abstract

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.
2008
9780769534374
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/4608
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact