Details

Autor(en) / Beteiligte

• Cui, Jin
• Lu, Xu
• Liang, Buwen

Titel

An Approach to Modeling and Verifying Multi-level Interrupt Systems with TMSVL

Ist Teil von

• Structured Object-Oriented Formal Language and Method, p.61-72

Ort / Verlag

Cham: Springer International Publishing

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• In embedded systems and operating systems, the interrupt mechanism is an important way to ensure real-time response to kinds of asynchronous events. While the interrupt mechanism changes the execution traces of the main program, it makes modeling and verification of systems with interrupt difficulty. Therefore, we propose an approach to modeling and verifying multi-level interrupt systems. Firstly, the model of multi-level interrupt systems based on Time Projection Temporal Logic (TPTL) is proposed. On this basis, the model can be used to extend the TMSVL language and the TMSVL interpreter so that multi-level interrupt systems can be modeled, simulated and verified automatically. Finally, a case study is given to show the correctness and practicability of the proposed approach.