- UNSW
- ...
- Student life
- Undergraduate research opportunities
- Advertised Taste of Research areas
- Formalising and verifying device controllers
- About us
-
Our schools
- Australian Graduate School of Engineering (AGSE)
- Biomedical Engineering
- Chemical Engineering
- Civil and Environmental Engineering
- Computer Science and Engineering
- Electrical Engineering and Telecommunications
- Mechanical and Manufacturing Engineering
- Minerals and Energy Resources Engineering
- Photovoltaic and Renewable Energy Engineering
- Study with us
- Student life
- Research & technology
- Alumni & industry
- Engage with us
- News & events
The TS group is working on verifying device drivers for LionsOS using the Pancake language. This work is inevitably dependent on a correct formalisation of the HW interface.
The project is to take an open-source Ethernet controller from the Verilog-Ethernet repository and, in close collaboration with the Pancake team formalise its software interface. Once successful, evaluate the use of the LUBIFIER tool for verifying the hardware implementation.
- Research environment
- Expected outcomes
- Supervisory team
- Reference material/links
The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.
- Formalisation of the Ethernet controller interface in HOL4;
- Report outlining the formalisation and experience with the use of verification tools.