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 in finite 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 in finite-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 veri. cation technique for checking linear temporal logic (LTL)-like interaction properties on control-user systems with unlimited number of components using finite-state veri. cation 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 de. ne 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.