Part of the book series:Lecture Notes in Computer Science ((LNPSE,volume 6405))
Included in the following conference series:
569Accesses
Abstract
Interrupts play an important role in embedded software. Unfortunately, they aggravate the state-explosion problem that model checking is suffering from. Therefore, we propose a new abstraction technique based on partial order reduction that minimizes the number of locations where interrupt handlers need to be executed during model checking. This significantly reduces state spaces while the validity of the verification results is preserved. The paper details the underlying static analysis which is employed to annotate the programs before verification. Moreover, it introduces a formal model which is used to prove that the presented abstraction technique preserves the validity of the branching-time logic CTL*-X by establishing a stutter bisimulation equivalence between the abstract and the concrete transition system. Finally, the effectiveness of this abstraction is demonstrated in a case study.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5719
- Price includes VAT (Japan)
- Softcover Book
- JPY 7149
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Schlich, B.: Model Checking of Software for Microcontrollers. Dissertation, RWTH Aachen University, Aachen, Germany (June 2008)
Noll, T., Schlich, B.: Delayed nondeterminism in model checking embedded systems assembly code. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 185–201. Springer, Heidelberg (2008)
Herberich, G., Noll, T., Schlich, B., Weise, C.: Proving correctness of an efficient abstraction for interrupt handling. In: Systems Software Verification (SSV 2008). ENTCS, vol. 217, pp. 133–150. Elsevier, Amsterdam (2008)
Emerson, E.A.: Handbook of Theoretical Computer Science. In: Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. The MIT Press, Cambridge (1991)
Yorav, K., Grumberg, O.: Static analysis for state-space reductions preserving temporal logics. Formal Methods in System Design 25(1), 67–96 (2004)
Brauer, J., Schlich, B., Reinbacher, T., Kowalewski, S.: Stack bounds analysis for microcontroller assembly code. In: 4th Workshop on Embedded Systems Security (WESS 2009), Grenoble, France. ACM, New York (2009) (to appear)
Heljanko, K.: Model checking the branching time temporal logic CTL. Research Report A45, Helsinki University of Technology, Digital Systems Laboratory, Espoo, Finland (May 1997)
Browne, M., Clarke, E., Grumberg, O.: Characterizing finite kripke structures in propositional temporal logic. Theor. Comput. Sci. 59(1-2), 115–131 (1988)
van Glabbeek, R., Weijland, W.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555–600 (1996)
Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 176–185. Springer, Heidelberg (1991)
Holzmann, G.J., Peled, D.A.: An improvement in formal verification. In: Formal Description Techniques VII. IFIP International Federation for Information Processing, pp. 197–211. Springer, Heidelberg (1995)
Peled, D.: Ten years of partial order reduction. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 17–28. Springer, Heidelberg (1998)
Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Regehr, J., Cooprider, N.: Interrupt verification via thread verification. Electronic Notes in Theoretical Computer Science 174(9), 139–150 (2007)
Kahlon, V., Sankaranarayanan, S., Gupta, A.: Semantic reduction of thread interleavings in concurrent programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 124–138. Springer, Heidelberg (2009)
Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Communications of the ACM 18(12), 717–721 (1975)
Katz, S., Peled, D.: Defining conditional independence using collapses. Theoretical Computer Science 101(2), 337–359 (1992)
Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Principles of Programming Languages (POPL 2009), Savanna, USA, pp. 2–15. ACM, New York (2009)
Farzan, A., Madhusudan, P.: Causal dataflow analysis for concurrent programs. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 102–116. Springer, Heidelberg (2007)
Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 37–51. Springer, Heidelberg (2008)
Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)
Lal, A., Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 282–298. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Embedded Software Laboratory, RWTH Aachen University, Ahornstr. 55, 52074, Aachen, Germany
Bastian Schlich, Jörg Brauer & Lucas Brutschy
Software Modeling and Verification Group, RWTH Aachen University, Ahornstr. 55, 52074, Aachen, Germany
Thomas Noll
- Bastian Schlich
You can also search for this author inPubMed Google Scholar
- Thomas Noll
You can also search for this author inPubMed Google Scholar
- Jörg Brauer
You can also search for this author inPubMed Google Scholar
- Lucas Brutschy
You can also search for this author inPubMed Google Scholar
Editor information
Editors and Affiliations
Bell Laboratories, Alcatel-Lucent, 600 Mountain Ave., 2B-435, 07974, Murray Hill, NJ, USA
Kedar Namjoshi
Saarland University, Campus E1, 66123, Saarbrücken, Germany
Andreas Zeller
IBM Research Laboratory, 31905, Haifa, Mount Carmel, Israel
Avi Ziv
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schlich, B., Noll, T., Brauer, J., Brutschy, L. (2011). Reduction of Interrupt Handler Executions for Model Checking Embedded Software. In: Namjoshi, K., Zeller, A., Ziv, A. (eds) Hardware and Software: Verification and Testing. HVC 2009. Lecture Notes in Computer Science, vol 6405. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19237-1_5
Download citation
Publisher Name:Springer, Berlin, Heidelberg
Print ISBN:978-3-642-19236-4
Online ISBN:978-3-642-19237-1
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative