Börger / Stärk Abstract State Machines

A Method for High-Level System Design and Analysis
2003
ISBN: 978-3-642-18216-7
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 438 Seiten, eBook

Zielgruppe

Professional/practitioner

Autoren/Hrsg.

Börger, Egon

Stärk, Robert

Inhaltsverzeichnis

1 Introduction.- 1.1 Goals of the Book and Contours of its Method.- 1.1.1 Stepwise Refinable Abstract Operational Modeling.- 1.1.2 Abstract Virtual Machine Notation.- 1.1.3 Practical Benefits.- 1.1.4 Harness Pseudo-Code by Abstraction and Refinement.- 1.1.5 Adding Abstraction and Rigor to UML Models.- 1.2 Synopsis of the Book.- 2 ASM Design and Analysis Method.- 2.1 Principles of Hierarchical System Design.- 2.1.1 Ground Model Construction (Requirements Capture).- 2.1.2 Stepwise Refinement (Incremental Design).- 2.1.3 Integration into Software Practice.- 2.2 Working Definition.- 2.2.1 Basic ASMs.- 2.2.2 Definition.- 2.2.3 Classification of Locations and Updates.- 2.2.4 ASM Modules.- 2.2.5 Illustration by Small Examples.- 2.2.6 Control State ASMs.- 2.2.7 Exercises.- 2.3 Explanation by Example: Correct Lift Control.- 2.3.1 Exercises.- 2.4 Detailed Definition (Math. Foundation).- 2.4.1 Abstract States and Update Sets.- 2.4.2 Mathematical Logic.- 2.4.3 Transition Rules and Runs of ASMs.- 2.4.4 The Reserve of ASMs.- 2.4.5 Exercises.- 2.5 Notational Conventions.- 3 Basic ASMs.- 3.1 Requirements Capture by Ground Models.- 3.1.1 Fundamental Questions to be Asked.- 3.1.2 Illustration by Small Use Case Models.- 3.1.3 Exercises.- 3.2 Incremental Design by Refinements.- 3.2.1 Refinement Scheme and its Specializations.- 3.2.2 Two Refinement Verification Case Studies.- 3.2.3 Decomposing Refinement Verifications.- 3.2.4 Exercises.- 3.3 Microprocessor Design Case Study.- 3.3.1 Ground Model DLXseq.- 3.3.2 Parallel Model DLXpar Resolving Structural Hazards.- 3.3.3 Verifying Resolution of Structural Hazards (DLXpar).- 3.3.4 Resolving Data Hazards (Refinement DLXdata).- 3.3.5 Exercises.- 4 Structured ASMs (Composition Techniques).- 4.1 Turbo ASMs (seq, iterate, submachines, recursion).- 4.1.1 Seq and Iterate (Structured Programming).- 4.1.2 Submachines and Recursion (Encapsulation and Hiding).- 4.1.3 Analysis of Turbo ASM Steps.- 4.1.4 Exercises.- 4.2 Abstract State Processes (Interleaving).- 5 Synchronous Multi-Agent ASMs.- 5.1 Robot Controller Case Study.- 5.1.1 Production Cell Ground Model.- 5.1.2 Refinement of the Production Cell Component ASMs.- 5.1.3 Exercises.- 5.2 Real-Time Controller (Railroad Crossing Case Study).- 5.2.1 Real-TimeProcess Control Systems.- 5.2.2 Railroad Crossing Case Study.- 5.2.3 Exercises.- 6 Asynchronous Multi-Agent ASMs.- 6.1 Async ASMs: Definition and Network Examples.- 6.1.1 Mutual Exclusion.- 6.1.2 Master-Slave Agreement.- 6.1.3 Network Consensus.- 6.1.4 Load Balance.- 6.1.5 Leader Election and Shortest Path.- 6.1.6 Broadcast Acknowledgment (Echo).- 6.1.7 Phase Synchronization.- 6.1.8 Routing Layer Protocol for Mobile Ad Hoc Networks.- 6.1.9 Exercises.- 6.2 Embedded System Case Study.- 6.2.1 Light Control Ground Model.- 6.2.2 Signature (Agents and Their State).- 6.2.3 User Interaction (Manual Control).- 6.2.4 Automatic Control.- 6.2.5 Failure and Service.- 6.2.6 Component Structure.- 6.2.7 Exercises.- 6.3 Time-Constrained Async ASMs.- 6.3.1 Kermit Case Study (Alternating Bit/Sliding Window).- 6.3.2 Processor-Group-Membership Protocol Case Study.- 6.3.3 Exercises.- 6.4 Async ASMs with Durative Actions.- 6.4.1 Protocol Verification using Atomic Actions.- 6.4.2 Refining Atomic to Durative Actions.- 6.4.3 Exercises.- 6.5 Event-Driven ASMs.- 6.5.1 UML Diagrams for Dynamics.- 6.5.2 Exercises.- 7 Universal Design and Computation Model.- 7.1 Integrating Computation and Specification Models.- 7.1.1 Classical Computation Models.- 7.1.2 System Design Models.- 7.1.3 Exercises.- 7.2 Sequential ASM Thesis (A Proof from Postulates).- 7.2.1 Gurevich’s Postulates for Sequential Algorithms.- 7.2.2 Bounded-Choice Non-Determinism.- 7.2.3 Critical Terms for ASMs.- 7.2.4 Exercises.- 8 Tool Support for ASMs.- 8.1 Verification of ASMs.- 8.1.1 Logic for ASMs.- 8.1.2 Formalizing the Consistency of ASMs.- 8.1.3 Basic Axioms and Proof Rules of the Logic.- 8.1.4 Why Deterministic Transition Rules?.- 8.1.5 Completeness for Hierarchical ASMs.- 8.1.6 The Henkin Model Construction.- 8.1.7 An Extension with Explicit Step Information.- 8.1.8 Exercises.- 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.3.1 Architecture Design and Virtual Machines.- 9.3.2 Protocols.- 9.3.3 Why use ASMs for Hw/Sw Engineering?.- 9.4 Making ASMs Fit for their Industrial Deployment.- 9.4.1 Practical Case Studies.- 9.4.2 Industrial Pilot Projects and Further Applications.- 9.4.3 Tool Integration.- 9.5 Conclusion and Outlook.- References.- List of Problems.- List of Figures.- List of Tables.