GGrantIndex
← Search

CSR---EHS: SHIM: Developing Embedded Systems with Deterministic Concurrency

$240,000FY2006CSENSF

Columbia University, New York NY

Investigators

Abstract

This project is creating the SHIM (software/hardware integration medium) development environment for the software in next-generation embedded systems. SHIM will improve designer productivity by making it easier to design correct systems and will facilitate architectural exploration by providing software synthesis. The SHIM model of computation provides deterministic concurrency with reliable communication, simplifying validation because behavior is reproducible. Based on asynchronous concurrent processes that communicate through rendezvous channels, SHIM can handle control, multi- and variable-rate dataflow, and data-dependent decisions. The SHIM language will give designers a correct-by-construction way to describe concurrent systems. Based on a formal semantics, SHIM guarantees systems comply with the model, something that would be difficult to ensure by adding a library to an existing language. An efficient simulator for SHIM will allow software to be simulated before hardware is available. Because of its determinism, SHIM guarantees fidelity between simulated behavior and the final implementation. A software synthesis system will generate C that works within existing environments such as real-time operating systems. The goals of this are configurability, (e.g., providing control over what is implemented as an interrupt routine) performance, and size optimization. A formal analysis tool will statically predict deadlocks, predict performance bottlenecks, and identify other design problems. Since SHIM is finite-state and fairly high level, formal analysis of SHIM systems is practical. Like any programming system, developers need libraries to use SHIM most efficiently. Facilitating such libraries will be a major focus of the language design; such libraries will be created as part of this project.

View original record on NSF Award Search →