Please use this identifier to cite or link to this item: https://doi.org/10.1007/s00165-009-0108-9
Title: A formal framework for modeling and validating Simulink diagrams
Authors: Chen, C. 
Dong, J.S. 
Sun, J. 
Keywords: Formal Verification
Real-Time Specification
Simulink
Z Language
Issue Date: 2009
Source: 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. https://doi.org/10.1007/s00165-009-0108-9
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
URI: http://scholarbank.nus.edu.sg/handle/10635/38947
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.

SCOPUSTM   
Citations

19
checked on Dec 7, 2017

WEB OF SCIENCETM
Citations

8
checked on Nov 22, 2017

Page view(s)

72
checked on Dec 11, 2017

Google ScholarTM

Check

Altmetric


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