research reported here, the ASM (Abstract State Machines) method has been used
to develop a practically viable method for defining, in a rigorous but concise
way, satisfactory ground models for software requirements. Such ground models
can be refined in a controllable way to executable code. 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. See the
papers on the ASM Ground
Model Method, the modeling constituent of the Asm Method:
- provides the possibility to make the
ground model into an EXECUTABLE MODEL which can be used for high-level
validation and experimentation. For an open source execution environment
- 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).
See the ASM Refinement
paper, an introduction into the refinement constituent of the Asm Method.
- 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. This makes the ASM method suitable in connection with the VerifiedSoftware Challenge.
For a systematic exposition of the
ASM systems engineering method in its full generality see the AsmBook.
The following papers pioneered some characteristic
and industrial applications of the method to build, analyze and refine ground
models for control systems and web services.
- Workflows, Web Services, Business
Processes, Interaction Patterns: An ASM-Based Approach. Survey. Final version to appear in
2008 - International Conference on ASM, B and Z. Springer LNCS 5238.
- WEB SERVICES MEDIATOR model (also known as
Provider ground model). Final version to appear in Proc.
ICFEM’05, Springer LNCS 3785, 2005, pp. 81-95. A refinement to a
high-level model for Semantic Web
Service Discovery is going to appear in International Journal of
Business Process Integration and Management (IJBPIM) Vol.4, Issue 1,
December 2006. ISSN (Online): 1741-8771, ISSN (Print): 1741-8763
- SERVICE INTERACTION PATTERNS (Draft
Final version to appear in Proc. ICFEM’05, Springer LNCS 3785
(2005), pp. 5-35, ISSN
- 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
model, 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 also Chapter 5.1 of 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,
of the solutions).
Using ASMs (see abstract),
starting from a user inspectable ground model
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)
- FALKO, the
first industrial reengineering
application of the Ground Model Method. See the Falko
experience report.pdf. For a later similar reengineering application
of the ASM Ground Model Method at Microsoft Research see the debugger