Abstract
In this paper, we investigate how to formalize and verify the System Requirements Specification (SRS) of Chinese Train Control System Level 3 (CTCS-3), which includes a set of basic operational scenarios that cooperate with each other to achieve the desired behavior of trains. It is absolutely necessary to prove that the cooperation of basic scenarios indeed completes the required behavior. As a case study, a combined scenario with several basic scenarios integrated is studied in this paper. We model each scenario as a Hybrid CSP (HCSP) process, and specify its properties using Hybrid Hoare Logic (HHL). Given such an annotated HCSP model, the deductive verification of conformance of the model to the properties is then carried out. For the purpose, we implement a theorem prover of HHL in Isabelle/HOL, with which the process including modelling and verification of annotated HCSP models can be mechanized. In particular, we provide a machine-checked proof for the combined scenario, with the result indicating a design error in SRS of CTCS-3.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
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
Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993)
He, J.: From CSP to hybrid systems. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 171–189. Prentice Hall International (UK) Ltd. (1994)
Heilmann, S.T.: Proof Support for Duration Calculus. PhD thesis, Technical University of Denmark (1999)
Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278–292. IEEE Computer Society (1996)
Hoenicke, J., Olderog, E.: CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nord. J. Comput. 9(4), 301–334 (2002)
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)
Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT 2011, pp. 97–106. ACM (2011)
Manna, Z., Pnueli, A.: Verifying hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 4–35. Springer, Heidelberg (1993)
Manna, Z., Sipma, H.: Deductive verification of hybrid systems using STeP. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol. 1386, pp. 305–318. Springer, Heidelberg (1998)
Moszkowski, B.C., Manna, Z.: Reasoning in interval temporal logic. In: Clarke, E., Kozen, D. (eds.) Logic of Programs, vol. 164, pp. 371–382. Springer, Heidelberg (1983)
Platzer, A.: Differential dynamic logic for hybrid systems. Journal of Automated Reasoning 41(2), 143–189 (2008)
Platzer, A., Quesel, J.: European train control system: A case study in formal verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 246–265. Springer, Heidelberg (2009)
Rasmussen, T.M.: Interval Logic - Proof Theory and Theorem Proving. PhD thesis, Technical University of Denmark (2002)
Skakkebaek, J.U., Shankar, N.: Towards a duration calculus proof assistant in PVS. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 660–679. Springer, Heidelberg (1994)
Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 305–320. Springer, Heidelberg (2004)
Zhang, S.: CTCS-3 Technology Specification. China Railway Publishing House (2008)
Zhou, C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Series: Monographs in Theoretical Computer Science. An EATCS Series. Springer (2004)
Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Zhou, C., Li, X.: A mean-value duration calculus. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, pp. 432–451. Prentice-Hall International (1994)
Zhou, C., Wang, J., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 511–530. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zou, L. et al. (2014). Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving. In: Cohen, E., Rybalchenko, A. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2013. Lecture Notes in Computer Science, vol 8164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54108-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-54108-7_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54107-0
Online ISBN: 978-3-642-54108-7
eBook Packages: Computer ScienceComputer Science (R0)