Description: Guaranteeing high-level architectural system properties
Primary Researchers: Sumant Kowshik

Embedded systems have proliferated into diverse and complex critical applications with stringent reliability and timeliness requirements. Guaranteeing reliability in the presence of increasing complexity of embedded systems have necessitated a multitude of architectural designs including integrated modular architectures and architectural designs for robustness by minimizing inter-component failure dependencies.

In the software development cycle, the system integration architect occupies a key position between the domain-specialist, designing the algorithms and the high-level logical design, and the individual software component developers. In essence, the system architect refines the logical design into concrete software components, while facilitating high-level properties such as timing, dependency management, and fault-tolerance. Existing tools for the systems architect include architecture description languages and model-checking tools, which specify and verify the architectural designs.

However, there is a gap between the architectural principles and the actual implementations developed by individual software developers. Low-level software errors, particularly in languages like C and C++, such as dangling pointer dereferences and array bounds errors, violate architectural properties. Recent research on debugging tools focus on best-effort approaches to detecting low-level programming errors. However, there is a need for tools that guarantee that high-level architectural properties are enforced in the component implementation. Failure to verify these properties in the actual code have caused two critical disasters in recent years, the satellite Phobos I and the Ariane V rocket.

The primary contribution of this work is to demonstrate the ability of static analysis tools to analyze individual components and guarantee high-level architectural properties in the system. In particular, we guarantee two key properties: (a) memory isolation and (b) safe exchange of data between components of different criticalities through run-time monitoring. Our solution combines language and library usage restrictions on the C language with a suite of compiler analyses to statically guarantee these properties. In doing so, we incur minimal (often zero) run-time overhead and do not require garbage collection, making our approach very attractive for embedded systems. We have examined different critical systems and embedded benchmarks and shown that our language restrictions are expressive enough for embedded systems while enabling statically guaranteeing high-level architectural properties. Finally, we show that we can verify other related architectural properties by extending our static analysis techniques.

Representative Publications

Sumant Kowshik, Grigore Rosu, and Lui Sha. Static Analysis to Enforce Safe Value Flow in Embedded Control Systems. Dependable Systems and Networks. , 2006.

Sumant Kowshik, Girish Baliga, Scott Graham, and Lui Sha.Co-design based Approach for Improving Robustness in Networked Control Systems. Dependable Systems and Networks. , 2005.


Related project: SafeCode