KORSO: Methods, Languages, and Tools for the Construction of Correct Software: Final Report

Front Cover
Manfred Broy, Stefan Jähnichen
Springer Science & Business Media, Nov 8, 1995 - Computers - 458 pages
This book constitutes the final report of the work carried out in the project KORSO ("Korrekte Software") funded by the German Federal Ministry for Research and Technology. KORSO is an evolutionary, prototype-oriented project aimed at improving the theoretical foundations of quality-driven software engineering and at implementing known techniques for applications of practical relevance.
The 21 strictly refereed papers presented are organized in five sections on methods for correctness, languages, development systems and logical frameworks, tools, and case studies. In addition, the preface and introductory paper give valuable background information and a concise state-of-the-art overview.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

From Experiments to Applications
1
Methods for Correctness
25
A Method for the Development of Correct Software
27
Realizing Sets by Hash Tables
58
Event Automata as a Generic Model of Reactive Systems
74
On ObjectOriented Design and Verification
92
Design of Modular Software Systems with Reuse
112
A Case Study in SPECTRUM
128
Construction and Deduction Methods for the Formal Development of Software
239
Experiences with a Specification Environment
255
Tools
268
Towards Correct Efficient and Reusable Transformational Developments
270
The Verification System Tatzelwurm
285
SEDUCT A Proof Compiler for First Order Logic
299
TRAVERDI Transformation and Verification of Distributed Systems
317
The KivApproach to Software Verification
339

Languages
148
KORSO Reference Languages Concepts and Application Domains
150
How to Cope with the Spectrum of SPECTRUM
173
A FineGrain Sort Discipline and its Application to Formal Program Construction
190
TROLL light The Language and Its Development Environment
205
Development Systems and Logical Frameworks
221
Formalization of Algebraic Specification in the Development Language Deva
223
Case Studies
369
Three Selected Case Studies in Verification
371
A Comparative Study in Formal Specification and Verification
388
A Medical Information System
417
Authors Addresses
446
Copyright

Common terms and phrases

Popular passages

Page 366 - YM Landis, An algorithm for the organization of information. Soviet Math. Dokl. 3 (1962) 1259-1262.

Bibliographic information