|Sandeep Shukla wants to boost the productivity of embedded system designers by developing formal analysis and validation methods/tools that allow engineers to quickly and accurately choose the optimal strategies for balancing system performance and resource usage.
He recently won a prestigious $400,000 National Science Foundation (NSF) Faculty Early Career Development Award to develop the formal methods and to create design automation methodologies and tools based on these formal methods, to optimally design embedded systems with mathematically provable quality of service guarantees.
30x More Embedded Systems Than PCs
According to Shukla, more than 30 times as many computers are used in embedded systems as in general-purpose personal computers. As embedded systems become more mobile and widespread including use in the human body, in geological and space sensors, and in weapons systems power, real-time communications, system availability, reliability, and other Quality of Service (QoS) issues grow more numerous and critical.
This growth makes design increasingly difficult, according to Shukla. Today the design options are huge and there is too much interaction between devices, too much uncertainty that must be modeled into a system.
Hardware/Software Design Options
For example, if we want to reduce power consumption by a system, we can do that in the hardware, or we can work at the operating system level by using certain programmatic techniques to make devices in the system require less power. These decisions at the hardware/software interface are often done in an ad hoc manner today, and are validated by expensive and time-consuming simulations, he said. Such decisions are difficult due to the amount of uncertainty in the system usage patterns, and device characteristics, he added.
Probabilistic Models & Game Theory
He is interested in developing mathematical techniques based on game theoretic models and probabilistic model checking. The advantages of probabilistic model checking are inherently exhaustive in searching among all possible scenarios, and quick determination of potentially catastrophic corner casesthose scenarios that come up under extraordinary conditions. He expects to use game theory to help coordinate multiple competing strategies.
Shukla plans to develop tools that will help designers choose between competing strategies and verify the probabilistic guarantees of the performance of the strategies. Im developing formal methods to design systems where I can provide mathematical tools that ensure certain conditions are met and the standards can be guaranteed with a high probability, he said.
Improving CAD Tools
He has been collaborating with researchers at the University of Birmingham, UK, the developers of PRISM, a publicly available model-checker and hopes to enhance their offering with his results.
Embedded Systems Specialization
In addition to the research and development, Shukla plans to develop an embedded systems specialization at Tech for computer engineers. There is a dire shortage of engineers experienced in designing and implementing embedded systems and only a handful of universities currently have specialization programs, he said.
For more information, please visit the website for the FERMAT Lab (Formal Engineering Research with Modeling, Abstraction, and Transformation). http://filebox.vt.edu/users/shukla/FERMAT.htm