Visualizing properties of Simulink models

摘要

Model-based development of software using tools such as MathWorks Simulink has become common in the engineering of safety-critical systems. When working with Simulink, engineers need to be able to assure that the subject models possess crucial properties such as: (1) safety properties are met, (2) the use of measurement units is consistent, (3) freedom from exceptions, (4) the execution sequences of blocks is as planned, and (5) data types are inferred properly. In this paper, we describe: (a) an approach to the graphic decoration of Simulink models to display information determined by formal verification, and (b) a system, SimulinkDec, that implements the decoration. Block colouring, enhancements to block textual descriptions, and comments are used to present the information of interest to the user. SimulinkDec provides a graphical user interface that allows engineers to easily perform formal verification and display the results of that analysis.