Please use this identifier to cite or link to this item:
Title: A verification system for interval-based specification languages with its application to simulink
Keywords: Real-time computing systems, Interval-based specification languages, Formal verification, PVS, Simulink
Issue Date: 3-Sep-2009
Source: CHEN CHUNQING (2009-09-03). A verification system for interval-based specification languages with its application to simulink. ScholarBank@NUS Repository.
Abstract: Real-time computing systems usually interact with physical environment, and their computations often involve mathematical functions of time. With their increasing usage in safety-critical situations, it is necessary and important to rigorously validate these system designs associated with the properties of the environment. Timed Interval Calculus (TIC) is an expressive specification language on modeling and reasoning about real-time systems. Its formal verification capabilities are useful to rigorously prove if system designs satisfy functional and non-functional requirements. When real-time computing systems are complex, it is difficult to ensure the correctness of each proof step and to keep track of all proof details in a pencil-and-paper manner. It is thus necessary and important to develop a verification system to make proofs easier. On the other hand, the analysis of these systems usually involves mathematical reasoning such as integral calculus for modeling physical dynamics, and induction mechanisms for dealing with arbitrary intervals and continuous time domain. This thesis presents a systematic way to develop a system to carry out TIC verification at an interval level with a high degree of automation, and further illustrates the extensibility and benefits of our approach. The verification system is built upon a powerful generic theorem prover, Prototype Verification System (PVS). A collection of supplementary rules and proof strategies have also been developed to make proofs more automated. In addition, we have expanded the verification system to handle Duration Calculus (DC) which is another popular interval-based specification language. We can reason about DC axioms and perform DC proofs in a manner similar to manual DC arguments. Based on the TIC-PVS verification system, a novel framework is proposed to explore the usage of formal methods on improving industrial tools, for example, Simulink which graphically models and simulates embedded systems. However, Simulink is deficient in checking requirements of high-level assurance, and this is where formals methods have strengths. Our framework can formally capture functional and timing aspects of Simulink diagrams, enlarge the design space of Simulink, and rigorously conduct validation of Simulink diagrams.
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
thesis.pdf2.49 MBAdobe PDF



Page view(s)

checked on Jan 20, 2018


checked on Jan 20, 2018

Google ScholarTM


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