CCRI: Medium: Collaborative Research: Open-Source, State-of-the-Art Symbolic Model-Checking Framework

安全关键型和安全关键型系统正以越来越快的速度进入我们的生活。这些系统帮助我们驾驶飞机，驾驶汽车，运送包裹，确保我们的电力供应，甚至使我们的家庭自动化。特别是当人类无法亲自完成任务时，例如，由于危险的工作环境，我们依赖于这样的系统。在任何安全关键系统进入人类环境之前，我们需要确保它是真正安全的。模型检查是严格检查安全性的一种流行且吸引人的方法：给定系统或系统的精确模型和安全要求，模型检查是一种“按钮”技术，用于证明系统总是安全运行，或者详细说明违反安全要求的系统执行的反例。模型检查的许多方面都是活跃的研究领域，包括关于系统行为空间的更有效的推理方法，以及更快的证明和反例搜索算法。随着模型检查越来越多地集成到安全关键系统的标准设计和验证过程中，模型检查研究的平台变得越来越有限。以前的选项已经成为闭源或行业工具；目前的研究平台不支持验证实际系统所需的表达性规范语言。该项目将填补目前模型检查研究平台的空白：建立一个免费的、开源的、可扩展的模型检查基础设施，该基础设施接受表达模型，并与当前维护的最先进的后端算法有效地接口，以提供可扩展的研究和验证工具。该项目将创建一个社区资源，其中包含一个文档完备的中间表示，以支持可扩展性，以及一个web门户，促进新的建模语言和后端算法的进步。为了添加新的建模语言或算法，研究人员只需要开发一个新的中间语言的翻译器，然后就可以将每个进步与最先进的模型检查集成在一起。这个社区基础设施将是在许多前沿应用领域（包括安全性、网络和操作系统验证）中进行正式验证工作的理想选择。该项目将特别针对嵌入式系统（CPS）社区，因为提议的新框架将使该社区的硬件验证问题更容易访问。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Safety-critical and security-critical systems are entering our lives at an increasingly rapid pace. These are the systems that help fly our planes, drive our cars, deliver our packages, ensure our electricity, or even automate our homes. Especially when humans cannot perform a task in person, e.g., due to a dangerous working environment, we depend on such systems. Before any safety-critical system launches into the human environment, we need to be sure it is really safe. Model checking is a popular and appealing way to rigorously check for safety: given a system, or an accurate model of the system, and a safety requirement, model checking is a "push button" technique to produce either a proof that the system always operates safely, or a counterexample detailing a system execution that violates the safety requirement. Many aspects of model checking are active research areas, including more efficient ways of reasoning about the system's behavior space, and faster search algorithms for the proofs and counterexamples.As model checking becomes more integrated into the standard design and verification process for safety-critical systems, the platforms for model checking research have become more limited. Previous options have become closed-source or industry tools; current research platforms don't have support for expressive specification languages needed for verifying real systems. This project will fill the current gap in model checking research platforms: building a freely-available, open-source, scalable model checking infrastructure that accepts expressive models and efficiently interfaces with the currently-maintained state-of-the-art back-end algorithms to provide an extensible research and verification tool. This project will create a community resource with a well-documented intermediate representation to enable extensibility, and a web portal, facilitating new modeling languages and back-end algorithmic advances. To add new modeling languages or algorithms, researchers need only to develop a translator to/from the new intermediate language, and will then be able to integrate each advance with the full state-of-the-art in model checking. This community infrastructure will be ideal for catapulting formal verification efforts in many cutting-edge application areas, including security, networking, and operating system verification. This project will particularly target outreach to the embedded systems (CPS) community as the proposed new framework will make hardware verification problems from this community more accessible.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.