In this paper we show how to integrate the use of Gurevich s Abstract State Machines (ASMs) into a complete software development life cycle. We present a structured software engineering method which allows the software engineer to control efficiently the modular development and the maintenance of well documented, formally inspectable and smoothly modifiable code out of rigorous ASM models for requirement specifications. We show that the code properties of interest (like correctness, safety, liveness and performance conditions) can be proved at high levels of abstraction by traditional and reusable mathematical arguments which-where needed-can be computer verified. We also show that the proposed method is appropriate for dealing in a rigorous but transparent manner with hardware-software co-design aspects of system development. The approach is illustrated by developing a C ++ program for the production cell control problem posed in [Lewerentz, Lindner 95]. The program has been validated by extensive experimentation with the FZI production cell simulator in Karlsruhe and has been submitted for inspection to the Dagstuhl seminar on "Practical Methods for Code Documentation and Inspection" (May 1997).

Programming Techniques, Requirement Specification, Stepwise Refinement, Code Documentation, Code Inspection, Program Verification, Model Checking, Abstract State Machines.