Safety-critical systems include systems such as air-traffic control, 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. The project will involve developing a framework for verifying safety-critical cyber-physical systems, incorporating failure analysis of the hardware components. The framework will build on an existing model checking approach which includes modelling component faults as views of a specification. One of the goals of the project will be to identify ways of using rely/guarantee reasoning for modelling different types of faults, such as omission and commission faults, in order to automate failure analyses such as Failure Modes and Effects Analysis. The rely/guarantee approach will need to be extended for handling real-time behaviour and probabilistic properties. The project would ideally include the application of the technique to a large case-study, such as an air-traffic control system.
The project scope is quite flexible and applicants are welcome to discuss related project ideas.
A background in computer science, software engineering, mathematics, systems engineering or related fields is essential. Familiarity with formal methods and logic is desirable. Experience with program reasoning approaches, temporal logic or model checking would be an advantage but is not essential. The applicant will need to meet the ANU requirements for PhD admission (see https://cecc.anu.edu.au/study/phd-mphil).
The starting date is flexible but preferably before mid 2024. Later starting dates may be negotiated.
If you’re interested in this project, contact Dr. Nisansala Yatapanage. Applications will be accepted until the position is filled, but apply by Jan 19th to receive full consideration.