Master’s thesis
In Focus, the interface behavior of a system is represented by relations on data streams. Systems are composed via parallel composition including feedback loops. Interface specifications are formulas over the input and output streams. The starting point of this work is a rigorous mathematical description of a calculus for proving that systems satsfy their specification.
The aim of the thesis is to use the theorem prover Isabelle to
- formalize the calculus relating systems and their specifications and
- show soundness and completeness of the calculus in Isabelle based on a given hand written proof.
Prerequisites:
Familiarity with Isabelle/HOL
Supervisors:
Prof. Manfred Broy
Prof. Tobias Nipkow