Abstract state machines A method for high level system design and analysis

Introduction......Page 9
Stepwise Refinable Abstract Operational Modeling......Page 11
Abstract Virtual Machine Notation......Page 13
Practical Benefits......Page 14
Harness Pseudo-Code by Abstraction and Refinement......Page 16
Adding Abstraction and Rigor to UML Models......Page 17
Synopsis of the Book......Page 18
Principles of Hierarchical System Design......Page 21
Ground Model Construction (Requirements Capture)......Page 24
Stepwise Refinement (Incremental Design)......Page 28
Integration into Software Practice......Page 34
Working Definition......Page 35
Definition......Page 36
Classification of Locations and Updates......Page 41
ASM Modules......Page 44
Illustration by Small Examples......Page 45
Control State ASMs......Page 52
Exercises......Page 61
Explanation by Example: Correct Lift Control......Page 62
Exercises......Page 70
Abstract States and Update Sets......Page 71
Mathematical Logic......Page 75
Transition Rules and Runs of ASMs......Page 79
The Reserve of ASMs......Page 84
Exercises......Page 90
Notational Conventions......Page 93
Requirements Capture by Ground Models......Page 95
Fundamental Questions to be Asked......Page 96
Illustration by Small Use Case Models......Page 100
Exercises......Page 117
Incremental Design by Refinements......Page 118
Refinement Scheme and its Specializations......Page 119
Two Refinement Verification Case Studies......Page 125
Decomposing Refinement Verifications......Page 141
Exercises......Page 142
Microprocessor Design Case Study......Page 145
Ground Model DLXseq......Page 146
Parallel Model DLXpar Resolving Structural Hazards......Page 148
Verifying Resolution of Structural Hazards (DLXpar)......Page 151
Resolving Data Hazards (Refinement DLXdata)......Page 156
Exercises......Page 164
Structured ASMs (Composition Techniques)......Page 167
Seq and Iterate (Structured Programming)......Page 168
Submachines and Recursion (Encapsulation and Hiding)......Page 175
Analysis of Turbo ASM Steps......Page 182
Exercises......Page 186
Abstract State Processes (Interleaving)......Page 188
Synchronous Multi-Agent ASMs......Page 195
Production Cell Ground Model......Page 196
Refinement of the Production Cell Component ASMs......Page 201
Exercises......Page 204
Real-Time Process Control Systems......Page 206
Railroad Crossing Case Study......Page 209
Exercises......Page 213
Asynchronous Multi-Agent ASMs......Page 215
Async ASMs: Definition and Network Examples......Page 216
Mutual Exclusion......Page 218
Master--Slave Agreement......Page 220
Network Consensus......Page 222
Load Balance......Page 223
Leader Election and Shortest Path......Page 224
Broadcast Acknowledgment (Echo)......Page 226
Phase Synchronization......Page 228
Routing Layer Protocol for Mobile Ad Hoc Networks......Page 231
Exercises......Page 236
Light Control Ground Model......Page 237
User Interaction (Manual Control)......Page 239
Automatic Control......Page 244
Failure and Service......Page 245
Component Structure......Page 247
Time--Constrained Async ASMs......Page 248
Kermit Case Study (Alternating Bit/Sliding Window)......Page 249
Processor-Group-Membership Protocol Case Study......Page 260
Exercises......Page 267
Async ASMs with Durative Actions......Page 268
Protocol Verification using Atomic Actions......Page 269
Refining Atomic to Durative Actions......Page 276
Event--Driven ASMs......Page 279
UML Diagrams for Dynamics......Page 282
Exercises......Page 290
Integrating Computation and Specification Models......Page 291
Classical Computation Models......Page 293
System Design Models......Page 301
Exercises......Page 308
Sequential ASM Thesis (A Proof from Postulates)......Page 309
Gurevich\'s Postulates for Sequential Algorithms......Page 310
Critical Terms for ASMs......Page 315
Exercises......Page 319
Verification of ASMs......Page 321
Logic for ASMs......Page 322
Formalizing the Consistency of ASMs......Page 323
Basic Axioms and Proof Rules of the Logic......Page 325
Why Deterministic Transition Rules?......Page 334
Completeness for Hierarchical ASMs......Page 336
The Henkin Model Construction......Page 338
An Extension with Explicit Step Information......Page 342
Exercises......Page 344
Model Checking of ASMs......Page 346
Execution of ASMs......Page 348
History and Survey of ASM Research......Page 351
The Idea of Sharpening Turing\'s Thesis......Page 352
Recognizing the Practical Relevance of ASMs......Page 353
Architecture Design and Virtual Machines......Page 357
Protocols......Page 359
Why use ASMs for Hw/Sw Engineering?......Page 360
Practical Case Studies......Page 362
Industrial Pilot Projects and Further Applications......Page 364
Tool Integration......Page 370
Conclusion and Outlook......Page 373
References......Page 377
List of Problems......Page 439
List of Figures......Page 441
List of Tables......Page 443
Index......Page 445