Formal verification of systems with an unlimited number of components

In many real component-based systems and patterns of component interaction, there can be identified a stable part (such as control component, server, instance handler) and a number of uniform components of the same type (users, clients, instances). Such systems, the so-called control-user systems, are often modelled using an infinite set of finite models of particular components, parameterised by the number of uniform components in the system. However, if the maximal number of components is not known, this results in infinite-state models, which cannot be directly verified with effective (finite-state) techniques, like model checking. In this case, more involved techniques have to be employed. A verification technique for checking linear temporal logic (LTL)-like interaction properties on control-user systems with unlimited number of components using finite-state verification is proposed. The method is based on computing a cutoff on the number of uniform components (users), such that if the system is proved to be correct for every number of user components up to the cutoff, it is guaranteed to be correct for any larger number of components. The authors define the cutoff, prove that it guarantees the required property, introduce heuristics for computing the cutoff and demonstrate the overall technique on a number of previously published models.