The widespread real-time and embedded systems are mostly interrupt-driven because their heavy interaction with environment is often initiated by interrupts. With the interrupt arrival being unpredictable and the interrupt handling being preemptive, a huge number of possible system behaviours are generated, which makes the correctness assurance of such systems a difficult and costly task. Model checking is considered to be one of the effective methods for exhausting behavioural state space for correctness, however, existing modelling approaches for interrupt-driven systems are either based on calculus or automata theory, with which designers in industry are not familiar. To address this problem, we propose a new modelling language called interrupt sequence diagram (ISD). By extending the popular UML sequence diagram notations, the ISD supports the modelling of interrupts’ essential features visually and concisely, with a formal semantics interpreting the unpredictable and prioritised preemptive system behaviour caused by interrupts. For model checking purpose, we have devised algorithms that automatically translate an ISD to a subset of hybrid automata so as to leverage the abundant off-the-shelf checkers. Experiments on examples from both real-world and existing literature were conducted and the results demonstrate our approach’s usability and effectiveness.