SHF: Small: Beyond Behavioral Software Contracts

为了创建复杂的应用程序，软件开发人员以类似乐高的方式组合组件。有些软件系统由上百个组件组成。这些组件之间的交互非常复杂，每个单独的组件都依赖于关于如何正确使用它的非正式描述，例如，“总是在这个之前运行这个功能，然后再运行这些部分之一”。但是，如果开发人员不小心违反了这些描述，事情可能会变得非常糟糕，让开发团队对问题的原因感到困惑。调查员和他的团队正在研究将这些非正式描述自动转换为检查的新技术。如果出现问题，这种检查会立即发出问题信号，包括提示哪些组件涉及违反使用规则。该项目将影响工作程序员的生活，消除无休止地寻找错误的时间。这个项目的目标不同于其他两种解决这个组合问题的方法。首先，类型系统在部署应用程序之前检查潜在的错误；但是现有的类型系统缺乏处理这些非正式描述的许多部分的能力。其次，运行时验证在应用程序执行的同时监视完整的系统规范；但是，运行时验证规范是在组件链接之后制定的，这意味着组件的开发人员无法保护其单独的代码。这个项目的新颖之处在于建立并扩展了行为软件契约。然而，调查者的团队正在开发一种机制来表示这些调用的序列以及与这些调用相关的所有值，而不是检查单个函数调用。然后，该机制允许组件开发人员根据这些序列的谓词来表达非正式的描述。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.