A verification system for interval-based specification languages with its application to simulink

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.