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.
-
INDEX:
- The index file for the FTP archive, containing BibTeX data for the documents.
-
Burghard v. Karger:
- Publications and reports by Burghard v. Karger
-
COORD JB 7/1:
- 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 procos@informatik.uni-kiel.de 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 (mf@informatik.uni-kiel.de)