Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

11-2007

Abstract

Simulink is popular in industry for modeling and simulating embedded systems. It is deficient to handle requirements of high-level assurance and timing analysis. Previously, we showed the idea of applying Timed Interval Calculus (TIC) to complement Simulink. In this paper, we develop machine-assisted proof support for Simulink models represented in TIC. The work is based on a generic theorem prover, Prototype Verification System (PVS). The TIC specifications of both Simulink models and requirements are transformed to PVS specifications automatically. Verification can be carried out at interval level with a high level of automation. Analysis of continuous and discrete behaviors is supported. The work enhances the applicability of applying TIC to cope with complex Simulink models.

Keywords

Simulink, Real-Time Specifications, Formal Verification, PVS

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15

First Page

95

Last Page

115

ISBN

9783540766483

Identifier

10.1007/978-3-540-76650-6_7

Publisher

Springer Link

City or Country

Boca Raton, FL, USA

Additional URL

https://doi.org/10.1007/978-3-540-76650-6_7

Download

Share

COinS