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), pp. 249-258. (Intervento presentato al convegno SEFM 2008 tenutosi a Cape Town nel 10/11/2008 - 14/11/2008) [10.1109/SEFM.2008.23].

Object Models with Temporal Constraints

Alessandro Cimatti;Marco Roveri;Angelo Susi;Stefano Tonetta
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
Proceedings 6th Int. Conference on Software Engineering and Formal Methods
Cape Town, South Africa
IEEE Computer Society
9780769534374
Cimatti, Alessandro; Roveri, Marco; Susi, Angelo; Tonetta, Stefano
Object Models with Temporal Constraints / Cimatti, Alessandro; Roveri, Marco; Susi, Angelo; Tonetta, Stefano. - (2008), pp. 249-258. (Intervento presentato al convegno SEFM 2008 tenutosi a Cape Town nel 10/11/2008 - 14/11/2008) [10.1109/SEFM.2008.23].
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/11572/258758
 Attenzione

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

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 5
social impact