Static analysis of physical properties in Simulink models

Cyber-physical systems model and react to changes in physical phenomena. Modeling introduces the possibility of error, yet physical properties of physical phenomena are poorly represented in common programming and modeling languages. We present an approach to encoding and analyzing dimensions, units, and scale factors. Our approach appends physical properties to SIMULINK block names using an easy-to-read and easy-to-write syntax. For example, a SIMULINK block that outputs a force might be named Force (kg m/s"2) or Force (N). Our approach provides static analysis using PVS: Simulink 2PVS translates SIMULINK models into PVS, and PVS proves consistent use of physical properties during type checking. Our approach enables engineers to detect defects arising from mistakes in handling physical properties during development. Detecting these defects during development both decreases overall system cost and increases overall system dependability.