Publication Type

Journal Article

Version

publishedVersion

Publication Date

5-2009

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 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

Simulink, Real-Time Specification, Z Language, Formal Verification

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Formal Aspects of Computing

Volume

21

Issue

5

First Page

451

Last Page

483

ISSN

0934-5043

Identifier

10.1007/s00165-009-0108-9

Publisher

Springer (part of Springer Nature): Springer Open Choice Hybrid Journals

Additional URL

https://doi.org/10.1007/s00165-009-0108-9

Download

Share

COinS