Skip to main content
SpringerLink
Log in

A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems

  • Conference paper
  • First Online:
Formal Methods – The Next 30 Years (FM 2019)

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

Included in the following conference series:

Abstract

Reactive systems are composed of a well defined set of event handlers by which the system responds to environment stimulus. In concurrent environments, event handlers can interact with the execution of other handlers such as hardware interruptions in preemptive systems, or other instances of the reactive system in multicore architectures. The rely-guarantee technique is a suitable approach for the specification and verification of reactive systems. However, the languages in existing rely-guarantee implementations are designed only for “pure programs”, simulating reactive systems makes the program and rely-guarantee conditions unnecessary complicated. In this paper, we decouple the system reactions and programs using a rely-guarantee interface, and develop PiCore, a parametric rely-guarantee framework for concurrent reactive systems. PiCore has a two-level inference system to reason on events and programs associated to events. The rely-guarantee interface between the two levels allows the reusability of existing languages and their rely-guarantee proof systems for programs. In this work we show how to integrate in PiCore two existing rely-guarantee proof systems. This work has been fully mechanized in Isabelle/HOL. As a case study, we have applied PiCore to the concurrent buddy memory allocation of a real-world OS, providing a verified low-level specification and revealing bugs in the C code.

This work has been supported in part by the National Natural Science Foundation of China (NSFC) under the Grant No.61872016, and the National Satellite of Excellence in Trustworthy Software Systems and the Award No. NRF2014NCR-NCR001-30, funded by NRF Singapore under National Cyber-security R&D (NCR) programme.

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. The Zephyr Project. https://www.zephyrproject.org/. Accessed December 2018

  2. Abrial, J.R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to event-B. Fundamenta Informaticae 77(1–2), 1–28 (2007)

    MathSciNet  MATH  Google Scholar 

  3. Aceto, L., Ingólfsdóttir, A., Larsen, K., Srba, J.: Reactive Systems - Modeling, Specification and Verification. Cambridge University Press, Cambridge (2007)

    Book  Google Scholar 

  4. Andronick, J., Lewis, C., Morgan, C.: Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system. In: Proceedings Workshop on Models for Formal Analysis of Real Systems MARS, pp. 10–24 (2015)

    Google Scholar 

  5. Back, R.J., Sere, K.: Superposition Refinement of Reactive Systems. Formal Aspects Comput. 8(3), 324–346 (1996)

    Article  Google Scholar 

  6. Back, R.J., Sere, K.: Stepwise refinement of action systems. Struct. Program. 12, 17–30 (1991)

    Google Scholar 

  7. Chen, H., Wu, X., Shao, Z., Lockerman, J., Gu, R.: Toward compositional verification of interruptible OS kernels and device drivers. In: 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 431–447. ACM (2016)

    Google Scholar 

  8. Dingel, J., Garlan, D., Jha, S., Notkin, D.: Towards a formal treatment of implicit invocation using rely/guarantee reasoning. Formal Aspects Comput. 10(3), 193–213 (1998)

    Article  Google Scholar 

  9. Fenkam, P., Gall, H., Jazayeri, M.: Composing specifications of event based applications. In: Pezzè, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 67–86. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36578-8_6

    Chapter  Google Scholar 

  10. Fenkam, P., Gall, H., Jazayeri, M.: Constructing deadlock free event-based applications: a rely/guarantee approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 636–657. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_35

    Chapter  Google Scholar 

  11. Garlan, D., Jha, S., Notkin, D., Dingel, J.: Reasoning about implicit invocation. In: Proceedings of the 6th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pp. 209–221. ACM, New York (1998)

    Google Scholar 

  12. Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 13, pp. 477–498. Springer, Heidelberg (1985). https://doi.org/10.1007/978-3-642-82453-1_17

    Chapter  Google Scholar 

  13. Hayes, I.J.: Generalised rely-guarantee concurrency: an algebraic foundation. Formal Aspects Comput. 28(6), 1057–1078 (2016)

    Article  MathSciNet  Google Scholar 

  14. Hayes, I.J., Colvin, R.J., Meinicke, L.A., Winter, K., Velykis, A.: An algebra of synchronous atomic steps. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 352–369. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_22

    Chapter  Google Scholar 

  15. Hoang, T.S., Abrial, J.-R.: Event-B decomposition for parallel programs. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 319–333. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11811-1_24

    Chapter  Google Scholar 

  16. Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)

    Article  Google Scholar 

  17. Klein, G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009, Big Sky, Montana, USA, pp. 207–220. ACM Press (2009)

    Google Scholar 

  18. Liang, H., Feng, X., Fu, M.: A rely-guarantee-based simulation for verifying concurrent program transformations. In: 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 455–468. ACM Press (2012)

    Google Scholar 

  19. Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: 24th Computer Security Foundations Symposium (CSF), pp. 218–232. IEEE Press (2011)

    Google Scholar 

  20. Moreira, N., Pereira, D., de Sousa, S.M.: On the mechanisation of rely-guarantee in Coq. Universidade do Porto, Technical report (2013)

    Google Scholar 

  21. Murray, T., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 126–142. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35308-6_12

    Chapter  Google Scholar 

  22. Murray, T., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: 29th IEEE Computer Security Foundations Symposium (CSF). IEEE Press (2016)

    Google Scholar 

  23. Nieto, L.P.: The rely-guarantee method in Isabelle/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 348–362. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36575-3_24

    Chapter  Google Scholar 

  24. Sanán, D., Zhao, Y., Hou, Z., Zhang, F., Tiu, A., Liu, Y.: CSimpl: a rely-guarantee-based framework for verifying concurrent programs. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 481–498. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_28

    Chapter  Google Scholar 

  25. Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle/HOL. Ph.D. thesis, Technical University Munich (2006)

    Google Scholar 

  26. van Staden, S.: On rely-guarantee reasoning. In: Hinze, R., Voigtländer, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 30–49. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19797-5_2

    Chapter  Google Scholar 

  27. Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 59–79. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_4

    Chapter  Google Scholar 

  28. Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput. 9(2), 149–174 (1997)

    Article  Google Scholar 

  29. Zhao, Y., Sanán, D.: Rely-guarantee reasoning about concurrent memory management in Zephyr RTOS. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 515–533. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25543-5_29

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Engineering, Beihang University, Beijing, China

    Yongwang Zhao

  2. Beijing Advanced Innovation Center for Big Data and Brain Computing, Beihang University, Beijing, China

    Yongwang Zhao

  3. School of Computer Science and Engineering, Nanyang Technological University, Singapore, Singapore

    David Sanán & Yang Liu

  4. MPI-SWS, Kaiserslautern, Germany

    Fuyuan Zhang

Authors
  1. Yongwang Zhao
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Sanán
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Fuyuan Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yang Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yongwang Zhao .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zhao, Y., Sanán, D., Zhang, F., Liu, Y. (2019). A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30942-8_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30941-1

  • Online ISBN: 978-3-030-30942-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation