Skip to main content
SpringerLink
Log in

Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus

  • Conference paper
  • First Online:
Dependable Software Engineering. Theories, Tools, and Applications (SETTA 2017)

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

Abstract

Deductive methods for the verification of hybrid systems vary on the format of statements in correctness proofs. Building on the example of Hoare triple-based reasoning, we have investigated several such methods for systems described in Hybrid CSP, each based on a different assertion language, notation for time, and notation for proofs, and each having its pros and cons with respect to expressive power, compositionality and practical convenience. In this paper we propose a new approach based on weakly monotonic time as the semantics for interleaving, the Duration Calculus (DC) with infinite intervals and general fixpoints as the logic language, and a new meaning for Hoare-like triples which unifies assertions and temporal conditions. We include a proof system for reasoning about the properties of systems written in the new form of triples that is complete relative to validity in DC.

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

Notes

  1. 1.

    Hoare style proof rules for a system with ch?x and ch!e appearing as primitive constructs were proposed by Zhou Chaochen et al. in [12]. That work features a different type of triples and follows the convention that process variables are not observable across threads thus ruling out a shared-variable emulation of communication.

References

  1. Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993)

    Article  Google Scholar 

  2. Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832–843 (1983)

    Article  MATH  Google Scholar 

  3. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993). doi:10.1007/3-540-57318-6_30

    Chapter  Google Scholar 

  4. Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. EATCS. Springer, Heidelberg (2004). doi:10.1007/978-3-662-06784-0

    MATH  Google Scholar 

  5. Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  6. Zhou, C., Dang, V.H., Li, X.: A duration calculus with infinite intervals. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 16–41. Springer, Heidelberg (1995). doi:10.1007/3-540-60249-6_39

    Chapter  Google Scholar 

  7. Cau, A., Moszkowski, B., Zedan, H.: ITL web pages. http://www.antonio-cau.co.uk/ITL/

  8. Dutertre, B.: On First-order Interval Temporal Logic. Report CSD-TR-94-3, Department of Computer Science, Royal Holloway, University of London (1995)

    Google Scholar 

  9. Goranko, V., Montanari, A., Sciavicco, G.: A road map of interval temporal logics and duration calculi. J. Appl. Non Classical Logics 14(1–2), 9–54 (2004)

    Article  MATH  Google Scholar 

  10. Guelev, D.P., Hung, D.V.: Prefix and projection onto state in duration calculus. In: Proceedings of TPTS 2002, ENTCS, vol. 65, no. 6. Elsevier Science (2002)

    Google Scholar 

  11. Guelev, D.P., Van Hung, D.: A relatively complete axiomatisation of projection onto state in the duration calculus. J. Appl. Non Class. Logics 14(1–2), 151–182 (2004). Special Issue on Interval Temporal Logics and Duration Calculi

    MATH  Google Scholar 

  12. Guelev, D.P., Wang, S., Zhan, N., Zhou, C.: Super-dense computation in verification of hybrid CSP processes. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 13–22. Springer, Cham (2014). doi:10.1007/978-3-319-07602-7_3

    Google Scholar 

  13. Wang, H., Xu, Q.: Completeness of temporal logics over infinite intervals. Discr. Appl. Math. 136(1), 87–103 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  14. Zhu, H., He, J.: A \(DC\)-based semantics for verilog. Technical report 183, UNU/IIST, P.O. Box 3058, Macau (2000)

    Google Scholar 

  15. Halpern, J.Y., Shoham, Y.: A propositional logic of time intervals. In: Proceedings of LICS 1986, pp. 279–292. IEEE Computer Society Press (1986)

    Google Scholar 

  16. Hansen, M.R., Zhou, C.: Chopping a point. In: BCS-FACS 7th Refinement Workshop, Electronic Workshops in Computing. Springer (1996)

    Google Scholar 

  17. Haxthausen, A.E., Yong, X.: Linking DC together with TRSL. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 25–44. Springer, Heidelberg (2000). doi:10.1007/3-540-40911-4_3

    Chapter  Google Scholar 

  18. He, J., Xu, Q.: Advanced features of duration calculus and their applications in sequential hybrid programs. Formal Asp. Comput. 15(1), 84–99 (2003)

    MATH  Google Scholar 

  19. He, J.: From CSP to hybrid systems. In: Roscoe, A.W. (ed.) A Classical Mind, pp. 171–189. Prentice Hall International (UK) Ltd., Hertfordshire (1994)

    Google Scholar 

  20. Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of LICS 1996, pp. 278–292. IEEE Computer Society Press (1996)

    Google Scholar 

  21. Hooman, J.: Extending Hoare logic to real-time. Formal Asp. Comput. 6(6A), 801–826 (1994)

    Article  MATH  Google Scholar 

  22. Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1–15. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17164-2_1

    Chapter  Google Scholar 

  23. Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Proceedings of EMSOFT 2011, pp. 97–106. ACM (2011)

    Google Scholar 

  24. Manna, Z., Pnueli, A.: Verifying hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 4–35. Springer, Heidelberg (1993). doi:10.1007/3-540-57318-6_22

    Chapter  Google Scholar 

  25. Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417–426 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  26. Moszkowski, B.: Temporal logic for multilevel reasoning about hardware. IEEE Comput. 18(2), 10–19 (1985)

    Article  Google Scholar 

  27. Moszkowski, B.: Executing Temporal Logic Programs. Cambridge University Press, Cambridge (1986). http://www.cse.dmu.ac.uk/~cau/papers/tempura-book.pdf

  28. Olderog, E.-R., Hoare, C.A.R.: Specification-oriented semantics for communicating processes. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 561–572. Springer, Heidelberg (1983). doi:10.1007/BFb0036937

    Chapter  Google Scholar 

  29. Pandya, P.K.: Some extensions to propositional mean-value calculus: expressiveness and decidability. In: Kleine Büning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 434–451. Springer, Heidelberg (1996). doi:10.1007/3-540-61377-3_52

    Chapter  Google Scholar 

  30. Pandya, P.K., Hung, D.: Duration calculus of weakly monotonic time. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 55–64. Springer, Heidelberg (1998). doi:10.1007/BFb0055336

    Chapter  Google Scholar 

  31. Pandya, P.K., Joseph, M.: P - a logic - a compositional proof system for distributed programs. Distrib. Comput. 5, 37–54 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  32. Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143–189 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  33. Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24743-2_32

    Chapter  Google Scholar 

  34. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 539–554. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24743-2_36

    Chapter  Google Scholar 

  35. Venema, Y.: A modal logic for chopping intervals. J. Logic Comput. 1(4), 453–476 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  36. Venema, Y.: Many-dimensional modal logics. Ph.D. thesis, University of Amsterdam (1991)

    Google Scholar 

  37. Wang, S., Zhan, N., Guelev, D.: An assume/guarantee based compositional calculus for hybrid CSP. In: Agrawal, M., Cooper, S.B., Li, A. (eds.) TAMC 2012. LNCS, vol. 7287, pp. 72–83. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29952-0_13

    Chapter  Google Scholar 

  38. Yong, X., George, C.: An operational semantics for timed RAISE. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1008–1027. Springer, Heidelberg (1999). doi:10.1007/3-540-48118-4_4

    Chapter  Google Scholar 

  39. Zhou, C., Wang, J., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 511–530. Springer, Heidelberg (1996). doi:10.1007/BFb0020972

    Chapter  Google Scholar 

Download references

Acknowledgements

Dimitar Guelev was partially supported through Bulgarian NSF Contract DN02/15/19.12.2016. Shuling Wang and Naijun Zhan were partially supported by NSFC under grants 61625206, by “973 Program” under grant No. 2014CB340701, by CDZ project CAP (GZ 1023), and by the CAS/SAFEA International Partnership Program for Creative Research Teams.

Author information

Authors and Affiliations

  1. Institute of Mathematics and Informatics, Bulgarian Academy of Sciences, Sofia, Bulgaria

    Dimitar P. Guelev

  2. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Shuling Wang & Naijun Zhan

  3. University of Chinese Academy of Sciences, Beijing, China

    Naijun Zhan

Authors
  1. Dimitar P. Guelev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shuling Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Naijun Zhan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dimitar P. Guelev .

Editor information

Editors and Affiliations

  1. Aalborg University, Aalborg, Denmark

    Kim Guldstrand Larsen

  2. University of Pennsylvania, Philadelphia, Pennsylvania, USA

    Oleg Sokolsky

  3. National University of Defense Technology, Changsha, China

    Ji Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Guelev, D.P., Wang, S., Zhan, N. (2017). Compositional Hoare-Style Reasoning About Hybrid CSP in the Duration Calculus. In: Larsen, K., Sokolsky, O., Wang, J. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2017. Lecture Notes in Computer Science(), vol 10606. Springer, Cham. https://doi.org/10.1007/978-3-319-69483-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-69483-2_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-69482-5

  • Online ISBN: 978-3-319-69483-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation