Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems

In many real software systems like Client-Server systems, one can identify a stable part (server, instance handler, control component) and a number of uniform components of the same type (clients, instances, users). When analysing performance and correctness of these systems we need to answer questions like "What is the maximal possible number of clients which can be handled simultaneously?" or more generally "What is the maximal possible number of clients which are in the some special situation when the control component is in a particular state?". In the paper we propose an automated technique solving such questions. For Client-Server systems we reduce the problem of finding the upper bound on the number of handled clients to the formal verification of reachability properties in infinite state transition systems. For the verification task we propose an efficient and fully automated algorithm which combines several techniques proposed in existing literature. Applying the algorithm we verify models of several previously published systems.