Keywords: model checking, timed automata, process algebra, computation tree logic, compilation
Units: 24 units
We designed a new programming language called, Fiducia to make embedded system applications correct-by-construct. We are implementing the language on top of Microkit, which delegates the calls to the seL4 microkernel. In this task, we aim to generate a formal model on timed automata (supported in the classical model checker Uppaal) from arbitrary Fiducia program and automatically verify important system level properties such as deadlock freeness, fairness etc.
The tasks includes the following:
- Develop a transpiler that translates a compiled Fiducia program to the timed automata representation in Uppaal;
- Implement a property specification language (reusing query language in Uppaal or an auto-specification using AI) and translates it to the CTL-based query language in Uppaal;
- Integrate the pipeline into Fiducia tool chain and develop user-friendly interfaces (command-line options are fine);
- Case study on practical embedded system applications and performance tuning.
Bonus:
- Prove the translation from Fiducia program to Timed Automata in Uppaal is valid;
- Research on keeping the state space small and verifiable.
Benefits: Student will be engaged in build practical tools for model checking real-world applications, sharpening their software development skills. The student would also have the chance being exposed to system programming (in Rust mainly), OS/microkernels, hardware.
Student who has:
- Strong foundation in formal methods and computer systems.
- Good programming skills (Rust preferred).
- Good knowledge in system programming, computer architecture. Activity