Abstract State Machines. A Method for High-Level System Design and Analysis

Description

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