Abstract State Machines

by Borger, Egon; Stark, Robert F.

• ISBN13: 9783540007029
• ISBN10: 3540007024
• Edition: CD
• Format: Hardcover
• Copyright: 2003-08-01
• Publisher: Springer Nature

Summary

The systems engineering method proposed in this book, which is based on Abstract State Machines (ASMs), guides the development of software and embedded hardware-software systems seamlessly from requirements capture to actual implementation and documentation. The method bridges the gap between the human understanding and formulation of real-world problems and the deployment of their algorithmic solutions by code-executing machines. Within a single conceptual framework it covers design, verification by reasoning techniques, and validation by simulation and testing. ASMs improve current industrial practice by using accurate high-level modeling and by linking the descriptions at the successive stages of system development in an organic and efficiently maintainable chain of rigorous and coherent system models at stepwise-refined abstraction levels. In several industrial projects the ASM method has proven its superiority compared to the popular UML methodology when designing complex parallel or dynamic systems.This book combines the features of a textbook and a handbook: the reader will find detailed explanations, proofs, and exercises as well as numerous examples and real-world case studies. Researchers will find here the most comprehensive description of ASMs available today and professionals will use it as a "modeling handbook for the working software engineer." As a textbook it supports self-study or it can form the basis of a lecture course. The book is complemented by a CD containing the whole book text, additional course material, solutions to exercises, and additional examples. Even more information can be found on the related website maintained by the authors: http://www.di.unipi.it/AsmBook/

Table of Contents

Introduction	p. 1
Goals of the Book and Contours of its Method	p. 3
Stepwise Refutable Abstract Operational Modeling	p. 3
Abstract Virtual Machine Notation	p. 5
Practical Benefits	p. 6
Harness Pseudo-Code by Abstraction and Refinement	p. 8
Adding Abstraction and Rigor to UML Models	p. 9
Synopsis of the Book	p. 10
ASM Design and Analysis Method	p. 13
Principles of Hierarchical System Design	p. 13
Ground Model Construction (Requirements Capture)	p. 16
Stepwise Refinement (Incremental Design)	p. 20
Integration into Software Practice	p. 26
Working Definition	p. 27
Basic ASMs	p. 28
Definition	p. 28
Classification of Locations and Updates	p. 33
ASM Modules	p. 36
Illustration by Small Examples	p. 37
Control State ASMs	p. 44
Exercises	p. 53
Explanation by Example: Correct Lift Control	p. 54
Exercises	p. 62
Detailed Definition (Math. Foundation)	p. 63
Abstract States and Update Sets	p. 63
Mathematical Logic	p. 67
Transition Rules and Runs of ASMs	p. 71
The Reserve of ASMs	p. 76
Exercises	p. 82
Notational Conventions	p. 85
Basic ASMs	p. 87
Requirements Capture by Ground Models	p. 87
Fundamental Questions to be Asked	p. 88
Illustration by Small Use Case Models	p. 92
Exercises	p. 109
Incremental Design by Refinements	p. 110
Refinement Scheme and its Specializations	p. 111
Two Refinement Verification Case Studies	p. 117
Decomposing Refinement Verifications	p. 133
Exercises	p. 134
Microprocessor Design Case Study	p. 137
Ground Model DLXseq	p. 138
Parallel Model DLXpar Resolving Structural Hazards	p. 140
Verifying Resolution of Structural Hazards (DLXpar)	p. 143
Resolving Data Hazards (Refinement DLXdata)	p. 148
Exercises	p. 156
Structured ASMs (Composition Techniques)	p. 159
Turbo ASMs (seq, iterate, submachines, recursion)	p. 160
Seq and Iterate (Structured Programming)	p. 160
Submachines and Recursion (Encapsulation and Hiding)	p. 167
Analysis of Turbo ASM Steps	p. 174
Exercises	p. 178
Abstract State Processes (Interleaving)	p. 180
Synchronous Multi-Agent ASMs	p. 187
Robot Controller Case Study	p. 188
Production Cell Ground Model	p. 188
Refinement of the Production Cell Component ASMs	p. 193
Exercises	p. 196
Real-Time Controller (Railroad Crossing Case Study)	p. 198
Real-Time Process Control Systems	p. 198
Railroad Crossing Case Study	p. 201
Exercises	p. 205
Asynchronous Multi-Agent ASMs	p. 207
Async ASMs: Definition and Network Examples	p. 208
Mutual Exclusion	p. 210
Master-Slave Agreement	p. 212
Network Consensus	p. 214
Load Balance	p. 215
Leader Election and Shortest Path	p. 216
Broadcast Acknowledgment (Echo)	p. 218
Phase Synchronization	p. 220
Routing Layer Protocol for Mobile Ad Hoc Networks	p. 223
Exercises	p. 228
Embedded System Case Study	p. 229
Light Control Ground Model	p. 229
Signature (Agents and Their State)	p. 231
User Interaction (Manual Control)	p. 231
Automatic Control	p. 236
Failure and Service	p. 237
Component Structure	p. 239
Exercises	p. 240
Time-Constrained Async ASMs	p. 240
Kermit Case Study (Alternating Bit/Sliding Window)	p. 241
Processor-Group-Membership Protocol Case Study	p. 252
Exercises	p. 259
Async ASMs with Durative Actions	p. 260
Protocol Verification using Atomic Actions	p. 261
Refining Atomic to Durative Actions	p. 268
Exercises	p. 271
Event-Driven ASMs	p. 271
UML Diagrams for Dynamics	p. 274
Exercises	p. 282
Universal Design and Computation Model	p. 283
Integrating Computation and Specification Models	p. 283
Classical Computation Models	p. 285
System Design Models	p. 293
Exercises	p. 300
Sequential ASM Thesis (A Proof from Postulates)	p. 301
Gurevich's Postulates for Sequential Algorithms	p. 302
Bounded-Choice Non-Determinism	p. 307
Critical Terms for ASMs	p. 307
Exercises	p. 311
Tool Support for ASMs	p. 313
Verification of ASMs	p. 313
Logic for ASMs	p. 314
Formalizing the Consistency of ASMs	p. 315
Basic Axioms and Proof Rules of the Logic	p. 317
Why Deterministic Transition Rules?	p. 326
Completeness for Hierarchical ASMs	p. 328
The Henkin Model Construction	p. 330
An Extension with Explicit Step Information	p. 334
Exercises	p. 336
Model Checking of ASMs	p. 338
Execution of ASMs	p. 340
History and Survey of ASM Research	p. 343
The Idea of Sharpening Turing's Thesis	p. 344
Recognizing the Practical Relevance of ASMs	p. 345
Testing the Practicability of ASMs	p. 349
Architecture Design and Virtual Machines	p. 349
Protocols	p. 351
Why use ASMs for Hw/Sw Engineering?	p. 352
Making ASMs Fit for their Industrial Deployment	p. 354
Practical Case Studies	p. 354
Industrial Pilot Projects and Further Applications	p. 356
Tool Integration	p. 362
Conclusion and Outlook	p. 365
References	p. 369
List of Problems	p. 429
List of Figures	p. 431
List of Tables	p. 433
Index	p. 435
Table of Contents provided by Publisher. All Rights Reserved.