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.

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