Title: Model Checking Multi-interruption Concurrent Programs with TMSVL
Abstract: 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.
Publication Year: 2021
Publication Date: 2021-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 1
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot