Towards formal specification visualization for testing and monitoring of cyber-physical systems

摘要: One of the main challenges in software development for safety-critical Cyber-Physical Systems (CPS) is in achieving a certain level of confidence in the system correctness and robustness. In order to perform formal monitoring, testing and verification of CPS, the fully modular tool STaliro is presented. The tool is designed for seamless integration with the Model Based Design (MBD) process in Matlab/Simulink™. STaliro performs robustness guided Metric Temporal Logic (MTL) testing and monitoring. Since writing specifications in MTL is an error prone task that requires expert temporal logic users, a graphical formalism for the development and visualization of specifications is presented. The article provides an upto-date overview of STaliro. It includes a discussion on the benefits of the fully modular architecture and the challenges encountered in its development.