ECE: Electrical & Computer Engineering
ECE News

Safety-critical embedded software: correct by construction?

Print Version

image of article

.pdf Print Version
76 KB

More Information

For more information, visit the The Virginia Tech’s Microelectromechanical Systems Laboratory (MEMS).


What do a Renault car and an AirBus 380 have in common? "Millions of lines of embedded software running in networked communication" is the reply from Sandeep Shukla, director of Virginia Tech's FERMAT lab. Safety-critical systems, such as those on cars and jets, are increasingly run by concurrent software systems reacting to a myriad sensor inputs.

The problem, he says, is verifying the correctness of an en­tire system func­tioning together. He is working with the Air Force Research Lab to generate software that is correct by construction for its specifications and can generate multiple sequential software components to work correctly across a network. They also may be multi-threaded, he says.


Shukla has been working with the French National Laboratory Institut National de Recherche en Informatique et en Automatic (IRISA) on a specification methodology called Polychrony, which allows one to specify the concurrent computations.

Based on Polychrony, the IRISA team and Shukla's FERMAT lab have previously proposed various methodologies for composing existing components to create new designs of systems-on-a-chip. For more information, visit