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

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

MORAVCOVÁ VAŘEKOVÁ Pavlína VAŘEKOVÁ Ivana ČERNÁ Ivana

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

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.