Mazur, Tomasz and Lowe, Gavin - A type reduction theory for systems with replicated components

lmcs:869 - Logical Methods in Computer Science, February 16, 2012, Volume 8, Issue 1
A type reduction theory for systems with replicated components

Authors: Mazur, Tomasz and Lowe, Gavin

The Parameterised Model Checking Problem asks whether an implementation Impl(t) satisfies a specification Spec(t) for all instantiations of parameter t. In general, t can determine numerous entities: the number of processes used in a network, the type of data, the capacities of buffers, etc. The main theme of this paper is automation of uniform verification of a subclass of PMCP with the parameter of the first kind, i.e. the number of processes in the network. We use CSP as our formalism. We present a type reduction theory, which, for a given verification problem, establishes a function \phi that maps all (sufficiently large) instantiations T of the parameter to some fixed type T^ and allows us to deduce that if Spec(T^) is refined by \phi(Impl(T)), then (subject to certain assumptions) Spec(T) is refined by Impl(T). The theory can be used in practice by combining it with a suitable abstraction method that produces a t-independent process Abstr that is refined by {\phi}(Impl(T)) for all sufficiently large T. Then, by testing (with a model checker) if the abstract model Abstr refines Spec(T^), we can deduce a positive answer to the original uniform verification problem. The type reduction theory relies on symbolic representation of process behaviour. We develop a symbolic operational semantics for CSP processes that satisfy certain normality requirements, and we provide a set of translation rules that allow us to concretise symbolic transition graphs. Based on this, we prove results that allow us to infer behaviours of a process instantiated with uncollapsed types from known behaviours of the same process instantiated with a reduced type. One of the main advantages of our symbolic operational semantics and the type reduction theory is their generality, which makes them applicable in a wide range of settings.


Source : oai:arXiv.org:1201.1716
DOI : 10.2168/LMCS-8(1:4)2012
Volume: Volume 8, Issue 1
Published on: February 16, 2012
Submitted on: January 5, 2011
Keywords: Computer Science - Logic in Computer Science,D.1.3, D.2.4, D.3.2


Share

Consultation statistics

This page has been seen 31 times.
This article's PDF has been downloaded 12 times.