CAREER: Live Programming for Finite Model Finders

职业：有限模型查找器的实时编程

• 批准号: 2337667
• 负责人: Allison Sullivan
• 金额: $ 52.5万
• 依托单位: University of Texas at Arlington
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-06-01 至 2029-05-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2337667&HistoricalAwards=false
• 关键词: CAREER; Live; Programming; Finite; Model

As software permeates every aspect of our everyday lives, the problem of software reliability has grown both in importance and complexity. Software modeling has shown promise in providing ways to improve software reliability, however the specialization required to build accurate software models has limited their adoption. Current model development environments are rather “bare bones,” providing no guidance or feedback other than the output itself, and limiting the revision process to the age-old “edit and check.” This project aims to address these challenges through the creation of a new model development environment. The project’s novelties are new tools that combine live programming innovations with the strengths inherent to modeling languages to provide a range of contextualized feedback during development. The project’s impacts are in lowering the barrier to entry for software modeling and aiding formal methods education. Concretely, this project focuses on bringing live programming to finite model finders to interweave the process of writing and evaluating a software model. To achieve this, the project investigates the efficacy of different live development interfaces that suggest edits to complete formulas and that help users explore and contrast how different edits impact the collection of scenarios produced. Since live programming elevates the role of the output, this project also explores a new model development workflow, output directed debugging, that enables users to edit the scenarios in order to correct the underlying model. In addition, these live interfaces will form the basis for an interactive learning environment for mathematical logic to improve formal methods education at both the undergraduate and graduate level.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.

随着软件渗透到我们日常生活的各个方面，软件可靠性问题变得越来越重要和复杂。软件建模在提供提高软件可靠性的方法方面已显示出希望，但是构建准确的软件模型所需的专业化限制了它们的采用。当前的模型开发环境相当“简单”，除了输出本身之外不提供任何指导或反馈，并将修订过程限制为古老的“编辑和检查”。该项目旨在通过创建新的模型开发环境来应对这些挑战。该项目的新颖之处在于新工具将实时编程创新与建模语言固有的优势相结合，在开发过程中提供一系列上下文反馈。该项目的影响在于降低软件建模的进入门槛并帮助正式方法教育。具体来说，该项目的重点是将实时编程引入有限模型查找器中，以将编写和评估软件模型的过程交织在一起。为了实现这一目标，该项目研究了不同实时开发界面的功效，这些界面建议进行编辑以完成公式，并帮助用户探索和对比不同的编辑如何影响所生成的场景集合。由于实时编程提升了输出的作用，因此该项目还探索了一种新的模型开发工作流程，即输出定向调试，使用户能够编辑场景以纠正底层模型。此外，这些实时界面将构成数理逻辑交互式学习环境的基础，以改善本科和研究生水平的形式方法教育。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。