SHF: Small: Beyond Behavioral Software Contracts

SHF：小型：超越行为软件合同

• 批准号: 2116372
• 负责人: Matthias Felleisen
• 金额: $ 49.86万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-07-01 至 2025-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2116372&HistoricalAwards=false
• 关键词: SHF; Small; Beyond; Behavioral; Software

To create complex applications, software developers compose components in a Lego-like manner. Some software systems consist of 100s of components. The interactions among these components are quite intricate, with each individual component relying on informal descriptions on how to use it properly, say, ``always run this functionality before this one, followed by one of these pieces.'' But, if a developer accidentally causes a violation of such descriptions, things can go horribly wrong, leaving the developer team dumbfounded about the cause of the problem. The investigator and his team are studying novel techniques for automatically turning these informal descriptions into checks. If things go wrong, such checks immediately signal a problem, including hints as to which components are involved in the usage violation. The project will impact the lives of working programmers, eliminating hours of endless search for errors.The project's goals differ from those of two other approaches that tackle this composition problem. First, type systems check for potential errors before the application is deployed; but existing type systems lack the power to deal with many parts of these informal descriptions. Second, run-time verification monitors complete systems specifications in parallel with the execution of the application; but run-time verification specifications are formulated after the components are linked, meaning the developers of components cannot protect their individual code. The novelty of this project is to build on, and extend, behavioral software contracts. Instead of checking individual function calls, however, the investigator's team is developing a mechanism for representing sequences of such calls and all values associated with these calls. This mechanism then allows component developers to express informal descriptions in terms of predicates over these sequences.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

为了创建复杂的应用程序，软件开发人员以乐高的方式组成组件。一些软件系统由100个组件组成。这些组件之间的相互作用非常复杂，每个组件都依赖于如何正确使用它的非正式描述，例如，``在此功能之前始终运行此功能，然后是其中一部分。''但是，如果开发人员意外地导致违反这样的看法，那么事情可能会发生可怕的错误，就会使开发人员团队陷入困境。调查员及其团队正在研究自动将这些非正式描述变成检查的新技术。 如果出现问题，此类检查会立即提示问题，包括有关违反使用涉及哪些组件的提示。 该项目将影响工作程序员的生活，消除了无限搜索错误的时间。项目的目标与解决该组成问题的其他两种方法的目标不同。首先，在部署应用程序之前，类型系统检查潜在错误；但是现有类型系统缺乏处理这些非正式描述的许多部分的能力。其次，运行时验证与应用程序执行并行监控完整的系统规格；但是，在链接组件后，制定运行时验证规范，这意味着组件的开发人员无法保护其单个代码。该项目的新颖性是建立并扩展行为软件合同。但是，调查员的团队没有检查单个功能调用，而是开发了一种代表这些调用序列以及与这些呼叫相关的所有值的机制。然后，这种机制使组件开发人员能够以这些序列的谓词来表达非正式的描述。该奖项反映了NSF的法定任务，并且使用基金会的知识分子优点和更广泛的影响审查标准，被认为值得通过评估来获得支持。