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

Arizona State University, Scottsdale AZ

Investigators

Abstract

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.