CAREER: Methodologies and Tools for Large Real-Time Concurrent System Verification

University Of South Florida, Tampa FL

Investigators

Abstract

ABSTRACT 0546492 Zheng, Hao U of South Florida 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 correct operation of systems must be guaranteed at any cost for safety critical applications that can be found in nuclear power plants and airplane flight control systems. 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, a verification approach based on formal methods, has unique advantages because it is fully automated and can produce counter-examples for errors in systems to help debugging. Because of very high verification coverage, it can find bugs hidden very deeply. However, capabilities and robustness of model checking cannot keep up with the exponential growth of concurrent system complexity. It imposes a great burden on the model checking users to have deep understanding of the underlying verification algorithms and heuristics for effective use of the tools, thus limiting the widespread acceptance of model checking. This research addresses the challenges to and limitations of real-time concurrent system verification. In this research, the investigator studies various approaches to handle the complexity issue inherent in model checking, and develops methods and tools that enable model checking to be applicable to large real-time concurrent systems. These methods and tools are completely transparent to users of model checking so that they can be used in the same way as simulation. The intellectual merit of this research lies in a set of novel methods and algorithms to enhance the capacity and robustness of model checking for real-time concurrent system verification based on composition, hierarchy, and abstraction. Furthermore, design and verification are viewed as being interdependent, and a design-for-verification method with a new framework of high abstraction level modeling and refinement is developed. Successful completion of this research project will have broader impact on significant reduction in verification cost in the current system design process with improved capability of model checking, thus lowering the overall design cost of the final products. In addition, enabling model checking to be more accessible leads to dramatic improvements on product quality and system security, and reduces the losses due to the holes in products and systems. The integrated education plan of this research develops a new learning framework focusing on increasing students' learning and thinking skills, and integrating research with education. In addition, K-12 and underrepresented students will be involved in the proposed research through NSF REU and RET programs.