Seminar Series 2015 - André Pedro

Seminar Series 2015 - André Pedro

Towards a Case Study on Runtime Verification of Lightweight Avionic Controllers using RMTLD3
25, Nov, 2015 11:30-12:30 (1 hour)
CISTER, Porto, Portugal

Current lightweight autopilot frameworks such as Ardupilot and PX4 lack the application of formal verification methods, and therefore they are unsafe in terms of memory-space and execution-time isolation. Focusing on time isolation and on the inherent real-time constraints required for these systems, we present a case study that address the specification of duration properties for runtime verification in order to increase the dependability of avionic controller systems.
We employ the \acl{RMTLD3} as the formalism to specify duration formulas that are able to ensure time isolation between execution units as well as the adaptability that those systems require to avoid possible overloads and/or faults introduced by fault-tolerant transient overload mechanisms.


PDF Presentation (580KB)

CISTER's main roles:
André Pedro

S101 Auditorium/Seminar Room
1st Floor

Event-related Photos and Videos