A TYPE REDUCTION THEORY FOR SYSTEMS WITH REPLICATED COMPONENTS
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 ma...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2012
|
| _version_ | 1797066584314871808 |
|---|---|
| author | Mazur, T Lowe, G |
| author_facet | Mazur, T Lowe, G |
| author_sort | Mazur, T |
| collection | OXFORD |
| description | 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 φ{symbol} 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 φ{symbol}(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 φ{symbol}(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 reduc- tion theory is their generality, which makes them applicable in a wide range of settings. © T. Mazur and G. Lowe. |
| first_indexed | 2024-03-06T21:44:10Z |
| format | Journal article |
| id | oxford-uuid:48f9aba0-b9a1-4fba-964e-bc57b681acbf |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T21:44:10Z |
| publishDate | 2012 |
| record_format | dspace |
| spelling | oxford-uuid:48f9aba0-b9a1-4fba-964e-bc57b681acbf2022-03-26T15:28:53ZA TYPE REDUCTION THEORY FOR SYSTEMS WITH REPLICATED COMPONENTSJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:48f9aba0-b9a1-4fba-964e-bc57b681acbfEnglishSymplectic Elements at Oxford2012Mazur, TLowe, GThe 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 φ{symbol} 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 φ{symbol}(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 φ{symbol}(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 reduc- tion theory is their generality, which makes them applicable in a wide range of settings. © T. Mazur and G. Lowe. |
| spellingShingle | Mazur, T Lowe, G A TYPE REDUCTION THEORY FOR SYSTEMS WITH REPLICATED COMPONENTS |
| title | A TYPE REDUCTION THEORY FOR SYSTEMS WITH REPLICATED COMPONENTS |
| title_full | A TYPE REDUCTION THEORY FOR SYSTEMS WITH REPLICATED COMPONENTS |
| title_fullStr | A TYPE REDUCTION THEORY FOR SYSTEMS WITH REPLICATED COMPONENTS |
| title_full_unstemmed | A TYPE REDUCTION THEORY FOR SYSTEMS WITH REPLICATED COMPONENTS |
| title_short | A TYPE REDUCTION THEORY FOR SYSTEMS WITH REPLICATED COMPONENTS |
| title_sort | type reduction theory for systems with replicated components |
| work_keys_str_mv | AT mazurt atypereductiontheoryforsystemswithreplicatedcomponents AT loweg atypereductiontheoryforsystemswithreplicatedcomponents AT mazurt typereductiontheoryforsystemswithreplicatedcomponents AT loweg typereductiontheoryforsystemswithreplicatedcomponents |