| 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 |
|
