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, Platu, 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 Platu and make it more general for other application domains.


Methods and Algorithms for Scalable Symbolic Model Checking

In symbolic model checking, sets of states, instead of individual ones, are manipulated. Since the sets can be characterized by Boolean functions, symbolic model checking is actually a sequence of Boolean operations. Boolean functions and their operations can be efficiently represented and implemented ordered reduced binary decision diagrams (OBDDs), as an example shown on the right. This has allowed systems with several thousand state variables to be successfully verified. Not long ago, a different Boolean reasoning engine, Boolean satisfiability solvers (SAT) emerged as an excellent alternative to OBDDs for symbolic model checking. SAT-based approaches are able to handle larger designs, especially for debugging instead of complete correctness proof, and display higher rebustness.

However, both OBDDs and SAT solvers have worst case exponential complexity. Therefore, approaches based on these two Boolean engines still have difficult to scale up for larger systems. In this project, we investigate methods and algorithms to make symbolic model checking scalable, and we are interested in


Massively Parallel Computing and Its Applications

Moore's law has dictated semi-conductor industry's phenomenal progresses in performance in the past. Now, due to the physical limits, most processors sold today are manufactored multiple cores, while the speed of the cores is not increasing significantly. Therefore, software programs have to be parallelized to achieve higher performance. In this project, our goal is to study characteristics of parallel computing, and its applications in certain domains, especially some hard problems in electronics design automation (EDA). We will study issues/difficulties of parallel computing related to these targeted problems, and discover patterns and programming methods/environments to ease the difficulty in application parallelization. The following lists projects that are currently being considered for parallelization. More will be added in the future.

Last updated: