Model Checking Multi-interruption Concurrent Programs with TMSVL

Concurrent programs are commonly used in real-time system software. Verifying the correctness of concurrent programs is an important job to ensure the reliability of real-time system software. The causes of concurrency in a real-time system program include task scheduling and interrupt mechanism, where multi-interruption is an effective means of real-time response to asynchronous events. This paper studies the modeling approach for multi-interruption concurrent programs based on TMSVL (Timed Modeling, Simulation and Verification Language), so as to verify temporal properties of multi-interruption concurrent programs, such as safety and liveness properties. The formal syntax and semantics of multi-interruption concurrent programs is established based on TMSVL, and the correctness and practicability of our approach is demonstrated with a case study.