Parameterized Verification of Infinite-state Processes with Global Conditions
2007 (English)In: Computer Aided Verification, Proceedings / [ed] Damm W, Hermanns H, 2007, 145-157 p.Conference paper (Refereed)
We present a simple and effective approximated backward reachability algorithm 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. We apply the algorithm to verify mutual exclusion for complex protocols such as Lamport's bakery algorithm both with and without atomicity conditions, a distributed version of the bakery algorithm, and Ricart-Agrawala's distributed mutual exclusion algorithm.
Place, publisher, year, edition, pages
2007. 145-157 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 4590
Computer and Information Science
IdentifiersURN: urn:nbn:se:uu:diva-10733ISI: 000248222700014ISBN: 978-3-540-73367-6OAI: oai:DiVA.org:uu-10733DiVA: diva2:38501
19th International Conference on Computer Aided Verification Berlin, GERMANY, JUL 03-07, 2007