SHF: Small: Collaborative Research: Online Verification-Validation

SHF：小型：协作研究：在线验证-确认

• 批准号: 1618756
• 负责人: David Van Horn
• 金额: $ 14万
• 依托单位: University of Maryland, College Park
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-09-01 至 2019-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1618756&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Online

Increasingly, modern software on the web is richly extensible, accelerating its evolution and dramatically reducing the time between development and deployment. The intellectual merit of this research consists of challenging the false choice between creating software that is extensible (easy to reuse and extend) and software that is correct (meets its specifications). The new approach advanced by this work, Incremental Verification-Validation, enables programmers to bring domain-specific safely disciplines to extensible systems, by providing a framework where these disciplines are communicated both precisely and usefully, as executable code. The project's broader significance and importance consist in changing the way programmers approach building correct extensible software for the web. The research targets ECMAScript (JavaScript), enabling this research to have a direct impact on the vast number of languages and systems that create and use JavaScript. Further, the project represents a new collaboration across the University of Colorado and University of Maryland, bringing together experts across verification, incremental computing, and runtime systems. Finally, this project benefits the graduate and undergraduate teaching mission at the participating universities, as aspects of the project enriches the program analysis and programming language courses.Incremental Verification-Validation encourages programmers to co-design their systems with executable specifications that check these systems dynamically, as they execute. Moreover, unlike typical assertions, which execute dynamically and non-incrementally, the proposed are subject to novel patterns that enhance their performance: In regressive validation, verification partially discharges some checks, dynamically rewriting the program with residual versions; in progressive verification, online verification occurs in passes that each cache and reuse work, to avoid from-scratch verification of facts that still hold from earlier passes. Finally, to avoid forcing analysis programmers to reason about incremental changes explicitly in each analysis that they create, the meta layer expresses incremental computations implicitly, using an implicitly-incremental meta language whose abstractions hide reasoning on a per-change basis.

现代网络软件的可扩展性越来越强，加速了其发展并大大缩短了开发和部署之间的时间。 这项研究的智力价值在于挑战在创建可扩展的软件（易于重用和扩展）和正确的软件（满足其规范）之间的错误选择。这项工作提出的新方法“增量验证-验证”使程序员能够将特定于领域的安全规则引入可扩展系统，方法是提供一个框架，在该框架中这些规则可以作为可执行代码精确而有效地进行传达。 该项目更广泛的意义和重要性在于改变程序员为网络构建正确的可扩展软件的方式。该研究针对 ECMAScript (JavaScript)，使该研究能够对创建和使用 JavaScript 的大量语言和系统产生直接影响。 此外，该项目代表了科罗拉多大学和马里兰大学之间的新合作，汇集了验证、增量计算和运行时系统方面的专家。最后，该项目有利于参与大学的研究生和本科生教学任务，因为该项目的各个方面丰富了程序分析和编程语言课程。增量验证鼓励程序员使用可执行规范共同设计他们的系统，这些规范在执行时动态检查这些系统。此外，与动态且非增量执行的典型断言不同，所提出的断言受到增强其性能的新颖模式的影响：在回归验证中，验证部分地解除了一些检查，用剩余版本动态重写程序；在渐进式验证中，在线验证发生在每个缓存和重用工作的传递中，以避免从头开始验证早期传递中仍然保留的事实。最后，为了避免迫使分析程序员在他们创建的每个分析中显式地推理增量变化，元层使用隐式增量元语言隐式地表达增量计算​​，该语言的抽象隐藏了基于每个变化的推理。