Scenario-based Interrupt-driven System Modeling And Verification

Interrupt-driven systems are widely used in security-critical embedded systems such as in the area of aerospace,industrial process control.These systems are ex-tremely harsh on the reliability of both hardware and software,and errors or failures in those systems can cause economic losses,large-scale environmental damage,and even casualties.So,it is important and necessary to ensure the reliability of interrupt-driven system.In interrupt-driven systems,a significant amount of system processing is initiated by interrupts.Many potential hazardous system behaviors can only be revealed under the specific interrupt triggering order.These hazards are affected by environment and the probability is extremely low.And,it is very difficult to promise the robustness and reliability on interrupt-driven systems by testing.In this paper,a scenario-based interrupt-driven system modeling and verification method is proposed,which includes two aspects:interrupt-driven system modeling and its verification.In the aspect of system modeling,we propose an interrupt-driven system model-ing method based on Interrupt Sequence Diagram(ISD).The ISD is an extension of the UML sequence diagram according to the UML extension mechanism,which in-cludes:1)define a new combination fragment type to model interruption;2)introduce variable assignment operations on interactive events,used for control the triggering condition of interrupts;3)extend time constraint to enhance the expressiveness of real-time requirements in system.The ISD can both model system tasks and interrupts of in interrupt-driven system simply.Moreover,it can characterize the unpredictability and preemption of interrupts concisely.In response to model verification,Interrupt-driven system model is build via ISD,and then it is converted this into a hybrid automaton network,which is equivalent to the ISD model in semantics.At last,SpaceEx,a hybrid automata verification tool,is used to check the properties of task timeout and data consistency.Based on the above ideas,we have implemented a model checking tool,ISD-Checker,for interrupt-driven systems,which provides a visual user interface that en-ables system designers to build interrupt-driven system models quickly.Meanwhile,the effectiveness of our method has been evaluated by some experiments.