View abstraction for systems with component identities

Conference item

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 synchronous message passing; in particular, each com- ponent process has an identity, which may be included in messages, and passed to third parties. We extend Abdulla et al.'s technique of view abstraction, together with techniques based on symmetry reduction, 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. Further, we show how to capture the specification of a queue or of a stack.

Authors: Lowe, G

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer Verlag
• Host title: 22nd International Symposium on Formal Methods, 15-17 July 2018, Oxford UK
• Journal: FM 2018
• Volume: 10951
• Pages: 505-522
• Series: Lecture Notes in Computer Science
• Publication date: 2018-07-12
• Acceptance date: 2018-04-09
• DOI: 10.1007/978-3-319-95582-7_30
• ISBN: 9783319955827