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

I-Corps：网络物理系统的正式规范驱动的验证和确认框架

• 批准号: 1454143
• 负责人: Georgios Fainekos
• 金额: $ 5万
• 依托单位: Arizona State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-09-01 至 2015-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1454143&HistoricalAwards=false
• 关键词: Corps; Formal; Specification; Driven; Verification

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.

使用当今可用的软件开发工具设计用于网络物理系统（CPS）的软件，例如现代飞机，汽车和医疗设备。 该软件可以通过实时限制分配，并且必须以非平凡的方式与物理环境进行交互。涉及安全关键系统的多个已知事故加强了测试和验证工具的需求，这些工具可以保证对系统的正确性和鲁棒性提供信心。随着安全至关重要的CP无处不在，需要确保正确的系统功能和性能的设计方法变得更加紧迫。该项目为复杂CP的测试，验证和验证提供了软件工具。该项目旨在将学术工具S-Taliro（一种用于验证和测试网络物理系统（CPS））的软件工具商业化。 S-Taliro通过在时间逻辑中表达的正式规格引导的自动测试生成和验证来提供此类功能。它可以分析大型且复杂的Simulink模型，用户定义的功能和BlackBox模型。 S-Taliro为规范伪造，参数估计，一致性测试和运行时规范监视提供了功能。此外，由于模块化体系结构，S-Taliro可以扩展以添加支持基于模型设计（MBD）过程的进一步功能。在当前的原型阶段，S-Taliro可以集成在Mathworks提供的MATLAB/SIMULINK中。