Machine-assisted proof support for validation beyond Simulink
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-assiste...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | text |
| Language: | English |
| Published: |
Institutional Knowledge at Singapore Management University
2007
|
| Subjects: | |
| Online Access: | https://ink.library.smu.edu.sg/sis_research/5053 https://ink.library.smu.edu.sg/context/sis_research/article/6056/viewcontent/Machine_Assisted_Proof_Support_for_Validation_Beyond_Simulink.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Singapore Management University |
| Language: | English |
| Summary: | 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. |
|---|