Author: Gavin Lowe
Paper Information
Title: | View abstraction for systems with component identities |
Authors: | Gavin Lowe |
Proceedings: | FM FMComplete |
Editors: | Jan Peleska, Klaus Havelund and Bill Roscoe |
Keywords: | Model checking, Parameterised verification problem, View abstraction, Symmetry reduction, Concurrent datatypes |
Abstract: | ABSTRACT. The parameterised verification problem seeks to verify all members of some family of systems. We consider the following instance: each system is composed of an arbitrary number of similar component processes, together with a fixed number of server processes; processes communicate via message passing; in particular, each component process has an identity, which may be included in messages, and passed to third parties. We extend the technique of view abstraction of Abdulla et al. to this setting. We give an algorithm and implementation that allows such systems to be verified for an arbitrary number of components. We show how this technique can be applied to a concurrent datatype built from reference-linked nodes, such as a linked list. |
Pages: | 17 |
Talk: | Jul 17 12:00 (Session 120) |
Paper: |