Paper Info
Title
Parametrised Compositional Verification with Multiple Process and Data Types
Abstract
We present an LTS-based (Labelled Transition System) CSP-like (Communicating Sequential Processes) formalism for expressing parametrised systems. The parameters are process types, which determine the number of replicated components, and data types, which enable components with a parametrised state space. We prove that the formalism is compositional and show how to combine two existing results for parametrised verification in order to check trace refinement between parametrised processes. The combined approach gives upper bounds, i.e., cut-offs, for types such that a parametrised verification task collapses into finitely many checks solvable by using existing finite state refinement checking tools. We have implemented the approach and applied it to prove mutual exclusion properties of network protocols and systems with shared resources. To the best our knowledge, our technique is the only one that combines compositionality and completeness with support for multiple parametric process and data types.
Year
DOI
Venue
2013
10.1109/ACSD.2013.9
ACSD
Keywords
Field
DocType
parametrised compositional verification,parametrised verification,parametrised state space,parametrised verification task collapse,data types,existing finite state refinement,existing result,parametrised process,data type,multiple parametric process,combined approach,multiple process,parametrised system,process calculus,upper bound,formal verification,communicating sequential processes,protocols,process control,cost accounting,calculus,semantics
Transition system,Computer science,Communicating sequential processes,Algorithm,Theoretical computer science,Data type,Mutual exclusion,Process calculus,Completeness (statistics),State space,Formal verification
Conference
ISSN
Citations 
PageRank 
1550-4808
4
0.42
References 
Authors
14
2
Name
Order
Citations
PageRank
Antti Siirtola1445.62
Keijo Heljanko275147.90