Tipo di prodotto | Articolo in rivista |
---|---|
Titolo | Bounded satisfiability checking of metric temporal logic specifications |
Anno di pubblicazione | 2013 |
Formato | Cartaceo |
Autore/i | Pradella M.; Morzenti A.; San Pietro P. |
Affiliazioni autori | DEIB, Politecnico di Milano, Italy |
Autori CNR e affiliazioni |
|
Lingua/e |
|
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. © 2013 ACM. |
Lingua abstract | inglese |
Altro abstract | - |
Lingua altro abstract | - |
Pagine da | - |
Pagine a | - |
Pagine totali | - |
Rivista | ACM 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:
|
Numero volume della rivista | 22 |
Fascicolo della rivista | 3 |
DOI | 10.1145/2491509.2491514 |
Verificato da referee | Sì: Internazionale |
Stato della pubblicazione | Published version |
Indicizzazione (in banche dati controllate) |
|
Parole chiave | Bi-infinite time, Bounded model checking, Formal methods, Refinement, Temporal logic |
Link (URL, URI) | http://www.scopus.com/inward/record.url?eid=2-s2.0-84894515204&partnerID=q2rCbXpz |
Titolo parallelo | - |
Data di accettazione | - |
Note/Altre informazioni | - |
Strutture CNR |
|
Moduli CNR | - |
Progetti Europei | - |
Allegati |
|
