We introduce Bounded Satisfiability Checking, a verification technique that extends Bounded Model Checking by allowing also the analysis of a descriptive model, consisting of temporal logic formulae, instead of the more customary operational model, consisting of a state-transition system. We define techniques for encoding temporal logic formulae into Boolean logic that support the use of bi-infinite time domain and of metric time operators. In the framework of Bounded Satisfiability Checking, we show how a descriptive model can be refined into an operational one, and how the correctness of such a refinement can be verified for the bounded case, setting the stage for a stepwise system development method based on a bounded model refinement. Finally, we show how the adoption of a modular approach can make the bounded refinement process more manageable and efficient. All introduced concepts are extensively applied to a set of case studies, and thoroughly experimented through Zot, our SAT solver-based verification toolset.

Bounded Satisfiability Checking of Metric Temporal Logic Specifications

PRADELLA, MATTEO;MORZENTI, ANGELO CARLO;SAN PIETRO, PIERLUIGI
2013-01-01

Abstract

We introduce Bounded Satisfiability Checking, a verification technique that extends Bounded Model Checking by allowing also the analysis of a descriptive model, consisting of temporal logic formulae, instead of the more customary operational model, consisting of a state-transition system. We define techniques for encoding temporal logic formulae into Boolean logic that support the use of bi-infinite time domain and of metric time operators. In the framework of Bounded Satisfiability Checking, we show how a descriptive model can be refined into an operational one, and how the correctness of such a refinement can be verified for the bounded case, setting the stage for a stepwise system development method based on a bounded model refinement. Finally, we show how the adoption of a modular approach can make the bounded refinement process more manageable and efficient. All introduced concepts are extensively applied to a set of case studies, and thoroughly experimented through Zot, our SAT solver-based verification toolset.
Formal methods; temporal logic; bounded model checking; refinement; bi-infinite time
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/11311/666182
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 34
  • ???jsp.display-item.citation.isi??? 22
social impact