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


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.


Visible to the public Model-Based Design Overview

This presentation conceptualizes Model-Based Design of a cyber-physical system. Three stages of a system under design at various levels of detail are depicted. The designs are captured by models that have computational semantics based on the execution engine on a host platform. The implementation as generated code executes on a target platform. Because executable, the design can be explored, tested, and verified while at various levels of detail. This enables separation of concerns and so allows raising the level of abstraction in design.


Visible to the public New Developments in Model-Integrated Development of High-Confidence Software

Slides for NSF Kickoff Meeting: Science of Integration for CPS on 11/29/2010

by, Joe Porter, Graham Hemmingway, Nicholas Kottenstette, Harmon Nine, Chris vanBuskirk, Gabor Karsai and Janos Sztipanovits

Provides steps for:

1. Design of working control system for Quadrotor Aircraft using a Simulink Based Model

2. Software design using the ESMoL Modeling Language