Temporal specifications of client-server systems and unbounded Agents (Record no. 48875)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 03737nam a2200277Ia 4500 |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 160627s2013||||xx |||||||||||||| ||und|| |
| 080 ## - UNIVERSAL DECIMAL CLASSIFICATION NUMBER | |
| Universal Decimal Classification number | HBNI Th49 |
| 100 ## - MAIN ENTRY--AUTHOR NAME | |
| Personal name | Sheerazuddin, S |
| Relator term | author |
| 245 ## - TITLE STATEMENT | |
| Title | Temporal specifications of client-server systems and unbounded Agents |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) | |
| Year of publication | 2013 |
| 300 ## - PHYSICAL DESCRIPTION | |
| Number of Pages | 164p. |
| 502 ## - DISSERTATION NOTE | |
| Dissertation note | 2013 |
| 502 ## - DISSERTATION NOTE | |
| Degree Type | Ph.D |
| 502 ## - DISSERTATION NOTE | |
| Name of granting institution | HBNI |
| 520 3# - SUMMARY, ETC. | |
| Summary, etc | 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. |
| 650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical Term | Computer Science |
| 653 10 - INDEX TERM--UNCONTROLLED | |
| Uncontrolled term | Client Server Model |
| 653 10 - INDEX TERM--UNCONTROLLED | |
| Uncontrolled term | Decidable Logics |
| 653 10 - INDEX TERM--UNCONTROLLED | |
| Uncontrolled term | HBNI Th 49 |
| 653 10 - INDEX TERM--UNCONTROLLED | |
| Uncontrolled term | Temporal Logics |
| 653 10 - INDEX TERM--UNCONTROLLED | |
| Uncontrolled term | Temporal Specifications |
| 720 1# - ADDED ENTRY--UNCONTROLLED NAME | |
| Thesis Advisor | Ramanujam, R. |
| Relator term | Thesis advisor [ths] |
| 856 ## - ELECTRONIC LOCATION AND ACCESS | |
| Uniform Resource Identifier | http://www.imsc.res.in/xmlui/handle/123456789/335 |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Koha item type | THESIS & DISSERTATION |
| Withdrawn status | Lost status | Damaged status | Not for loan | Current library | Full call number | Accession Number | Uniform Resource Identifier | Koha item type |
|---|---|---|---|---|---|---|---|---|
| IMSc Library | HBNI Th49 | 67763 | http://www.imsc.res.in/xmlui/handle/123456789/335 | THESIS & DISSERTATION |