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.