Abstract:
The Client-server model of computing is a distributed application structure that
partitions tasks or workloads between service providers, called servers, and service requesters, called clients. In this thesis, the formal specification and
verification of such client server systems are studied. For convenience, they are considered to be of two kinds: Single Client Multiple Server Systems (SCMS) and Single Server Multiple Client Systems (SSMC).
In SCMS systems, a single client interacts with a host of servers, directly or
indirectly, to obtain some service. The number of servers is fixed a priori. The
use of formal methods for SCMS is concentrated mainly on reasoning about communication among the various servers. In particular, the challenge is to come up
with appropriate logical languages to describe good (valid) patterns and with procedures for checking that all behaviours (computations) of a given system conform
to these good patterns. The suitability of m-LTL is explored to specify properties of SCMS systems, and found that two changes are appropriate. The main theorem for w-LTL that we present is the decidability of satisfiability and model checking. For each paradigm, we present an automaton model, System of Passive Clients
(SPS) for discrete services and System of Active Clients (SAS), for session-oriented
services. Our models have the desired capability, they allow for unbounded number
of clients. Consequently, these are infinite space systems. As a result, their reachability properties are typically undecidable to check. In this thesis it is shown that SAS are equivalent to (or have the same behaviour as) multi-counter automata, whereas SPS is a subclass of SAS. The class of SAS machines have the same closure properties as class of counter machines with no zero test. There are several candidate temporal logics for message passing systems, but these work with a priori fixed number of agents, and for any message, the identity of the sender and the receiver are fixed at design time. It is needed to extend such logics with means for referring to agents in some more abstract manner (than by name).
A natural and direct approach to refer to unknown clients is to use logical variables:
Rather than work with atomic propositions p, we use monadic predicates p(x) to refer to property p being true of client x. One can quantify over such x existentially and universally to specify policies relating clients. It is shown that, the satisfiability and model checking of LSPS to be decidable. The proof uses a formula automaton construction, and in this sense, offers some novelty for a temporal logic with some (limited) quantification. A fragment of monadic monodic temporal logic is proposed as the specification language for SAS. A formula automaton
construction is presented, using a multi-counter automaton, that leads to a non-elementary decision procedure for the satisfiability of LSAS.