Research On Modeling And Verifying Timing Constraints Of Interrupt- Driven Systems

It is an important goal to satisfy its timing constraints when designing a real-time em-bedded system. Usually, timing constraints require a real time system to conforms to its functional specification while ensuring the timeliness of its behaviors. That is, a real-time embedded system must perform its functionality in time. Interrupt is an im-portant mechanism for embedded systems to give real-time responses. It allows a sys-tem’s execution to be interrupted by external events, and leads the system to execute corresponding codes of event handlers immediately. To ensure the timely execution of time-critical functions, designers must carefully combine both the task scheduling mechanism and the interrupt mechanism, when designing a real-time system.How to use preemptive scheduling mechanism and interrupt mechanism to design a real-time system so that all its timing constraints are satisfied is one of the challenging problems in embedded systems design. The executing traces of embedded systems are determined the combination of many factors, such as the task scheduling mechanism, the interrupt mechanism, the characteristics of the interrupt source, the execution time of the codes and etc, which is an infinite set. By now, there is no effective design method that ensures a design can always match its timing constraints. Therefore, the methods to assure the timeliness of system mostly rely on verification techniques taken when the design is finished.This paper focus on modeling and verifying real-time systems driven by periodic interrupt sources in terms of linear hybrid automata. We propose methods to verify timing constraints based on the path-oriented reachability and bounded reachability verification techniques for linear hybrid automata respectively, which transforms the timing constraints verification problems to reachability verification problems of linear hybrid automata at first. The reachability verification for the Linear hybrid automata is undecidable. Thus, we build a decidable subclass of models for real-time systems driven by periodic interrupt sources based on one-stopwatch automata, which is the system with only two-level interruption, and give an effective algorithm to verifying timing constraints. The main works of this paper are as following:· We propose a modeling method for real-time systems driven by periodic inter-rupt sources based on linear hybrid automata after we analysis the modeling requirements of this system and the limitations of the Interrupt timed automata. In the real-time system models, we can define several stopwatches to compute the cumulative execution time, and define the interrupt priority to simulate the interrupt mechanism. The model of the interrupt source describes the incoming of the interrupt source by global clock variables. The whole model is construct-ed by composing the real-time system model and the interrupt source model on their common events.· Based on the linear hybrid automata model, we study the methods to verify time constrains using path-oriented reachability verification and bounded reachabili-ty verification techniques. The timing constraints of a real-time system can be verified by checking the reachability of linear hybrid automata. Based on the path-oriented reachability verification method, we can construct a path set. All paths in the set can not satisfy the specification. Then we translate the time-constraints verification problem into the path set reachability checking problem. Adopting the bounded-reachability checking and constraint the system’s exe-cution by an integer k, we can check whether a timing constraint is satisfied in k steps.· Based on one-stopwatch automata, we construct a decidable subclass of models for real-time systems driven by periodic interrupt sources, where the real-time system consists only two-level interruption, and study the verification of its tim-ing constraints. By transforming the system model into an model without timing constraints, that can be called a state equivalence class graph, we can convert the problem of verifying timing constraints of two-level interrupt-driven system into the problem of the reachability checking in graph. The graph search algorith- m is used to solve the reachability problem. The complexity of this method is O[(|Q|+|E|)·2δ(N)],where |Q| stands for the numbers of locations, and |E| represents the numbers of transitions,δ(N) stands for the length of the clock constraints of N assuming binary encoding.