科研之友
微信
新浪微博
Facebook
分享链接
摘要
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 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.
- 出版日期2012
