Development of a Provably Correct Codegenerator for Hierarchic Statemachines

Norbert Schirmer

Master Thesis (2001)


In this diploma thesis a provably correct codegenerator for hierarchic statemachines is developed. Hierarchic statemachines are a prominent formalism to describe the behaviour of finite state systems. They are often used to model safety critical applications for embedded systems. Thus it is crucial to ensure the correctness of the generated code. The codegenerator described in this thesis has a high degree of reliability, because it is formally specified and verified inside the theorem prover Coq. The combined approach to specify, program and verify the codegenerator in a single machine-supported process is described and evaluated.

 Online Copy

Available as compressed PDF-File (585KB)

 BibTeX Entry

  author = "Norbert Schirmer",
  title  = "Development of a Provably Correct Codegenerator for Hierarchic Statemachines",
  school = {Universit\"at Ulm},
  year   = 2001,

Norbert Schirmer
Last modified: Wed Oct 31 16:56:06 MET 2001