Interrupt driving system verification method based on interrupt sequence diagram

Abstract

The invention discloses an interrupt drive system verification method based on an interrupt sequence diagram, which comprises the following steps of: 1, establishing an interrupt drive system model based on the interrupt sequence diagram; 2, according to the interrupt sequence diagram obtained in the step 1, dividing an interaction fragment into a basic interaction fragment and a composite interaction fragment; step 3, sequentially converting the basic interaction fragment and the composite interaction fragment into an automatons; step 4, synthesizing the plurality of automatons obtained in the step 3 into a hybrid automaton; 5, extracting constraints of the interrupt sequence graph, and adding the constraints to the automaton model obtained through conversion; 6, extracting verification attribute information in the interrupt sequence diagram, and adding the verification attribute serving as a constraint to the automaton model obtained through conversion; 7, describing the automaton into an input format acceptable by an automaton verification tool; and step 8, performing verification by adopting an automaton verification tool.

Description

technical field [0001] The invention belongs to the fields of software engineering and system design verification. The invention relates to a method for verifying an interrupt-driven system based on an interrupt sequence diagram. Interrupt-driven system designers can use this method to describe and verify interrupt-driven systems simply and intuitively. Background technique [0002] With the rapid development of computer technology, computer systems have entered all aspects of our lives, rail transit systems, financial systems, medical systems, etc. have been highly computerized. The interrupt-driven system has been widely used in interrupt-driven systems with relatively limited hardware and software resources, such as aerospace, industrial process control, etc., and these systems are usually safety-critical systems, and their incorrect functions or failures will cause serious damage. Accidents such as economic loss, large-scale destruction or even casualties. In an inter...

AI Technical Summary

Problems solved by technology

[0005] In terms of model verification, the automata model is generally used for comprehensive detection of software systems based on the idea of ​​model verification. In fact, the interrupt-driven system based on automata based on the automata model is not conducive to the interrupt-driven system designers. Modeling, and the automaton model cannot intuitively express the interactive behavior and real-time requirements of the system like the sequence diagram

For some complex system interaction scenarios, the state space of the system is very large, and it is very difficult and error-prone to construct such an automaton model

Images