January 24, 2010 — Sandeep Shukla has received about $1.25 million in new grants for safety-critical software system design. The Office of the Secretary of Defense allocated $498,000 towards developing tools for the trustworthy composition of independently-developed embedded software components. Another $750,000 comes from the Air Force Labs at Rome, NY, for developing a way to synthesize concurrent software components on mission-critical embedded hardware platforms some of which may have multiple cores.
Generating Provably-Correct Software
Embedded software is used throughout modern safety-critical systems such as aircraft, vehicles, and weapons. However, most of this software is programmed manually, according to Shukla, and the available tools for automatic generation of embedded software, such as SCADE, are unable to take full advantage of multi-core processors. As such, he observes, bugs are a fact of life. He cites examples “such as the priority inversion in the Mars Rover software or Toyota, where subtle bugs escape even the best programmers and testers.”
Shukla and his team hope to solve this by developing models, methods, and algorithms that generate provably-correct and predictable embedded software.
Modeling computation and data flow
The team is also developing EmCodeSyn, a visual design tool that will allow developers to model embedded platforms. The model will use a formal specification notation called MRICDF (Multi-rate Instantaneous Channel Connected Data Flow Actors Network), which will specify the behavior of system components.
The aim of the EmCodeSyn too is to be able to guarantee the real-time behavior of a system, even when dealing with multiple concurrent threads of execution on two or more processor cores.
European avionics and automotive companies are already generating a significant amount of their control software using formal approaches, he says. The systems use a simple time-triggered composition model, however, which reduces efficiency.
MRICDF will use event-driven composition, but avoids some problems by describing processes as acting on a potentially infinite data flow, which, Shukla says, “makes specification of synchronization between concurrent activities within each component much easier.”
Cooperation with SUNY Albany
Shukla and his team are also working with researchers at the University at Albany, who will develop algorithms to extract theorems out of a set of formulas which is crucial in the process of automated code synthesis.