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.
Requirements
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.
Contact
If you’re interested in this project, contact Dr. Nisansala Yatapanage. Scholarships are available for PhD students.