CAREER: Live Programming for Finite Model Finders

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

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.