25, Nov, 2015 11:30-12:30 (1 hour)
CISTER, Porto, Portugal

ABSTRACT:
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.

EVENT PHOTOS:
At CISTER's Facebook page

DOWNLOAD:
PDF Presentation (580KB)

CISTER's main roles: