Introduction
Goals of the Book and Contours of its Method
Stepwise Refinable Abstract Operational Modeling
Abstract Virtual Machine Notation
Practical Benefits
Harness Pseudo-Code by Abstraction and Refinement
Adding Abstraction and Rigor to UML Models
Synopsis of the Book
ASM Design and Analysis Method
Principles of Hierarchical System Design
Ground Model Construction (Requirements Capture)
Stepwise Refinement (Incremental Design)
Integration into Software Practice
Working Definition
Basic ASMs
Definition
Classification of Locations and Updates
ASM Modules
Illustration by Small Examples
Control State ASMs
Exercises
Explanation by Example: Correct Lift Control
Exercises
Detailed Definition (Math. Foundation)
Abstract States and Update Sets
Mathematical Logic
Transition Rules and Runs of ASMs
The Reserve of ASMs
Exercises
Notational Conventions
Basic ASMs
Requirements Capture by Ground Models
Fundamental Questions to be Asked
Illustration by Small Use Case Models
Exercises
Incremental Design by Refinements
Refinement Scheme and its Specializations
Two Refinement Verification Case Studies
Decomposing Refinement Verifications
Exercises
Microprocessor Design Case Study
Ground Model DLXseq
Parallel Model DLXpar Resolving Structural Hazards
Verifying Resolution of Structural Hazards (DLXpar)
Resolving Data Hazards (Refinement DLXdata)
Exercises
Structured ASMs (Composition Techniques)
Turbo ASMs (seq, iterate, submachines, recursion)
Seq and Iterate (Structured Programming)
Submachines and Recursion (Encapsulation and Hiding)
Analysis of Turbo ASM Steps
Exercises
Abstract State Processes (Interleaving)
Synchronous Multi-Agent ASMs
Robot Controller Case Study
Production Cell Ground Model
Refinement of the Production Cell Component ASMs
Exercises
Real-Time Controller (Railroad Crossing Case Study)
Real-Time Process Control Systems
Railroad Crossing Case Study
Exercises
Asynchronous Multi-Agent ASMs
Async ASMs: Definition and Network Examples
Mutual Exclusion
Master--Slave Agreement
Network Consensus
Load Balance
Leader Election and Shortest Path
Broadcast Acknowledgment (Echo)
Phase Synchronization
Routing Layer Protocol for Mobile Ad Hoc Networks
Exercises
Embedded System Case Study
Light Control Ground Model
Signature (Agents and Their State)
User Interaction (Manual Control)
Automatic Control
Failure and Service
Component Structure
Exercises
Time--Constrained Async ASMs
Kermit Case Study (Alternating Bit/Sliding Window)
Processor-Group-Membership Protocol Case Study
Exercises
Async ASMs with Durative Actions
Protocol Verification using Atomic Actions
Refining Atomic to Durative Actions
Exercises
Event--Driven ASMs
UML Diagrams for Dynamics
Exercises
Universal Design and Computation Model
Integrating Computation and Specification Models
Classical Computation Models
System Design Models
Exercises
Sequential ASM Thesis (A Proof from Postulates)
Gurevich's Postulates for Sequential Algorithms
Bounded-Choice Non-Determinism
Critical Terms for ASMs
Exercises
Tool Support for ASMs
Verification of ASMs
Logic for ASMs
Formalizing the Consistency of ASMs
Basic Axioms and Proof Rules of the Logic
Why Deterministic Transition Rules?
Completeness for Hierarchical ASMs
The Henkin Model Construction
An Extension with Explicit Step Information
Exercises
Model Checking of ASMs
Execution of ASMs
History and Survey of ASM Research
The Idea of Sharpening Turing's Thesis
Recognizing the Practical Relevance of ASMs
Testing the Practicability of ASMs
Architecture Design and Virtual Machines
Protocols
Why use ASMs for Hw/Sw Engineering?
Making ASMs Fit for their Industrial Deployment
Practical Case Studies
Industrial Pilot Projects and Further Applications
Tool Integration
Conclusion and Outlook
References
List of Problems
List of Figures
List of Tables
Index