Abstract State Machines

1 Introduction.- 1.1 Goals of the Book and Contours of its Method.- 1.2 Synopsis of the Book.- 2 ASM Design and Analysis Method.- 2.1 Principles of Hierarchical System Design.- 2.2 Working Definition.- 2.3 Explanation by Example: Correct Lift Control.- 2.4 Detailed Definition (Math. Foundation).- 2.5 Notational Conventions.- 3 Basic ASMs.- 3.1 Requirements Capture by Ground Models.- 3.2 Incremental Design by Refinements.- 3.3 Microprocessor Design Case Study.- 4 Structured ASMs (Composition Techniques).- 4.1 Turbo ASMs (seq, iterate, submachines, recursion).- 4.2 Abstract State Processes (Interleaving).- 5 Synchronous Multi-Agent ASMs.- 5.1 Robot Controller Case Study.- 5.2 Real-Time Controller (Railroad Crossing Case Study).- 6 Asynchronous Multi-Agent ASMs.- 6.1 Async ASMs: Definition and Network Examples.- 6.2 Embedded System Case Study.- 6.3 Time-Constrained Async ASMs.- 6.4 Async ASMs with Durative Actions.- 6.5 Event-Driven ASMs.- 7 Universal Design and Computation Model.- 7.1 Integrating Computation and Specification Models.- 7.2 Sequential ASM Thesis (A Proof from Postulates).- 8 Tool Support for ASMs.- 8.1 Verification of ASMs.- 8.2 Model Checking of ASMs.- 8.3 Execution of ASMs.- 9 History and Survey of ASM Research.- 9.1 The Idea of Sharpening Turing's Thesis.- 9.2 Recognizing the Practical Relevance of ASMs.- 9.3 Testing the Practicability of ASMs.- 9.4 Making ASMs Fit for their Industrial Deployment.- 9.5 Conclusion and Outlook.- References.- List of Problems.- List of Figures.- List of Tables.