Title: “Monitoring UAV flights with Copilot”
Presenter: Frank Dedden, NIA Visitor (Utrecht University)
Date: Friday, November 30, 2018
Time: 11AM-Noon
Location: NASA/LaRC/ Building 1230, Room 264A
Sponsor: Alwyn Goodloe, NASA/LaRC
Abstract: Ultra-critical systems require high level assurances that cannot always be guaranteed at compile time. The use of runtime verification (RV) allows us to monitor these systems at runtime, detect property violations early, and limit the potential consequences of these errors. Monitors for highly-critical embedded systems can be implemented directly in C, but this results in low-level code that is error prone, hard to understand and difficult to maintain. In this presentation we present Copilot, a high-level runtime verification framework for ultra-critical embedded systems. Runtime monitors are based on data streams and can be defined using a high-level Embedded Domain Specific Language (EDSL) with support for a variety of Temporal Logics (TL). Our language is strongly typed and includes advanced notions like structs and arrays, which results in declarative high-level specifications that are easier to understand than traditional counterparts. Copilot generates C code with static memory requirements for these high-level specifications, which can be compiled to run on embedded hardware.