Temporal specifications of client-server systems and unbounded Agents[HBNI Th49]

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.