Introduction to the Formal Design of Real-Time Systems

1 Scene Set.- 1.1 Making Models.- 1.2 Lies, Damn Lies and Models.- 1.3 Abstraction, Atomicity and Algebras.- 1.4 Labelled Transition Systems.- 1.5 One at Once, All Together and In Time.- 1.6 Real-Time Systems.- 2 Concurrency and Communication.- 2.1 Concurrency - Defining the Problems.- 2.2 Programming Domain Solutions.- 2.3 Review and Rethink.- 3 Message Passing.- 3.1 Choosing the Best.- 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.3 Recursion.- 4.4 Actions, Particles, Composites and All Sorts.- 4.5 Synchronisation.- 4.6 Constructional Design.- 4.7 Message Passing.- 4.8 Agents Lurking.- 4.9 Specifications and Proof.- 5 Equivalence.- 5.0 The Need For Equivalence.- 5.1 Traces.- 5.2 From Traces to Bisimulations.- 5.3 Bisimulation.- 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.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.