Algebraic foundations of systems specification

Authors

Publication date 18 August 1999

Algebraic foundations Systems specification

Collections of articles of miscellaneous specific interest (00B15) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Formal languages and automata (68Q45)

Review text

The articles of this volume will be reviewed individually. From the introduction: This volume provides a state-of-the-art report of the are a of algebraic specification. It consists of surveys of the major research topic s in the area and is authored by leading experts in the field. The production of this book was an activity of the IFIP Working Group 1.3 in cooperation with the ESPRIT Basic Research Working Group COMPASS. In recent years, IFIP WG1.3 has been organizing and supporting the Common Framework Initiative for Algebraic Specification, and Development (CoFI) that aims at the provision of a family of specification languages at different levels of software development with a widely accepted algebraic and logical basis. As a first step, the central language CASL has been designed for the specification of conventional software including requirement definition, design and architectural aspects. One may say that the presente d state-of the-art report provides the algebraic and logical foundations of the CoFI project. In more detail, this volume is organized in the following way. Bernot and Gaudel motivate the use of formal methods and -- in particular -- of algebraic specification techniques from a software engineering point of view in Chapter 1. The basic notions and notations of algebraic specifications centered around many-sorted algebras and equational calculus are recalled by Sannella an d Tarlecki in Chapter 2 while Cerioli, Mossakowski, and Reichel extend the foundational framework to a partial first-order logic in Chapter 3. The variety of al Sannella and Wirsing give an overview of the various proposed algebraic specification languages from the early candidates CLEAR and ACT ONE to the most recent attempt, the design of CASL as a standard specification language. Chapters 9 to 11 are concerned with term rewriting and proof theory as the foundations for evaluation and verification of algebraic specifications. In Chapter 9, Kirchner discusses various forms and aspects of term rewriting as a basis for interpreter semantics. As a major advantage of formal specification is the chance to guarantee correctness, theorem proving techniques and proof systems for algebraic specifications are extensively presented by Padawitz with respect to flat specifications in Chapter 10 and by Bidoit, Cengarle, and Hennicker with respect to structuring and refinement. The last three chapters deal with prominent applications domains. Ehrich relates algebraic specification with object orientation in Chapter 12 . Astesiano, Broy, and Reggio introduce the reader to the algebraic specification of concurrent systems in Chapter 13. Finally, Basin and Krieg-Brückner provide a formalization of the development process in Chapter 14. The main goal of this book is to disseminate fundamental knowledge about the area of algebraic specification and to expose the state of the art in a systematic way. The aim is to attract students, scientists, researchers and system developers interested in formal methods in general and algebraic specification in particular. Indexed articles: \textit{Gaudel, Marie-Claude; Bernot, Gilles}, The role of formal specifications, 1-12 [Zbl 0944.68525] \textit{Sannella, Donald; Tarlecki, Andrzej}, Algebraic preliminaries, 13-30 [Zbl 0945.68129] \textit{Cerioli, Maura; Mossakowski, Till; Reichel, Horst}, From total equational to partial first-order logic, 31-104 [Zbl 0949.03028] \textit{Tarlecki, Andrzej}, Institutions: An abstract framework for formal specifications, 105-130 [Zbl 0945.68130] \textit{Reichel, Horst}, Specification semantics, 131-158 [Zbl 0945.68131] \textit{Orejas, Fernando}, Structuring and modularity, 159-200 [Zbl 0945.68132] \textit{Ehrig, Hartmut; Kreowski, Hans-Jörg}, Refinement and implementation, 201-242 [Zbl 0953.68096] \textit{Sannella, Donald; Wirsing, Martin}, Specification languages, 243-272 [Zbl 0979.68555] \textit{Kirchner, Hélène}, Term rewriting, 273-320 [Zbl 0960.68087] \textit{Padawitz, Peter}, Proof in flat specifications, 321-384 [Zbl 0958.68109] \textit{Bidoit, Michel; Cengarle, María Victoria; Hennicker, Rolf}, Proof systems for structured specifications and their refinements, 385-433 [Zbl 0948.68118] \textit{Ehrich, Hans-Dieter}, Object specification, 435-465 [Zbl 0958.68108] \textit{Astesiano, Egidio; Broy, Manfred; Reggio, Gianna}, Algebraic specification of concurrent systems, 467-520 [Zbl 0973.68150] \textit{Basin, David; Krieg-Brückner, Bernd}, Formalization of the development process, 521-610 [Zbl 0958.68107]

Recommendations

Cited in

(23)

Describes a project that uses

Uses Software

CoFI

This page was built for publication: Algebraic foundations of systems specification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4255593)