Parametrised Compositional Verification with Multiple Process and Data Types
The authors present an LTS-based (Labeled Transition System) CSP-like (Communicating Sequential Processes) formalism for expressing parameterized systems. The parameters are process types, which determine the number of replicated components, and data types, which enable components with a parameterized state space. They prove that the formalism is compositional and show how to combine two existing results for parameterized verification in order to check trace refinement between parameterized processes. The combined approach gives upper bounds, i.e., cut-offs, for types such that a parameterized verification task collapses into finitely many checks solvable by using existing finite state refinement checking tools.