Portal de Periódicos da CAPES

A method for the development of correct software

1995; Springer Science+Business Media; Linguagem: Inglês

10.1007/bfb0015454

1611-3349

Peter Pepper, Martin Wirsing, Ralph Betschko, Manfred Broy, Sabine Dick, Klaus Didrich, Joachim Faulhaber, Wolfgang Grieskamp, Heinrich Hußmann, Michael Mehlich, Wolfgang Reif, Martin K. Beyer, Stefan Gastinger, Maritta Heisel, Friedrich von Henke, Junbo Liu, Bernd Krieg-Brückner, Thomas Santen, Gerhard Schellhorn, Oscar Slotosch, Kurt H. Stenzel, Martin Strecker, N. Vlachantonis, Burkhart Wolff,

Embedded Systems Design Techniques

In requirements engineering domain modeling with formal specifications is integrated with informal and pre-formal approaches for the construction of a formal requirements specification of the "functional" properties of the required system. The specifications are used in the modeling and analysis parts of the requirement process and provide means for validation, including early prototyping and theorem-proving.An evolutionary process model is proposed for system design and program development, whereby the correctness of all development steps is checked by suitable verification tools. The model centers around a development graph which consists of units, e.g. formal specifications, proofs, and programs, and relations between these units. There are three kinds of relations: syntactic relations, semantic relations, and modifications. In each development step units are either created, transformed, or modified.Program and system development are understood as the development of specifications from the requirement specification to a constructive specification which can then be directly transformed into a program. Main features of the approach are modularity, compositionality, and reusability of specifications, programs, and proofs.