Chunqing's PhD Thesis

• For Review Version (1.5 lined,12pt): PDF.

Real-time computing systems usually interact with physical environment, and they 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 at an early stage.

Timed Interval Calculus (TIC) is an expressive specification language on modeling and reasoning about real-time systems. It supports differential and integral calculus as well. The formal verification capabilities of TIC are useful to rigorously prove if system designs satisfy functional and non-functional (specifically, timing) 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 ease proofs. 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). From our rigorous checking of TIC reasoning rules, subtle flaws in original rules have been discovered. 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 thus reason about DC axioms and perform DC proofs in a manner similar to the corresponding manual DC arguments. Moreover, an improper proof step in a common DC case study has been identified.

Based on the verification system, a formal framework is proposed to complement Simulink which graphically models and simulates embedded systems. Simulink is deficient in checking requirements of high-level assurance and lacks support of timing analysis. This framework captures the functional and timing aspects of Simulink diagrams, enlarges design space, and copes with validation beyond Simulink. Furthermore, semantic incompleteness and a bug in Simulink library blocks have been discovered from the rigorous validation.

Publications from the Thesis

• Chunqing Chen, Jin Song Dong, Jun Sun and Andrew Martin. A Verification System for Interval-based Specification Languages, ACM Transactions on Software Engineering and Methodology. Accepted with Minor Revision..
• Chunqing Chen, Jin Song Dong and Jun Sun. A Formal Framework for Modeling and Validating Simulink Diagrams, Formal Aspects of Computing. Accepted.
• Chunqing Chen, Jin Song Dong and Jun Sun. A Verification System for Timed Interval Calculus, In the 30th International Conference of Software Engineering (ICSE'08), Leipzig, Germany, 2008.
• Chunqing Chen, Jin Song Dong and Jun Sun. Machine-assisted Proof Support for Validation beyond Simulink, In the 9th International Conference on Formal Engineering Methods (ICFEM'07), Boca Raton, USA, 2007.
• Chunqing Chen, Jin Song Dong. Applying Timed Interval Calculus to Simulink Diagrams, In the 8th International Conference on Formal Engineering Methods (ICFEM'06), Macau, China, 2006.  

Last updated: 02/09/2009