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.