Applying timed interval calculus to Simulink diagrams

Simulink has been used widely as an industry tool to model and simulate embedded systems. With increasing usage of embedded systems in real-time safety-critical situations, Simulink is deficient to cope with the requirements of high-level assurance and timing analysis. In this paper, we present a systematic approach to translate Simulink diagrams to Timed Interval Calculus (TIC), a notation extending Z to support real-time system specification and verification. This work is based on the same angle chosen by Simulink and TIC where they model systems in terms of continuous time. Translated TIC specifications preserve the functional and timing aspects of the diagrams, and cover a wide range of Simulink blocks. After the translation, we can increase the design space by specifying important requirements, especially timing constraints exactly on the system or its components. Moreover, we can take advantage of TIC reasoning rules to formally verify systems with requirements, and hence elevate the design quality of Simulink.