The Design of Communicating Systems

"The professional schools will resume their professional responsibilities just to the degree that they can discover a science of design, a body of intellectually tough, partly formalizable, partly empirical teachable doctrine about the design process. " [H.A. Simon, 1968} Design is aimed at the transformation or translation of a specification or high­ level description into a description in terms of some real-world primitives. As such it involves the removal of the uncertainty about the way in which a required system can be realized. To optimally support the design of systems, we must look at the design process as a whole and at the strong relationship that exists between a designer, the applied design method, the required design tools and the ways in which designs can be expressed. This book focuses on that relationship. The application field we are concerned with is the design of systems in which the communication between system elements is a major design feature. Examples of such communicating systems are: communication protocols, telephone exchange control systems, process control systems, highly modular systems, embedded software, interactive systems, and VLSI systems. In summary, we are concerned with systems in which concurrency plays a major role (concurrency defines the mutual relationship between the activities in the different parts of a system or within a collection of systems).

I Expressing Designs.- 1 The Basic Design Cycle.- 1.1 The two directions of the design process.- 1.2 Writing specifications and implementations.- 1.3 Verifications which shape design processes.- 1.4 Mechanisms for synthesis and verification..- 1.5 Trends in specification techniques.- 2 Calculus of Communicating Systems.- 2.1 Introduction to CCS.- 2.2 Actions.- 2.3 Representation of behaviours of agents.- 2.4 Semantics of CCS operators.- 2.5 Parallel composition of agents.- 2.6 Expansion law.- 2.7 Synchronization and value-passing.- 3 Verification.- 3.1 The principle of verification in CCS.- 3.2 Bisimulation and observation equivalence.- 3.3 An algorithm for finding a weak bisimulation.- 3.4 Verification induction.- 3.5 CCS laws.- 3.6 Verifying large expressions.- 3.7 An X-ray Diagnostic System (XDS).- 3.8 Verification of the XDS implementation.- 3.9 OSI-layers.- 4 Fairness, queues and time.- 4.1 Fairness.- 4.2 FIFO communication.- 4.3 Deriving time-out conditions.- 4.3.1 A transmission protocol.- 4.3.2 Calculating behaviour sequences.- 4.3.3 The impact of timing conditions.- 4.4 Translating programs into CCS.- 4.4.1 The LAN protocol.- 4.4.2 Some notational devices.- 4.4.3 Translation of the protocol into CCS.- 4.4.4 Expansion of the sender and receiver expressions.- 5 Synthesis.- 5.1 Synthesis strategies.- 5.2 Synthesis by mirroring.- 5.2.1 The principle of mirroring.- 5.2.2 Mirror observation equivalence.- 5.3 Synthesis by interface derivation.- 5.3.1 Causal relations.- 5.3.2 Synthesis rules.- 5.3.3 The Combination Algorithm.- 5.3.4 Linking a server to a communication network.- 5.4 Completing the specification.- 6 CCS and SDL.- 6.1 A short overview of SDL.- 6.2 Linking CCS and SDL.- 6.3 A pipeline.- 6.4 A handshake system.- 6.5 A network protocol.- 6.6 SS7 call processing control.- 7 CCS and Petri Nets.- 7.1 From CCS to Petri Nets.- 7.2 From Petri Nets to CCS.- 7.3 Communication via a shared buffer.- 7.4 Communication between a printer and a printer monitor.- 7.5 An assignment statement.- 7.6 A multiplier.- Ii A Design Method for Communicating SYSTEMS.- 8 Design Process Descriptions.- 8.1 A programming example.- 8.2 The basic design cycle.- 8.3 A design process model.- 8.4 Refinement of the design process model.- 8.5 Meta programs.- 8.6 Design method for communicating systems.- 9 The Communication Model.- 9.1 Introduction.- 9.2 Applying the combination algorithm.- 9.3 Introducing blocking behaviour.- 9.4 Verification of the result.- 9.5 The meta program.- 9.6 Communication model of switching nodes.- 10 The Application Model.- 10.1 The formalization step.- 10.2 Network concepts.- 10.3 Service area.- 10.4 The derivation of routing predicates.- 10.5 The connection model ml.- 10.6 A specification of upw, dwn, hor.- 10.7 The connection model m2.- 10.8 Error predicates - their effect on ml.- 10.9 Error predicates - their effect on m2.- 11 The Process Model.- 11.1 Introduction.- 11.2 The entrance process.- 11.3 Identification processes.- 11.4 Selection processes.- 11.5 The response process.- 11.6 Verification of the result.- 11.7 Data model.- Iii Design, Creativity and Learning.- 12 Design Iterations.- 12.1 Iterations and the basic design cycle.- 12.2 Godel’s theorem.- 12.3 Design and computability.- 12.4 Design and chaos.- 12.5 Design and entropy.- 13 The Role of CAD and Learning in Design.- 13.1 Computations in CAD.- 13.2 CAD and entropy.- 13.3 Learning and knowledge representation.- 14 Design Metrics.- 14.1 Design and information.213.- 14.2 The information content of a hardware design.- 14.3 Halstead’s metrics.- 14.4 The information content of a software program.- 14.5 Relating the Information Model with Halstead’s metrics.- 14.6 Development time estimation.