I-Corps: VeriSight CPS: Enhancing the Design and Operation of Cyber-Physical Systems with Verified Insight

信息物理系统（CPS）将计算与物理过程紧密结合。例子包括现代汽车、医疗设备、玩具、无人机、机器人、智能恒温器和暖通空调系统等等。随着“物联网（IoT）”的日益流行，这些系统的商业潜力已经得到了认可。随着CPS/IoT系统的设计走向主流，从研究、业余爱好者和小众工业活动到主流的大规模工业，设计挑战也在增加。一个主要的挑战是帮助设计师和用户更好地了解他们的系统：系统必须和不应该有什么行为，为什么它们表现出某些期望/不希望的行为，以及如何设计和实现它们以实现期望的行为。该项目建议创建一个软件工具包VeriSight CPS，并研究其应对这一挑战的能力。VeriSight可用于在系统设计和操作的各个阶段回答有关系统的查询。VeriSight工具包预计将在几个领域产生工业影响，包括运输、机器人和医疗设备。该项目的技术目标是开发一个软件工具包，以协助网络物理系统的规范、设计、验证、调试、优化和维护，并在一组具有高影响的应用程序中调查其有效性。其基础理论是设计自动化和机器学习的形式化方法的新颖混合。与主流的机器学习和数据分析技术不同，VeriSight CPS涉及使用验证技术来分析模型和回答查询。该项目的预期贡献包括适用于多个应用领域的VeriSight CPS的通用软件架构，各种用户交互模型的研究，以及在关键CPS领域（包括交通、医疗设备和机器人）的工业应用的探索。这个创新军团（I-Corps）项目的一个关键部分将是采访潜在客户，例如，从上面列出的类别，并确定哪些选择将是最富有成效的。

Cyber-Physical Systems (CPS) tightly integrate computation with physical processes. Examples include modern automobiles, medical devices, toys, drones, robots, smart thermostat and HVAC systems and many more. The commercial potential of these systems has been recognized with the growing buzz around the "Internet of Things (IoT)." As the design of CPS/IoT systems goes mainstream, from a research, hobbyist, and niche industrial activity to a mainstream, large-scale industry, the design challenges are mounting. A primary challenge is to help designers and users gain better insight into their systems: what behaviors the systems must and must not have, why they exhibit certain desired/undesired behaviors, and how to design and implement them to achieve desired behavior. This project proposes to create a software toolkit, VeriSight CPS, and investigate its capabilities to meet this challenge. VeriSight can be used to answer queries about a system at various phases of the design and operation of a system. Industrial impact of the VeriSight toolkit is anticipated in several areas, including transportation, robotics, and medical devices.The technical goals of this project are to develop a software toolkit to assist in the specification, design, verification, debugging,optimization, and maintenance of cyber-physical systems, and to investigate its effectiveness in a focused set of applications of high impact. The underlying theory is a novel blend of formal methods for design automation and machine learning. Unlike mainstream machine learning and data analytics techniques, VeriSight CPS involves the use of verification technology to analyze models and to answer queries. The envisioned contributions of the project include a general software architecture for VeriSight CPS applicable to multiple application domains, the investigation of various user interaction models, and an exploration of industrial applications in key CPS domains including transportation, medical devices, and robotics. A key part of this Innovation Corps (I-Corps) project will be to interview potential customers, e.g., those from the categories listed above, and determine which options will be the most fruitful.