Verification of Safety-critical Systems

Picture of Nisansala Yatapanage Nisansala Yatapanage

19 Feb 2023

Safety-critical systems include systems such as air-traffic control, medical, railway and industrial systems. The critical aspect of these systems is that if something goes wrong, human lives would be in danger. For this reason, it is essential to verify that the system has been designed to correctly handle events such as hardware components malfunctioning.

For this project, you will develop a verification technique for safety-critical systems that uses the rely/guarantee reasoning method. Rely/guarantee reasoning was originally designed for specifying and verifying concurrent systems. Safety-critical systems often contain concurrent components, so rely/guarantee is a natural choice for verifying these systems.


This project has a large scope and could be adapted to suit students of any level, from Bachelor research projects and Honours to PhD projects. You will need an ability to reason about logic and you should have completed a course on discrete mathematics including logic and set theory, e.g. MATH1005 at ANU. Familiarity with Hoare logic, such as covered in COMP1600, is preferred. PhD students should have a strong background in logic, formal methods, mathematics or related subjects.

Prior knowledge about safety-critical systems, verification and rely/guarantee reasoning is not required.


If you’re interested in this project, contact Dr. Nisansala Yatapanage. Scholarships are available for PhD students.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times arrow-up