FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
View abstraction for systems with component identities

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: