Egon Börger
Robert Stärk
Abstract State Machines
A Method for High-Level System Design and Analysis
X+440p., Springer-Verlag, 2003, ISBN 3-540-00702-4

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. 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.

This book combines the features of a textbook and a handbook. 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 AsmBook Website maintained by the authors.

### Overview

Copyright
Content of the CD
Links

### Copyright

This work consists of a printed book and a CD-ROM packaged with the book, and is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilm or in any other way, and storage in data banks. Duplication of this publication or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965, in its current version, and permission for use must always be obtained from Springer-Verlag. Violations are liable for prosecution under the German Copyright Law. Springer-Verlag or the authors make no warranty for representation, either expressed or implied with respect to this CD-ROM or book, including their quality, merchantibility, or fitness for a particular purpose. In no event will Springer or the authors be liable for direct, indirect, special, incidental, or consequential damages arising out of the use or inability to use the CD-ROM or book, even if Springer-Verlag or the authors have been advised of the possibility of such damages.

### Content of the CD

[ Note: You can view and print Adobe PDF files with the free Acrobat Reader® software. ]

[ Note: If the links in a PDF file do not work, open the file directly from the CD with Acrobat Reader. ]

- AsmBook.pdf, Solutions.pdf
  The book and the solutions to exercises in PDF format with embedded links to PDF slides.
- AsmBookPPT.pdf, SolutionsPPT.pdf
  The book and the solutions to exercises in PDF format with embedded links to PowerPoint slides.
- Lectures (PDF/PowerPoint slides)
  - AsmDefinition [ pdf ]
  - AsmMethod [ pdf | ppt ]
  - ASP [ pdf ]
  - AsyncASM [ pdf | ppt ]
  - Bakery [ pdf | ppt ]
  - ComponentModel [ pdf | ppt ]
  - DbRecovery [ pdf | ppt ]
  - Debugger [ pdf | ppt ]
  - Falko [ pdf | ppt ]
  - GateController [ pdf | ppt ]
  - GroupMemberProtocol [ pdf | ppt ]
  - Kermit [ pdf | ppt ]
  - LightControl [ pdf ]
  - LightControlRequirements [ pdf ]
  - PipeliningRISC [ pdf | ppt ]
  - ProdCell [ pdf | ppt ]
  - RefinemtMeth [ pdf | ppt ]
  - TurboASM [ pdf ]
  - UniversalCompModel [ pdf | ppt ]
- Examples (PDF/PowerPoint slides)
  - Backtracking [ pdf | ppt ]
  - ChooseForall [ pdf | ppt ]
  - Clock [ pdf | ppt ]
  - Consensus [ pdf | ppt ]
  - Conway [ pdf | ppt ]
  - DaemonGame [ pdf | ppt ]
  - DiningPhilosophers [ pdf | ppt ]
  - EchoAlgorithm [ pdf | ppt ]
  - LeaderElection [ pdf | ppt ]
  - Lift [ pdf | ppt ]
  - LinkedList [ pdf | ppt ]
  - LoadBalance [ pdf | ppt ]
  - MasterSlave [ pdf | ppt ]
  - MultipleReadsOneWrite [ pdf | ppt ]
  - PhaseSynchronization [ pdf | ppt ]
  - ShortestPath [ pdf | ppt ]
  - SortingSampling [ pdf | ppt ]
  - SpecCPipe [ pdf | ppt ]
  - Stack [ pdf | ppt ]
  - Switch [ pdf | ppt ]
  - TuringMachine [ pdf | ppt ]
- Exercises (PDF/PowerPoint slides)
  - ExerStms [ pdf | ppt ]
  - GroundModelsSimpleExls [ pdf | ppt ]

### Links

AsmBook Website (containing updates and additional material)
Abstract State Machines Archive

Robert Stärk, ETH Zürich, January 2003