A formal framework for modeling and validating Sim

Authors: Chunqing Chen Jin Song Dong Jun Sun

Publish Date: 2009/03/18

Volume: 21, Issue: 5, Pages: 451-483

PDF Link

Abstract

Simulink has been widely used in industry to model and simulate embedded systems With the increasing usage of embedded systems in realtime safetycritical situations Simulink becomes deficient to analyze timing requirements with highlevel assurance In this article we apply Timed Interval Calculus TIC a realtime specification language to complement Simulink with TIC formal verification capability We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams Next Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects Important requirements such as timing bounded liveness can be precisely specified in TIC for whole diagrams or some components Lastly validation of TIC models can be rigorously conducted with a high degree of automation using a generic theorem prover Our framework can enlarge the design space by representing environment properties to open systems and handle complex diagrams as the analysis of continuous and discrete behavior is supported

Keywords: