Parametrised Interface Automata

Interface theories (ITs) enable us to analyse the compatibility of interfaces and refine interfaces while preserving their compatibility. However, most ITs are for finite state interfaces whereas real software systems are heavily parametrised involving components, of which the number cannot be a priori fixed. We present, at least to our knowledge, the first IT which allows to specify the parametric number of parametrised interfaces. The formalism is based on interface automata (IAs), where the parameters are types, which determine the number of replicated components, and variables, which refer to individual components. Moreover, we provide a fully algorithmic procedure for checking the compatibility of and refinement between parametrised IAs. The procedure determines upper bounds, i.e., cut-offs, for the parameters such that both the parametrised verification tasks collapse into finitely many checks between finite state IAs up to the cut-offs. The proof technique behind the results is a generalisation of an existing technique used in the context of safety property verification. We have implemented the approach and applied it to an example system.