Automated Software Verification: Foundations and Applications

自动化软件验证：基础和应用

• 批准号: RGPIN-2017-03998
• 负责人: Gurfinkel, Arie
• 金额: $ 2.48万
• 依托单位: University of Waterloo
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=710544
• 关键词: Automated; Software; Verification; Foundations; Applications

Modern software systems are incredibly complex engineered artifacts. They rely on intricate algorithms, developed by large, often distributed, teams, and are build out of many interconnected components. Software systems are extremely difficult to get right, to verify, and to certify. Software bugs are common even in such safety-critical industries as medical devices, automotive, and avionics. Yet, our society is increasingly becoming dependent on reliable operation of such systems. The border between safety- and non-safety-critical system is being eroded. Dealing with this complexity requires increased automation in verification and certification. Since the establishment of the Computer Science discipline, scientists have envisioned a mechanical verifier that would provide this automation. While the last few decades have seen tremendous progress towards this goal, it remains unrealized and challenging task. The long term objective of my proposed research is to develop scalable automated verification that is usable by software engineers and is integrated into the software development lifecycle. In the next five years, the proposed research will focus on building foundations of scalable automated verification based on Software Model Checking and exploring novel applications of verification in Software Engineering. Particular emphasis will be placed on automating modular reasoning, synthesis of environment assumptions, extending applicability of automated reasoning to complex models, and verification of concurrent and distributed systems. The proposed research will significantly extend applicability and usability of automated verification in practice. The long-term goal of the proposed research is to develop useful powerful software verification tools and supporting methodologies. These techniques will have a significant impact on Canadian industry by providing tools that will increase confidence and reduce bugs in software systems. Furthermore, the program will train Highly Qualified Personnel with the necessary skills to effectively apply automated verification to software systems. The research in software verification is highly interdisciplinary, requiring in-depth knowledge of logic, formal methods, automated reasoning, and software engineering. Techniques, decision engines, and tools developed for verification are often applicable to many related problems in Software Engineering and Computer Science. The project will train Highly Qualified Personnel in the fields of Software Verification and Software Engineering with a unique combination of interdisciplinary skills. It is expected that these skills will help the HQP to make a long lasting impact on Canadian industry and research.

现代软件系统是极其复杂的工程制品。它们依赖于复杂的算法，这些算法由大型且通常是分布式的团队开发，并且由许多互连的组件构建而成。软件系统的正确性、验证和认证极其困难。即使在医疗设备、汽车和航空电子设备等安全关键行业，软件错误也很常见。然而，我们的社会越来越依赖于此类系统的可靠运行。安全关键系统和非安全关键系统之间的界限正在被侵蚀。 处理这种复杂性需要提高验证和认证的自动化程度。自计算机科学学科建立以来，科学家们就设想了一种能够提供这种自动化功能的机械验证器。尽管过去几十年在实现这一目标方面取得了巨大进展，但它仍然是一项尚未实现且具有挑战性的任务。我提出的研究的长期目标是开发可供软件工程师使用并集成到软件开发生命周期中的可扩展的自动化验证。 未来五年，拟议的研究将侧重于构建基于软件模型检查的可扩展自动化验证的基础，并探索验证在软件工程中的新颖应用。将特别强调自动化模块化推理、环境假设的综合、将自动推理的适用性扩展到复杂模型以及并发和分布式系统的验证。拟议的研究将显着扩展自动验证在实践中的适用性和可用性。 拟议研究的长期目标是开发有用的、强大的软件验证工具和支持方法。这些技术将通过提供增强信心并减少软件系统错误的工具，对加拿大工业产生重大影响。此外，该计划还将培训具有必要技能的高素质人员，以有效地将自动验证应用于软件系统。 软件验证的研究是高度跨学科的，需要对逻辑、形式方法、自动推理和软件工程有深入的了解。为验证而开发的技术、决策引擎和工具通常适用于软件工程和计算机科学中的许多相关问题。该项目将培训软件验证和软件工程领域的高素质人才，并具有独特的跨学科技能组合。预计这些技能将帮助总部对加拿大工业和研究产生长期持久的影响。