Provably correct systems

  • Jifeng He
  • , C. A.R. Hoare
  • , Martin Fräinzle
  • , Markus Müller-Olm
  • , Ernst Rüdiger Olderog
  • , Michael Schenke
  • , Michael R. Hansen
  • , Anders P. Ravn
  • , Hans Rischel

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

33 Scopus citations

Abstract

The goal of the Provably Correct Systems project (ProCoS) is to develop a mathematical basis for development of embedded, realtime, computer systems. This survey paper introduces the specification languages and verification techniques for four levels of development: Requirements definition and control design; Transformation to a systems architecture with program designs and their transformation to programs; Compilation of real-time programs to conventional processors, and Compilation of programs to hardware.

Original languageEnglish
Title of host publicationFormal Techniques in Real-Time and Fault-Tolerant Systems - 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems - ProCoS, Proceedings
EditorsHans Langmaack, Willem-Paul de Roever, Jan Vytopil, Jan Vytopil
PublisherSpringer Verlag
Pages288-335
Number of pages48
ISBN (Print)9783540584681
DOIs
StatePublished - 1994
Externally publishedYes
Event3rd International Symposium on Formal Techniques in Real Time and Fault Tolerance Organized Jointly with Working Group Provably Correct Systems, ProCoS 1994 - Lubeck, Germany
Duration: 19 Sep 199423 Sep 1994

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume863 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Symposium on Formal Techniques in Real Time and Fault Tolerance Organized Jointly with Working Group Provably Correct Systems, ProCoS 1994
Country/TerritoryGermany
CityLubeck
Period19/09/9423/09/94

Fingerprint

Dive into the research topics of 'Provably correct systems'. Together they form a unique fingerprint.

Cite this