Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems
| Authors | |
|---|---|
| Year of publication | 2008 |
| Type | Article in Proceedings |
| Conference | Proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08) |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | Client-Server systems; formal verification; infinite state systems; component-based system analysis |
| Description | In many real software systems like Client-Server systems, one can identify a stable part and a number of uniform components of the same type. 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. |
| Related projects: |