Consiglio Nazionale delle Ricerche

Tipo di prodottoArticolo in rivista
TitoloBounded satisfiability checking of metric temporal logic specifications
Anno di pubblicazione2013
Autore/iPradella M.; Morzenti A.; San Pietro P.
Affiliazioni autoriDEIB, Politecnico di Milano, Italy
Autori CNR e affiliazioni
  • inglese
AbstractWe 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. © 2013 ACM.
Lingua abstractinglese
Altro abstract-
Lingua altro abstract-
Pagine da-
Pagine a-
Pagine totali-
RivistaACM transactions on software engineering and methodology
Attiva dal 1992
Editore: Association for Computing Machinery, - New York, NY
Paese di pubblicazione: Stati Uniti d'America
Lingua: inglese
ISSN: 1049-331X
Titolo chiave: ACM transactions on software engineering and methodology
Titolo proprio: ACM transactions on software engineering and methodology.
Titolo abbreviato: ACM trans. softw. eng. methodol.
Titoli alternativi:
  • Transactions on software engineering and methodology
  • Association for Computing Machinery transactions on software engineering and methodology
Numero volume della rivista22
Fascicolo della rivista3
Verificato da refereeSì: Internazionale
Stato della pubblicazionePublished version
Indicizzazione (in banche dati controllate)
  • Scopus (Codice:2-s2.0-84894515204)
Parole chiaveBi-infinite time, Bounded model checking, Formal methods, Refinement, Temporal logic
Link (URL, URI)
Titolo parallelo-
Data di accettazione-
Note/Altre informazioni-
Strutture CNR
  • IEIIT — IEIIT - Sede secondaria di Milano
Moduli/Attività/Sottoprogetti CNR-
Progetti Europei-
Bounded Satisfiability Checking of Metric Temporal Logic Specifications (documento privato )
Tipo documento: application/pdf