Abstraction and Automation for Reasoning about Complex Software

复杂软件推理的抽象和自动化

• 批准号: RGPIN-2015-06366
• 负责人: Chechik, Marsha
• 金额: $ 3.64万
• 依托单位: University of Toronto
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=708422
• 关键词: Abstraction; Automation; Reasoning; about; Complex

Modern software development is a complex and messy business. Requirements are likely incomplete. New development uses complex existing libraries, tools and components that can fail. Multiple development teams proceed on different schedules, making it difficult to assure that their artifacts will "talk to each other" as intended. Every time a change is made, expensive quality assurance needs to be performed to ensure that software still does what it was supposed to. Such problems are made even more dire because many companies, especially in automotive, electronics, aerospace and defense domains, need to maintain families of software product variants with similar yet not identical functionality (e.g., supporting different types of customers and/or software platforms).    I believe that many of the above problems can be aided by the availability of industrially scalable automated reasoning and analysis tools that enable users to answer essential questions about their artifacts. For example, they can determine the impact of a proposed change, ask "what if" questions about their designs, determine whether the different features are going to interact, check whether desired properties of a component would hold in any environment, etc. Creating such tools requires expertise both in formal verification and in software engineering, as many of the challenges are in improving usability of the analysis tools for SE practitioners, performing analysis at the "right" level of abstraction, enabling analysis earlier in the development lifecycle where complete information is not yet available, reusing results of analysis between product variants, etc.    The goal of this project is to develop precise, effective and scalable automated techniques to solve a variety of complex software engineering problems. The emphasis will be on enabling analysis of artifacts with incomplete information, handling product lines, and analysis reuse. I intend to leverage my in-depth knowledge of verification tools such as model-checkers and static analyzers as well as strive to establish the right abstractions to facilitate reasoning. Success of this project will significantly expand the scope of applicability of automated reasoning and analysis in practice.

现代软件开发是一项复杂而混乱的业务。需求可能不完整。新的开发使用复杂的现有库、工具和组件，这些都可能会失败。多个开发团队按照不同的时间表进行，这使得很难保证他们的工件将按照预期“相互通信”。每次进行更改时，都需要执行昂贵的质量保证，以确保软件仍然能够按照预期工作。由于许多公司，特别是在汽车、电子、航空航天和国防领域，需要维护具有相似但不相同功能的软件产品变体家族（例如，支持不同类型的客户和/或软件平台），因此此类问题变得更加严重。