Course Material & Suggested Readings (E.Börger)
The goal of the course is to teach a practical technique
for disciplined rigorous system engineering. For this purpose, Abstract
State Machines (ASMs) are used as scientifically well-founded and industrially viable
basis for the design and analysis of complex systems. The analysis covers both
verification and validation, using mathematical reasoning (possibly
theorem-prover-verified or model-checked) or experimental simulation (by
running the executable models). The method, which has been applied successfully
to programming languages, protocols, embedded systems, architectures,
requirements capture, etc., is illustrated for defining, in a rigorous but
concise way, satisfactory ground models for software requirements, and
for refining such ground models in a controllable way to executable
code. The student is guided to understand how the operational and abstract
character of ASMs
- makes the FAITHFULNESS OF THE
GROUND MODEL with respect to the informally given requirements checkable
for the application domain expert (falsifiable in the Popperian sense),
namely by direct inspection,
- provides the possibility to
make the ground model into an EXECUTABLE MODEL which can be used for
high-level validation and experimentation,
- supports, by stepwise
refinements, LINKing the high-level definition in a transparent way TO its
IMPLEMENTATION, where each refinement step reflects design decisions one
wants do be documented for future reference (extensions, modifications,
maintenance),
- simplifies
the system analysis, necessary for the justification of the design
correctness, by offering a RIGOROUS framework for the ANALYSIS OF RUN TIME
PROPERTIES at the appropriate level of abstraction
The
book is used to illustrate an extensive case study in applying practical
rigorous methods to the design and the analysis of a real-life software system.
The book provides a structured and high-level description, together with a
mathematical and an experimental analysis, of Java and of the Java Virtual
Machine (JVM), including the standard compilation of Java programs to JVM code
and the security critical bytecode verifier component of the JVM. The following
fundamental property of JVM verification and execution of compiled Java
programs is analysed and proved:
Under
explicitly stated conditions, any well-formed and well-typed Java program, when
correctly compiled, passes the verifier and is executed on the
JVM. It executes without violating any run-time checks, and is correct with
respect to the expected behavior as defined by the Java machine.
The description is structured
into modules, and its abstract character implies that it is truly platform and
programming language independent. It comes with a natural refinement to
executable machines on which code can be tested. The method we develop for this
purpose can be applied to other virtual machines and to other programming
languages as well.
Lecture Slides and Papers
Copyright Notice. The work below
is copyright by Egon Börger, and
other authors, who reserve all rights to their work. Fair personal use
of the material is welcome, including using and making the material available
for lecturing. In doing this, the source and the authors should be mentioned,
when passing off the material this copyright notice should be added. In
particular, it would not be fair to pass off any material made publicly
available here as your own work.
Slides for lecturers, covering
most of the themes mentioned below, are available electronically via the
AsmBook web site.
- High Level System Design
and Analysis using Abstract State Machines (A non-technical introduction
explaining the ASM method, surveying its major applications prior to 1999,
and comparing it to other major modelling approaches in the literature. Abstract). A predecessor of
this paper from 1995 is Why
Use Evolving Algebras in Hardware and Software Engineering where the basic methodological and
epistemological aspects of the concept of ASMs (then called evolving
algebras) are explained (WhyAsm95). The role of ASMs in a more general
perspective of Modeling Discrete Systems is surveyed in a handbook
article that is going to appear in Encyclopedia of Physical Sciences and
Technology, Academic Press 2001, a draft
version is available in Microsoft word format.
- The ASM Method for System Design and Analysis. A
Tutorial Introduction (In: Springer
LNAI 3717 (2005), 264-283) with lecture
slides
- Definition of syntax and
semantics of ASMs. A textbook
form of this definition for sequential ASMs can be found in Chapter 2
of Jbook. An updated textbook
definition is found in the AsmBook.
- Composition and Submachine
Concepts for Sequential ASMs (A definition of composition
and structuring concepts which reflect frequently used refinements of
ASMs, in particular SEQ, ITERATE and parameterized (recursive)
SUBMACHINEs.) Abstract
and ComposingASMs.ps
or ComposingASMs.pdf.
See also Chapter 4.1 of the AsmBook.
- Design for Reuse via
Structuring Techniques for ASMs (An application of the above mentioned
concepts for structuring ASMs, namely to the definition of the
architecture of the Java
Virtual Machine. JVMComposition.pdf
or JVMComposition.ps)
- LIGHT CONTROL case study, proposed for a comparison of
requirements engineering methods to a Dagstuhl
seminar on Requirements Capture/Documentation/Validation, organized by Egon Boerger (Universita di Pisa), Dave Parnas
(McMaster University, CAN), Baerbel Hoerger (Daimler-Chrysler, Ulm), and
Dieter Rombach (Universitaet Kaiserslautern) from June 14-18, 1999. Some
problem solutions have been selected for publication in a special issue of the Journal of
Universal Computer Science. This includes an ASM
ground model, which has been made executable in AsmGofer by J.
Schmid. See also Chapter 6.2 of the AsmBook.
- PRODUCTION CELL case study, proposed
for a competition and comparison of formal methods for software
development by C. Lewerentz and T. Lindner in Springer LNCS 891. From a
user inspectable ASM ground model
(or ProdCell.pdf,
published in JUCS3.5, 1997),
going through an intermediate refined ASM model, Luca Mearelli has derived
C++ code which
has been extensively and successfully validated controlling the simulator
made available for the competition by FZI Karlsruhe. The required safety
and liveness properties, which we prove by standard mathematical arguments
to hold in the ASM ground model, have been successfully model checked by
Kirsten Winter (see abstract).
See also Chapter 5.1 of the AsmBook.
- STEAM BOILER case study,
proposed for an international competition to
a Dagstuhl seminar on formal program specification and development
methods. The informal problem
formulation by Jean-Raymond Abrial, an executable steam boiler simulator
developed by Anne Loetzbeyer, and 23 problem solutions, using different
methods, are contained in the CD accompanying Springer LLNCS 1165 Formal
Methods for Industrial Applications (see flyer, contents,
preface,
survey
of the solutions).
Using ASMs (see abstract),
starting from a user inspectable ground model.ps
(or SteamBoiler.pdf)
which formalizes the informally expressed requirements, and going through
intermediate refined models which reflect further design decisions, C++ code
has been developed and validated by Igor Durdanovic (and is available for
further testing or experimentation on the CD ROM accompanying the Springer
LLNCS vol. 1165)
- Two industrial experience
reports on software engineering applications of the ASM method under
industrial constraints, published in ASM’2000 Springer LNCS 1912
- Report on a Practical
Application of ASMs in Software Design (Design of a central component in
a software system for the construction and validation of timetables for
railway systems: Falko.pdf
project at Siemens Corporate Research, Munich. Abstract)
- See www.eecs.umich.edu/gasm for
further papers published on ASMs and their applications, covering
high-level design and analysis of real-life programming languages and
their implementations on virtual or real machines (e.g. Java/JVM, C, VHDL,
SDL), of protocols (e.g. Kerberos), embedded system control programs,
architectures (RISC processors, PVM, APE, ASIC components), requirements
capture, etc.
.