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

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