文章基本信息

标题：Integrating ASMs into the Software Development Life Cycle
本地全文：下载
作者：Egon Börger ; Luca Mearelli
期刊名称：Journal of Universal Computer Science
印刷版ISSN：0948-6968
出版年度：1997
卷号：3
期号：5
页码：603-665
出版社：Graz University of Technology and Know-Center
摘要：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).