Description

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.

References

1. Distributed code generation from Lotos NT specifications (Digital version available here)

Additional Resources

1. The paper