model checking

file

Visible to the public Credible Autocoding and Verification of Embedded Software (CrAVES)

Submitted by lememta on Mon, 02/01/2016 - 5:36am. Contributors:

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.

file

Visible to the public Methodologies for Engineering with Plug-and-Learn Components: Synthesis and Analysis Across Abstraction Layers

Submitted by John Gallagher on Mon, 02/01/2016 - 5:36am. Contributors:

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).