Abstract
This paper presents an overtime-detection model-checking technique for interrupt processing systems. It is very important to verify real-time properties of such systems because many of them are safety-critical. This paper gives a method to check that critical interrupts can be handled within their timeout periods. Interrupt processing systems are modeled as extended timed automata. Our technique checks whether the system under check can handle critical interrupts in time using symbolic model-checking techniques. Taking an aerospace control system as an example, we show that our technique can find time-scheduling problems in interrupt processing systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Silberschatz, A., Galvin, P.B.: Operating System Concepts (1998)
Walker, W., Cragon, H.G.: Interrupt Processing in Concurrent Processors. IEEE Computer 28(6), 36–46 (1995)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Brylow, D., Palsberg, J.: Deadline Analysis of Interrupt-driven Software (2003)
Alur, R., Dill, D.: A Theroy of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)
Henzinger, T.A.: The Theory of Hybrid Automata. LICS, 278–292 (1996)
Zhao, J., Li, X., Zheng, T., Zheng, G.: Removing Irrelevant Atomic Formulas for Checking Timed Automata Efficiently. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 34–45. Springer, Heidelberg (2004)
Dill, D.L.: Timing Assumptions and Verification of Finite-state Concurrent Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhou, X., Zhao, J. (2013). An Overtime-Detection Model-Checking Technique for Interrupt Processing Systems. In: Yuan, Y., Wu, X., Lu, Y. (eds) Trustworthy Computing and Services. ISCTCS 2012. Communications in Computer and Information Science, vol 320. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35795-4_61
Download citation
DOI: https://doi.org/10.1007/978-3-642-35795-4_61
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35794-7
Online ISBN: 978-3-642-35795-4
eBook Packages: Computer ScienceComputer Science (R0)