|title:||Code generation from Formal Specifications|
|keywords:||formal specifications, process algebra, code generation, automated verification and testing|
|topics:||Languages , Software Technology|
|committee:||Jaco van de Pol|
One design flow supported by formal methods is to first specify requirements (e.g. in temporal properties), construct a design model (e.g. in process algebra) and implement the system (e.g. in Java). Formal verification checks if the design satisfies all properties, and Model-based testing checks if the implementation conforms to the design.
A next step would be to automate the design steps. In particular, it should be possible to generate (parts of) the implementation from the design model. Typical research questions could be:
- what is the current state of the art in code generation from models
- how to generate code from a process algebra specification in general
- how to generate efficient code from a specification that follows some guidelines
Relevant courses: Verification Engineering, Compiler Construction, Concurrent and Distributed Programming.
- Distributed code generation from Lotos NT specifications (Digital version available here)