CAREER: Live Programming for Finite Model Finders

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

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.