Description: Developing software for large-scale embedded systems and systems interacting with an external environment
Primary researchers: Mu Sun, Ajay Tirumala
Components, esp. in embedded and real-time systems, to function correctly or at a desired level of performance, must satisfy certain formally unexpressed yet necessary conditions. These conditions are termed as assumptions. This must be done in addition to the components’ compliance with functional interfaces exposed. Often, the assumptions are embedded in the documentation or the component’s code. Interestingly, many of the assumptions can be encoded in a machine-checkable format, but the current software engineering practices do not provide a clean method to do so.
The goals of this project are to:
- Provide a framework to encode assumptions in a machine checkable format.
- Provide a grammar for disparate component developers to encode assumptions (and provide guarantees) in a standard format.
- Provide a vocabulary for the properties of an assumption.
- Enable composition of assumptions, when systems are built from smaller sub-systems.
- Automatically validate a relevant subset of assumptions during system evolution.
- Vertical assumptions tracking : Track the assumptions across the software life-cycle.
A. Tirumala, T.Crenshaw and others. Prevention of failures arising from assumptions on software components in real-time systems. ACM SIGBED Review. July, 2005.
L.Gu, D.Jia, P.Vicaire, T.Yan, L.Luo, A.Tirumala and others.Lightweight detection and classification for wireless sensor networks in realistic environments. ACM Sensys. 2005.