Skip to main content
SpringerLink
Log in

Testing the IPC Protocol for a Real-Time Operating System

  • Conference paper
Verified Software: Theories, Tools, and Experiments (VSTTE 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9593))

Included in the following conference series:

Abstract

In this paper, we adapt model-based testing techniques to concurrent code, namely for test generations of an (industrial) OS kernel called PikeOS. Since our data-models are complex, the problem is out of reach of conventional model-checking techniques. Our solution is based on symbolic execution implemented inside the interactive theorem proving environment Isabelle/HOL extended by a plugin with test generation facilities called HOL-TestGen.

As a foundation for our symbolic computing techniques, we refine the theory of monads to embed interleaving executions with abort, synchronization, and shared memory to a general but still optimized behavioral test framework.

This framework is instantiated by a model of PikeOS inter-process communication system-calls. Inheriting a micro-architecture going back to the L4 kernel, the system calls of the IPC-API are internally structured by atomic actions; according to a security model, these actions can fail and must produce error-codes. Thus, our tests reveal errors in the enforcement of the security model.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Hierons, R.M., Bowen, J.P., Harman, M. (eds.): FORTEST. LNCS, vol. 4949. Springer, Heidelberg (2008)

    Google Scholar 

  2. Brucker, A.D., Wolff, B.: Test-sequence generation with Hol-TestGen with an application to firewall testing. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 149–168. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Brucker, A.D., Wolff, B.: hol-TestGen: an interactive test-case generation framework. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 417–420. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Brucker, A.D., Wolff, B.: On theorem prover-based testing. Formal Aspects Comput. 25, 683–721 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  5. Brucker, A.D., Feliachi, A., Nemouchi, Y., Wolff, B.: Test program generation for a microprocessor. In: Veanes, M., Viganò, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 76–95. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  6. Ponce de León, H., Haar, S., Longuet, D.: Conformance relations for labeled event structures. In: Brucker, A.D., Julliand, J. (eds.) TAP 2012. LNCS, vol. 7305, pp. 83–98. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Euro-Mils. http://www.euromils.eu/

  8. Feliachi, A., Gaudel, M.-C., Wenzel, M., Wolff, B.: The \(Circus\) testing theory revisited in Isabelle/HOL. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 131–147. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Gill, A.: Introduction to the Theory of Finite-State Machines. McGraw-Hill, New York (1962)

    MATH  Google Scholar 

  10. Härtig, H., Hohmuth, M., Liedtke, J., Schönberg, S., Wolter, J.: The performance of microkernel-based systems. In: SOSP (1997)

    Google Scholar 

  11. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: SOSP, pp. 207–220 (2009)

    Google Scholar 

  12. Liedtke, J.: On \(\mu \)-kernel construction. SOSP 29(5), 237–250 (1995)

    Google Scholar 

  13. Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI-Quart. 2(3), 219–246 (1989)

    MathSciNet  MATH  Google Scholar 

  14. Common criteria for information technology security evaluation. http://www.commoncriteriaportal.org/

  15. Musuvathi, M., Qadeer, S., Ball, T.: Chess: a systematic testing tool for concurrent software. Technical report MSR-TR-2007-149, Microsoft Research (2007)

    Google Scholar 

  16. Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  17. Shan Lu, W.J., Zhou, Y.: A study of interleaving coverage criteria. In: ESEC-FSE Companion, pp. 533–536 (2007)

    Google Scholar 

  18. SYSGO: Pikeos. http://www.sysgo.com/products/pikeos-rtos-and-virtualization-concept/

  19. SYSGO: PikeOS Fundamentals. SYSGO (2013)

    Google Scholar 

  20. SYSGO: PikeOS Kernel. SYSGO (2013)

    Google Scholar 

  21. Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Wadler, P.: Comprehending monads. Math. Struct. Comput. Sci. 2(4), 461–493 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  23. Zhu, H., Hall, P.A.V., May, J.H.R.: Software unit test coverage and adequacy. ACM Comput. Surv. (CSUR) 29(4), 366–427 (1997)

    Article  Google Scholar 

Download references

Acknowledgement

This work was partially supported by the Euro-MILS project funded by the European Union’s Programme [FP7/2007-2013] under grant agreement number ICT-318353.

Author information

Authors and Affiliations

  1. SAP SE, Vincenz-Priessnitz-Str. 1, 76131, Karlsruhe, Germany

    Achim D. Brucker

  2. LRI, Université Paris Sud, CNRS, Centrale Supélec, Université Saclay, Orsay, France

    Yakoub Nemouchi & Burkhart Wolff

  3. SYSGO AG, Am Pfaffenstein 14, 55270, Klein-Winternheim, Germany

    Oto Havle

Authors
  1. Achim D. Brucker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Oto Havle
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yakoub Nemouchi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Burkhart Wolff
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Achim D. Brucker .

Editor information

Editors and Affiliations

  1. Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA, USA

    Arie Gurfinkel

  2. Department of Electrical Engineering and Computer Science, University of California, Berkeley, USA

    Sanjit A. Seshia

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Brucker, A.D., Havle, O., Nemouchi, Y., Wolff, B. (2016). Testing the IPC Protocol for a Real-Time Operating System. In: Gurfinkel, A., Seshia, S.A. (eds) Verified Software: Theories, Tools, and Experiments. VSTTE 2015. Lecture Notes in Computer Science(), vol 9593. Springer, Cham. https://doi.org/10.1007/978-3-319-29613-5_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-29613-5_3

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29612-8

  • Online ISBN: 978-3-319-29613-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation