Toward Designing Correct Concurrent Systems

Biological bugs can make people ill, or even endanger people's life. Similarly, logical bugs can make concurrent systems unreliable, or even fail. In today's concurrent system designs, finding and fixing logical bugs early is of the highest priority because it is very costly when bugs are found late in the design stage. Bugs left undetected in systems can cause huge losses to the economy and human society. The infamous examples include an error in the arithmetic unit of a Intel Pentinum processor which caused a loss of almost $500 million and an error in the flight control software of the on-board computer which caused the explosion of Ariane 5 rocket. The latest example is an error in AMD Barcelona Quad-core processors casues 9 months delay in product shipment, and huge market share loss. In the safety critical applications that can be found in nuclear power plants and airplane flight control systems, the correct operation of systems must be guaranteed at any cost.

For more examples of system flaws and their consequences, please see Software Horror Stories.

The following figure shows that the gap between design and verification capabilities is widening, and verification is becoming a serious bottleneck. This requires the development of more powerful verification technologies so that the system designs that can be manufactured can be also be effectively verified..
Harry Foster, Assertion-based Verification: Industry Myths to Realities (Invited Tutorial)}, CAV, 2008.

However, making sure complex systems work correctly is very difficult because both functional complexity and density of systems are growing exponentially, imposing unprecedented challenges on verification. Among various verification technologies, model checking, has some unique advantages.

It can find bugs hidden very deeply in a system. However, capabilities and robustness of model checking cannot keep up with the exponential growth of concurrent system complexity. This is the well known state explosion problem, which limits model checking to small designs. To effectively use model checking to large designs, it requires users to have deep understanding of the underlying verification algorithms and heuristics, thus limiting its widespread acceptance.

My research focus is to address the above difficulties by developing new methodologies and algorithms to make model checking scalable to large design. Therefore, system designers can focus on achieve their design goals effortlessly instead of worrying verification. The following are the several current projects being pursued in my research group.


Methodologies and Tools for Large Scale Real-Time Concurrent System Verification

In this research project, a model checker based on explicit graph representations, Plato, has been being developed for real-time asynchronous system verification. We have developed various compositional (modular) verification approaches that are able to handle asynchronous designs with very high complexity. Additionally, several state space reduction techniques have also been developed to control the complexity of the intermediate results during compositional verification process. These methods and techqniques are fully automated and completely transparent to the users. The following list shows the possible items that will further improve the capability of Plato and make it more general for other application domains.


Methods and Algorithms for Scalable Symbolic Model Checking

Both BDD and SAT solver based symbolic model checking approaches have worst case exponential complexity. In this project, we investigate methods and algorithms to make symbolic model checking scalable. We are interested in


Last updated: