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.