Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/40075
Title: Machine-assisted proof support for validation beyond Simulink
Authors: Chen, C. 
Dong, J.S. 
Sun, J. 
Keywords: Formal verification
PVS
Real-time specifications
Simulink
Issue Date: 2007
Source: Chen, C.,Dong, J.S.,Sun, J. (2007). Machine-assisted proof support for validation beyond Simulink. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 4789 LNCS : 96-115. ScholarBank@NUS Repository.
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. © Springer-Verlag Berlin Heidelberg 2007.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/40075
ISBN: 9783540766483
ISSN: 03029743
Appears in Collections:Staff Publications

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

Page view(s)

76
checked on Dec 16, 2017

Google ScholarTM

Check


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