Abstract: The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which model-level control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems.

Abstract: Cyber-Physical Systems (CPS) that modify themselves to improve performance or repair damage often recast the modular relationships among system components that enable Verification and Validation (V&V). We focus on in-flight control adaptation of damaged Flapping-Wing Micro Air Vehicles (FW-MAV).