We present a sound and fully automated method for the verification of safety properties of parameterized systems with unbounded local data variables, a new class of infinite-state systems parametric in several dimensions. The method builds upon a specification and an assertional language based on the combination of multiset rewriting and constraints. We introduce new classes of parameterized systems for which verification of safety properties is decidable, and we introduce abstractions, defined at the level of constraints, to handle examples outside these classes. As case-study, we apply the method to verify fully automatically mutual exclusion properties for formulations of the ticket mutual exclusion algorithm parametric in the number of clients, servers, and in which both clients and servers have unbounded local data.

Beyond parameterized verification

Bozzano, Marco;Delzanno, Giorgio
2002

Abstract

We present a sound and fully automated method for the verification of safety properties of parameterized systems with unbounded local data variables, a new class of infinite-state systems parametric in several dimensions. The method builds upon a specification and an assertional language based on the combination of multiset rewriting and constraints. We introduce new classes of parameterized systems for which verification of safety properties is decidable, and we introduce abstractions, defined at the level of constraints, to handle examples outside these classes. As case-study, we apply the method to verify fully automatically mutual exclusion properties for formulations of the ticket mutual exclusion algorithm parametric in the number of clients, servers, and in which both clients and servers have unbounded local data.
978-3-540-43419-1
File in questo prodotto:
File Dimensione Formato  
tacas02.pdf

solo utenti autorizzati

Tipologia: Documento in Pre-print
Licenza: NON PUBBLICO - Accesso privato/ristretto
Dimensione 232.09 kB
Formato Adobe PDF
232.09 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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: http://hdl.handle.net/11582/309023
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact