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

生物细菌可以使人生病，甚至危及人们的生命。同样，逻辑错误会使并发系统变得不可靠，甚至失败。在当今的并发系统设计中，及早发现并修复逻辑错误是最重要的，因为在设计阶段的后期发现错误是非常昂贵的。系统中的漏洞如果不被发现，可能会给经济和人类社会造成巨大损失。对于核电站和飞机飞行控制系统中的安全关键应用，必须不惜一切代价确保系统的正确运行。然而，确保复杂系统正常工作是非常困难的，因为系统的功能复杂性和密度都在指数级增长，这给验证带来了前所未有的挑战。在各种验证技术中，模型检测是一种基于形式化方法的验证方法，具有独特的优势，因为它是完全自动化的，可以为系统中的错误生成反例来帮助调试。由于验证覆盖率非常高，它可以找到隐藏得非常深的错误。然而，模型检测的能力和健壮性跟不上并发系统复杂性的指数增长。深入了解底层的验证算法和启发式算法以有效使用模型检查工具，给模型检查用户带来了很大的负担，从而限制了模型检查的广泛接受。在这项研究中，研究人员研究了各种方法来处理模型检测固有的复杂性问题，并开发了使模型检测适用于大型实时并发系统的方法和工具。这些方法和工具对模型检查的用户是完全透明的，因此可以像使用模拟一样使用它们。本研究的智能价值在于提出了一套新的方法和算法，以增强基于组合、层次和抽象的实时并发系统验证的模型检测的能力和健壮性。在此基础上，将设计与验证视为相互依赖的关系，提出了一种基于高抽象层次建模和求精的面向验证设计方法。这一研究项目的成功完成将对在当前系统设计过程中大幅降低验证成本产生更广泛的影响，提高模型检查能力，从而降低最终产品的总体设计成本。此外，使模型检查更容易实现，将显著提高产品质量和系统安全性，并减少由于产品和系统中的漏洞而造成的损失。这项研究的综合教育计划开发了一个新的学习框架，侧重于提高学生的学习和思维能力，并将研究与教育相结合。此外，K-12和代表性不足的学生将通过NSF REU和RET计划参与拟议的研究。

ABSTRACT0546492Zheng, HaoU of South FloridaBiological 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.