Approximated parameterized verification of infinite-state processes with global conditions |
| |
| Authors: | Parosh Aziz Abdulla Giorgio Delzanno Ahmed Rezine |
| |
| Affiliation: | (1) Division of Computer Systems, Uppsala University, Box 337, 75105 Uppsala, Sweden;(2) Dipartimento di Informatica e Scienze dell’Informazione, Università di Genova, Via Dodecaneso 35, 16146 Genova, Italy;(3) Laboratoire d’Informatique Algorithmique: Fondements et Applications, Université Paris 7, Case 7014, 75205 Paris Cedex 13, France |
| |
| Abstract: | We present a simple and effective approximated backward reachability procedure for parameterized systems with existentially and universally quantified global conditions. The individual processes operate on unbounded local variables ranging over the natural numbers. In addition, processes may communicate via broadcast, rendez-vous and shared variables. The procedure operates on an over-approximation of the transition system induced by the parameterized system. We verify mutual exclusion for complex protocols such as atomic, non-atomic and distributed versions of Lamport’s bakery algorithm. |
| |
| Keywords: | Parameterized systems Unbounded processes Over-approximation |
| 本文献已被 SpringerLink 等数据库收录！ |
|
