The Technique Of Model Checking Of Real-time Systems And Its Application For Interrupt-Driven Systems

Real-time embedded systems are widely used in safety critical systems. Any system failure could cause significant loss of life and property. So, it is vital to ensure the reliability of safety-critical interrupt-driven real-time systems. The correctness of a real-time system is depends not only on the logical result of computation, but also on the time at which the result are generated.In order to ensure security and reliability of software systems, formal methods have been proposed to verify the correctness of these systems. Formal verification, which based on the mathematics and logic theory, can help designers and developers to detect system errors in the early phase. Model checking is an automatically formal verification technique which is mainly used in the verification of concurrent systems with finite state-spaces. Model checking uses formal languages to describe system models and specifications, performs exhaustive exploration on model state-spaces, and checks whether the system model of concurrent system satisfies its specification automatically. Today, the fruitful achievement in the research of real time model checking has been widely applied to the industrial community in the process of designing and developing.The main work of this thesis includes following aspects:●The main challenge in model checking is the state-space explosion problem. To alleviate this problem, we propose a new approach of partial order reduction technique for timed automata model checking. This method avoids the exhaustive state-space exploration by enumerating only part of enabled transitions at some symbolic states. We give some sufficient conditions on which partial enumeration does not change the reachability analysis result. Efficient algorithms are presented to check these conditions. The optimized reachability analysis algorithm computes only successors w.r.t. part of enabled transitions when it visits a symbolic state the first time. Later, the algorithm revisits generated states to check whether it is necessary to enumerate all●To assist system designers and developers improving the reliability of the real-time system by the model checking technique, we propose a method to model the interrupt-driven system and the rule to abstract the model system from a real-time system. First of all, we identify the major system elements (including system scheduling tasks, interrupts and their handlers) and their parameters relevant to time-related failures. And, we provide several forms for system designers to specify these elements and parameters during the design phase. Then, we propose the method to transform these elements and parameters into formal models. The interrupt source is modeled as the interrupt timed automaton. The execution processes of interrupt handlers are modeled by the interrupt vector and the CPU process stack.●The interrupt-driven system usually consists of interrupt handlers and system-scheduling tasks. When an interrupt occurs, the corresponding interrupt-handler executes in response. The operating system schedules a set of tasks to deal with routine events and post-processing of some interrupts. In the real-time control system, it is important that interrupts are handled within their specific deadlines. Otherwise, it may cause catastrophic system failures. Based on the method of modelling the real-time system and transforming from the required information of given forms into the formal system model, we provide a model-checking algorithm to check the above formal model whether interrupt handlers can be executed within their response deadlines. Moreover, we provide a variation of this algorithm to check properties of the integrity of shared resources and the atomicity of subprograms.●We extend the model system to describe more complex system behaviors. In the extended system, interrupt processing program and system tasks can be related by control variables. The model system executes different segments of code according to the value of the related control variable. Then, we provide a bounded model checking algorithm for the refined model system. The algorithm explores all feasible paths using the depth-first searching method. During the exploring process, the time constraints and time requirement in the specification are resolved by the SMT solver.