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

职业：大型实时并发系统验证的方法和工具

• 批准号: 0546492
• 负责人: Hao Zheng
• 金额: $ 40万
• 依托单位: University of South Florida
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-03-15 至 2012-02-29
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0546492&HistoricalAwards=false
• 关键词: CAREER; Methodologies; Tools; Large; Real

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.

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