ProCoS at the Christian-Albrechts-Universität Kiel

General information

The ESPRIT BRA project ProCoS II aims to improve dependability, reduce timescales and cut development costs of construction for embedded systems, particularly in real-time and safety-critical applications. It uses and develops the results of basic research into fundamental properties of interactive systems. It aims to provide a scientific basis for future standards of practice in the development of embedded systems, ensuring correctness of all stages in the development, from elicitation and analysis of requirements through design and implementation of programs down to compilation and execution on verified hardware.

Partners of the University of Kiel in this project are Oxford University (C.A.R. Hoare, coordinator), DTU Lyngby (A.P. Ravn) and Oldenburg University (E.-R. Olderog). The work in Kiel concentrates on correct compiler specification, development and implementation. Persons involved with this project in Kiel include Prof. Dr. Hans Langmaack (local coordinator), Dr. Bettina Buth, Dr. Karl-Heinz Buth, Dr. Martin Fränzle, Dr. Burghard von Karger, Dr. Markus Müller-Olm.

Selected documents produced for the ProCoS project at Kiel University

See also the README file for additional information.

The index file for the FTP archive, containing BibTeX data for the documents.
Burghard v. Karger:
Publications and reports by Burghard v. Karger
Provably Correct Systems - FTRTFT'94 Tutorial, Jonathan Bowen and C.A.R. Hoare and Michael R. Hansen and Anders P. Ravn and Hans Rischel and Ernst-Rüdiger Olderog and Michael Schenke and Martin Fränzle and Markus Müller-Olm and Jifeng He and and Zheng Jianping, School material, FTRTFT'94 Symposium, Lübeck, Germany, 19-23 September 1994. (102 pages)
DTH APR 21/1:
Developing Correct Systems, J. P. Bowen, M. Fränzle, E.-R. Olderog and A. P. Ravn, June 1993. Also appeared in the Proceedings of the 5th Euromicro Workshop on Real-Time Systems, IEEE Computer Society Press, 1993, 176-189.
Kiel BB 5/1:
Operation Refinement Proofs for VDM-like Specifications, Bettina Buth, February 1995.
Kiel KHB 3/1:
Simulation of SOS Definitions with Term Rewriting Systems, Karl-Heinz Buth, April 1994.
Kiel KHB 4/1:
Techniques for Modelling Structured Operational and Denotational Semantics Definitions with Term Rewriting Systems, Karl-Heinz Buth, August 1994 (193 pages).
Kiel KHB 5/1:
Automated Code Generator Verification Based on Algebraic Laws, Karl-Heinz Buth, September 1995 (21 pages).
Kiel MF 10/2:
Drift and Granularity of Time in Real-Time System Implementation, Martin Fränzle and Markus Müller-Olm, August 1993 (11 pages).
Kiel MF 11/3:
Proposal for a Programming Language Core for ProCoS II, Martin Fränzle and Burghard von Karger, August 1993.
Kiel MF 16/2:
Test preorder and refinement, Martin Fränzle, December 1994.
Kiel MF 17/3:
A Discrete Model of VLSI Dynamics in Hybrid Control Applications, Martin Fränzle, April 1995.
Kiel MF 18/1:
From Continuity to Discreteness - five views of embedded control hardware, Martin Fränzle, August 1995.
Kiel MMO 6/2:
On Translation of TimedPL and Capture of Machine Instruction Timing, Markus Müller-Olm, August 1993.
Kiel MMO 9/2:
A Process Language and its Model, Markus Müller-Olm, August 1994.
Kiel MMO 10/2:
A New Proposal for TimedPL's Semantics, Markus Müller-Olm, August 1994.
Kiel MMO 12/4:
Structuring Code Generator Correctness Proofs by Stepwise Abstracting the Machine Language's Semantics, Markus Müller-Olm, August 1995.
Kiel MMO 13/3:
The Concrete Syntax of TimedPL, Markus Müller-Olm, August 1995.
Kiel MMO 14/1:
A Short Description of the Prototype Compiler, Markus Müller-Olm, August 1995.
Kiel MMO 15/1:
Modular Compiler Verification (A Summary), Markus Müller-Olm, August 1995.
Kiel MMO 16/2:
Compiling the Gas Burner Case Study, Markus Müller-Olm, August 1995.
Kiel MMO 17/1:
An Exercise in Compiler Verification, Markus Müller-Olm, October 1995.

Contact for more information on ProCoS at Kiel.

Part of the ProCoS archive.

See also information on the city of Kiel (in German).

Martin Fränzle (