I-Corps: Formal Specification Driven Verification and Validation Framework for Cyber-Physical Systems

使用当今可用的软件开发工具为网络物理系统（CPS）（如现代飞机、汽车和医疗设备）设计软件是一项挑战。软件可以在实时约束下分发，并且必须以重要的方式与物理环境交互。涉及安全关键系统的多个已知事故加强了对测试和验证工具的需求，这些工具可以保证对系统正确性和健壮性的信心。随着对安全至关重要的CPS变得无处不在，对保证正确系统功能和性能的设计方法的需求变得更加迫切。该项目产生了用于测试、验证和确认复杂CPS的软件工具。该项目旨在将学术工具S-TaLiRo商业化，这是一种用于验证和测试网络物理系统（CPS）的软件工具。S-Taliro通过启用自动测试生成和验证来提供这样的功能，这些测试生成和验证是由用时态逻辑表示的正式规范指导的。它可以分析大型复杂的Simulink模型、用户自定义函数和黑盒模型。S-Taliro提供了规范伪造、参数估计、一致性测试和运行时规范监控的功能。此外，由于采用模块化架构，S-Taliro可以进行扩展，以添加进一步的功能，以支持基于模型的设计（MBD）流程。在目前的原型阶段，S-Taliro可以集成在Mathworks提供的Matlab/Simulink中。

Designing software for cyberphysical systems (CPS), such as modern airplanes, automobiles, and medical devices, using the software development tools available today is a challenge. The software may be distributed with real time constraints and must interact with the physical environment in non-trivial ways. Multiple known accidents involving safety critical systems reinforce the need for testing and verification tools that provide a guaranteed level of confidence in the system correctness and robustness. As safety-critical CPS become ubiquitous, the need for design methods that guarantee correct system functionality and performance becomes more urgent. This project results in software tools for testing, verification and validation of complex CPS.This project aims to commercialize the academic tool S-TaLiRo, a software tool for the verification and testing of Cyber-Physical Systems (CPS). S-Taliro provides such capabilities by enabling automatic test generation and verification guided by formal specifications expressed in temporal logics. It can analyze large and complex Simulink models, user-defined functions and blackbox models. S-Taliro provides functionality for specification falsification, parameter estimation, conformance testing and runtime specification monitoring. Moreover, due to the modular architecture, S-Taliro can be extended to add further functionality in support of model-based design (MBD) processes. At its current prototype stage, S-Taliro can be integrated in Matlab/Simulink provided by Mathworks.