Timed Monitorability in Theory and Practice

We will investigate a decision procedure for the monitorability of timed-properties of software controlled systems. A property defines a behaviour that a system is expected to exhibit, or in some cases, to not exhibit. In Runtime Verification, a property is monitorable if it is possible to construct a monitor that can detect the system’s conformance to the property in finite time.

Real-time software is crucial to the operation of nearly all of today’s safety-critical systems. Aircraft, spacecraft, power plants, cars, trucks, radiology machines, pacemakers, and many more devices run software that must strictly account for timing. Monitoring these devices for correct operation is one way that engineers can increase confidence that they are not failing at their critical tasks, but monitoring is only useful if the properties being monitored are monitorable. If it is not possible to determine in finite time that a property is satisfied or violated, then monitoring it is pointless.

This project will find classes of monitorable timed properties and introduce algorithms and tools for determining them. This program will bring opportunities for additional collaborations with Canadian industry interested in timed monitoring and provide visibility for Canadian research in the wider world of theoretical computer science.

Faculty Supervisor:

Sean Kauffman

Student:

Partner:

Aalborg University

Discipline:

Computer science

Sector:

Aerospace; Automotive; Cyber Security

University:

Queen's University

Program: