Reasoning about Contingent Events in Distributed Systems

Abstract

This dissertation is concerned with requirements analysis and design for open distributed systems. These are systems which are hacked about over time consisting of people, computers and other equipment collaborating on shared activities through a variety of media. The dissertation describes a theoretical framework for distinguishing and reasoning about patterns of action and interaction all the way from the computer systems to the processes of system evolution. It reports the validation of the approach in the design of a wide area communication system for an itinerant workforce of flight crew. The structure and behaviour of software and social processes is abstracted using an object oriented language, BETA, with conventions for concurrency, object aggregration, communication, classification and generalisation. The language is given an operational semantics in Milner's process calculus CCS. A proof assistant developed by Cleaveland is used to establish temporal properties of a domain expressed in the propositional mu-calculus. The power and versatility of this modelling apparatus is demonstrated by a reconstruction of a lengthy manual mutual exclusion proof. This machinery is used as the basis for a method of system development. The thesis identifies a taxonomy of architectural components, assembling them in a manner suggested by Winograd's language/action theory and Ciborra's transaction cost analysis. The inventory includes social roles, organisational units, distributed services and communication media. A domain is specified as a network of transactions between roles which may be performed by people or machines. The modelling apparatus allows us to systematically enumerate breakdowns, bottlenecks, gaps and inefficiencies in their performance. These perceptions allow system architects and their clients to envisage the kind of system support that may be needed to streamline transactions, improve them or even to change the organisation. Contingency in social and machine communication is central to reasoning about the fabric of transactions that articulate a workplace. To highlight these mismatches in a form that is accessible to people who expect to play a part in the organisation I simulate transaction networks using hypercard. By giving hypercard an operational semantics in CCS the simulation becomes a specification formally related to the pseudo-code description in BETA. A case study is reported of the application of the method to the design of a wide area multimedia system. The domain is modelled in pseudo-code as a recursive, concurrent invocation of a communicating subsystem. The hypercard simulation is analysed to identify where breakdowns might occur in the field and the results of observations are expressed in the form of a spreadsheet. The simulation is used to negotiate the resource and technical requirements of the new system which will be created by translating it into executable code. The dissertation concludes with a discussion of the design of a CASE tool and an advanced scripting environment for analysis and executable specification that is suggested by the work.