Introduction to the Formal Design of Real-Time Systems

but when we state that A 'equals' B , as well having to know what we mean by A and B we also have know what we mean by 'equals'. This section explores the role of observers; how different types of observ­ er see different things as being equal, and how we can produce algo­ rithms to decide on such equalities. It also explores how we go about writing specifications to which we may compare our SCCS designs. • The final section is the one which the students like best. Once enough of SCCS is grasped to decide upon the component parts of a design, the 'turning the handle' steps of composition and check­ ing that the design meets its specification are both error-prone and tedious. This section introduces the concurrency work bench, which shoulders most of the burden. How you use the book is up to you; I'm not even going to suggest path­ ways. Individual readers know what knowledge they seek, and course leaders know which concepts they are trying to impart and in what order.

1 Scene Set.- 1.1 Making Models.- 1.2 Lies, Damn Lies and Models.- 1.3 Abstraction, Atomicity and Algebras.- 1.3.1 Algebras, Specifications and Other Related Things.- 1.4 Labelled Transition Systems.- 1.4.1 An Algebra of Transition Systems.- 1.5 One at Once, All Together and In Time.- 1.5.1 A Process Algebra for Sequential Systems.- 1.5.2 A Process Algebra for Concurrent Systems.- 1.6 Real-Time Systems.- 2 Concurrency and Communication.- 2.1 Concurrency - Defining the Problems.- 2.2 Programming Domain Solutions.- 2.2.1 Mutual Exclusion.- 2.2.2 Critical Sections.- 2.2.3 Synchronisation.- 2.2.4 Semaphores.- 2.2.5 Monitors.- 2.3 Review and Rethink.- 3 Message Passing.- 3.1 Choosing the Best.- 3.1.1 The Contenders.- 3.1.2 The Choosing.- 3.2 Blocking Send.- 3.3 CCS (Calculus of Communicating Systems).- 3.4 Rendezvous.- 3.5 Conclusion.- 4 Synchronous Calculus of Communicating Systems.- 4.1 An Overview of SCCS.- 4.2 Plain SCCS.- 4.2.1 Naming of Parts.- 4.2.2 Basic Operators and Propositions.- 4.3 Recursion.- 4.3.1 Recursion in SCCS Terms.- 4.3.2 Derived Agents.- 4.4 Actions, Particles, Composites and All Sorts.- 4.5 Synchronisation.- 4.5.1 Interaction.- 4.6 Constructional Design.- 4.6.1 Scoping and Synchronisation.- 4.6.2 Choice of Choices.- 4.6.3 Example - Software Interrupts.- 4.6.4 Distributing Pruning over Product.- 4.7 Message Passing.- 4.7.1 Parameter Passing.- 4.7.2 Message Passing.- 4.7.3 Predicated Choice.- 4.8 Agents Lurking.- 4.8.1 Delay ?.- 4.8.2 One Agent Waits.- 4.8.3 Both Agents Wait.- 4.8.4 Examples.- 4.8.5 Message Passing and Waiting.- 4.9 Specifications and Proof.- 4.9.1 Mutual Exclusion.- 4.9.2 Livelock - Software Scheduler.- 4.9.3 Deadlock - Software Scheduler.- 4.9.4 Comments.- 5 Equivalence.- 5.0 The Need For Equivalence.- 5.1 Traces.- 5.2 From Traces to Bisimulations.- 5.3 Bisimulation.- 5.3.1 Strong Bisimulation.- 5.3.2 From Strong Bisimulation to an Equivalence.- 5.3.3 Observational Equivalence.- 5.3.4 Observational Congruence.- 6 Automating SCCS.- 6.0 Concurrency Work Bench: an Introduction.- 6.1 CWB and Agent Behaviours.- 6.2 Agents, Bisimulation and CWB.- 6.3 Comments.- 7 Proving Things Correct.- 7.1 Modal Logics.- 7.1.1 Hennessy-Milner Logic.- 7.1.2 Propositional Modal Mu-Calculus - Modal Logic plus Fixed Points.- 7.2 Modal Logic, CWB and Satisfaction.- 8 End End Note.- Appendix 1 Some of the More Useful SCCS Propositions.- Appendix 2 Notation Used Throughout the Book.- References.