Please use this identifier to cite or link to this item:
Title: A formal framework for modeling and validating Simulink diagrams
Authors: Chen, C. 
Dong, J.S. 
Sun, J. 
Keywords: Formal Verification
Real-Time Specification
Z Language
Issue Date: 2009
Citation: Chen, C., Dong, J.S., Sun, J. (2009). A formal framework for modeling and validating Simulink diagrams. Formal Aspects of Computing 21 (5) : 451-483. ScholarBank@NUS Repository.
Abstract: Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a real-time 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. © 2009 British Computer Society.
Source Title: Formal Aspects of Computing
ISSN: 09345043
DOI: 10.1007/s00165-009-0108-9
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.