Formal verification of systems with an unlimited number of components

1 2 3 In many real component-based systems and patterns of component interaction, there can be identified a stable part (like control component, server, instance handler) and a number of uniform components of the same type (users, clients, instances). Such systems, so called Control-User systems, are often modelled using an infinite set of finite models of particular components, parametrised 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. In this paper, we propose a verification technique for checking LTL-like interaction properties on Control-User systems with unlimited number of components using finite-state verification. Our method is based on com1The authors have been supported by the grant No. 1ET400300504. 2The author has been...

• Type: Journal
• Year: 2008
• Where: IEE
• Authors: Pavlína Vareková, Barbora Zimmerova, Pavel Moravec 0002, Ivana Cerná
• Keywords: Control-User Systems, IEE 2008, Real Component-based Systems, Uniform Components