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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 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
Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993)
Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832–843 (1983)
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
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
Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)
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
Cau, A., Moszkowski, B., Zedan, H.: ITL web pages. http://www.antonio-cau.co.uk/ITL/
Dutertre, B.: On First-order Interval Temporal Logic. Report CSD-TR-94-3, Department of Computer Science, Royal Holloway, University of London (1995)
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)
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)
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
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
Wang, H., Xu, Q.: Completeness of temporal logics over infinite intervals. Discr. Appl. Math. 136(1), 87–103 (2004)
Zhu, H., He, J.: A \(DC\)-based semantics for verilog. Technical report 183, UNU/IIST, P.O. Box 3058, Macau (2000)
Halpern, J.Y., Shoham, Y.: A propositional logic of time intervals. In: Proceedings of LICS 1986, pp. 279–292. IEEE Computer Society Press (1986)
Hansen, M.R., Zhou, C.: Chopping a point. In: BCS-FACS 7th Refinement Workshop, Electronic Workshops in Computing. Springer (1996)
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
He, J., Xu, Q.: Advanced features of duration calculus and their applications in sequential hybrid programs. Formal Asp. Comput. 15(1), 84–99 (2003)
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)
Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of LICS 1996, pp. 278–292. IEEE Computer Society Press (1996)
Hooman, J.: Extending Hoare logic to real-time. Formal Asp. Comput. 6(6A), 801–826 (1994)
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
Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Proceedings of EMSOFT 2011, pp. 97–106. ACM (2011)
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
Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417–426 (1981)
Moszkowski, B.: Temporal logic for multilevel reasoning about hardware. IEEE Comput. 18(2), 10–19 (1985)
Moszkowski, B.: Executing Temporal Logic Programs. Cambridge University Press, Cambridge (1986). http://www.cse.dmu.ac.uk/~cau/papers/tempura-book.pdf
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
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
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
Pandya, P.K., Joseph, M.: P - a logic - a compositional proof system for distributed programs. Distrib. Comput. 5, 37–54 (1991)
Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143–189 (2008)
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
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
Venema, Y.: A modal logic for chopping intervals. J. Logic Comput. 1(4), 453–476 (1991)
Venema, Y.: Many-dimensional modal logics. Ph.D. thesis, University of Amsterdam (1991)
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
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
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
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
Corresponding author
Editor information
Editors and Affiliations
Rights 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)