Modeling with Abstract State Machines: A support for accurate system design and analysis.
Egon Börger · Modellierung · 2004
We survey applications of the Abstract State Machines (ASM) method for high-level system modeling and for well-documented refinements of abstract models to code. The outstanding feature of the ASM method is that within a single, precise yet simple, conceptual framework it naturally supports and uniformly links the major activities which occur during the typical software life cycle, namely: • requirements capture by constructing satisfactory ground models, i.e. accurate highlevel system blueprints, serving as precise contract and formulated in a language which is understood by all stakeholders (see [Bo03a]), • detailed design by stepwise refinement, bridging the gap between specification and code design by piecemeal, systematically documented detailing of abstract models down to executable code (see [Bo03b]), • validation of models by their simulation, based upon the notion of ASM run and supported by numerous tools to execute ASMs (ASM Workbench [De01], AsmGofer [Sc], C-based XASM [AK01], .NET-executable AsmL engine [Fo01]), • verification of model properties by proof techniques, also tool supported, e.g. by KIV [SA97] or PVS [Do98, GR00] or model checkers [Wi97, DW00, GTW03], • documentation for inspection, reuse and maintenance by providing, through the intermediate models and their analysis, explicit descriptions of the software structure and of the major design decisions. The key to the practicability of ASMs also under industrial constraints is to be found in the simple and intuitive way in which ASMs support defining most general Virtual Machines (VMs) and their refinements to lower levels of abstraction. ASMs naturally extend Finite State Machines by allowing a) states with arbitrarily complex or abstract data structures and b) runs with transitions where multiple components act either simultaneously (synchronous parallellism) or asynchronously (like globally asynchronous, locally synchronous Codesign-FSMs). The flexible ASM refinement notion provides a uniform conceptual framework for effectively relating different system views and aspects, in both design and analysis, filling a gap in the UML framework. The general yet frugal character of the ASM language, namely for a rigorous form of pseudo-code over abstract data, is the source for the flexibility in modeling and analysis which has been experienced in such different areas as: • industrial standardization projects: models for the ISO-Prolog standard [BD90], the ECMA standard for C# [BFGS04], the IEEE-VHDL93 standard [BGM94], the ITUT standard for SDL-2000 [GGP03], • programmming languages: definition and analysis of the semantics and the implementation for the major real-life programmming languages, e.g. SystemC [MRR03], Java and its implementation on the Java Virtual Machine [SSB01], domain-specific languages used at the Union Bank of Switzerland [KST98], etc. • architectural design: verification (e.g. of pipelining schemes [BM97] or of VHDLbased hardware design at Siemens [Sc02, Ch.2]), architecture and compiler coexploration [Te01, TWFT00], • reengineering and design of industrial control systems: software projects at Siemens related to railway [BBC96, BPS00] and mobile telephony network components [CP02], debugger specification at Microsoft [BBG00], • protocols: for authentication, cryptography, cache-coherence, routing-layers for distributed mobile ad hoc networks, group-membership etc., focussed on verification, • verification of compilation schemes and compiler back-ends [BR95, BD96, DGVZ98, SSB01], • modeling e-commerce [AVFY98] and web services [FGV04], • simulation and testing: fire detection system in coal mines [BCF96], simulation of railway scenarios at Siemens [BPS00], implementation of behavioral interface specifications on the .NET platform and conformence test of COM components at Microsoft [BS02], compiler testing [KKP03], test case generation [GR03]. The AsmBook [BS03] introduces into the ASM method and illustrates it by textbook examples, which are extracted from real-life case studies and industrial applications. Additional material, including slide decks for lecturers, can be downloaded from the AsmBook website www.di.unipi.it/AsmBook/.