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的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估。