Presentation
From static analyses to runtime verification of cyber-physical systems
DescriptionModern autonomous systems, known as Cyber-Physical Systems (CPSs), contain thousands of lines of source code running on hundreds of Electronic Control Units (ECUs). Traditional formal verification methods may miss runtime faults. This paper proposes a temporal monitoring logic to derive a runtime verification method for CPSs analyzed with a dataflow Model of Computation and Communication (MoCC). The runtime verification method developed here verifies that properties derived from static analyses remain valid at runtime. This contribution is illustrated by the formalization of some runtime properties on a partial dataflow model of the Ingenuity helicopter.
Event Type
Work-in-Progress Poster
TimeWednesday, July 12th6:00pm - 7:00pm PDT
LocationLevel 2 Lobby
AI
Autonomous Systems
Cloud
Design
EDA
Embedded Systems
RISC-V
Security