Abstract
We extend existing verification methods for CSP-OZ-DC to reason about real-time systems with complex data types and timing parameters. We show that important properties of systems can be encoded in well-behaved logical theories in which hierarchic reasoning is possible. Thus, testing invariants and bounded model checking can be reduced to checking satisfiability of ground formulae over a simple base theory. We illustrate the ideas by means of a simplified version of a case study from the European Train Control System standard.
This work was partly supported by the German Research Council (DFG) under grant SFB/TR 14 AVACS. See http://www.avacs.org for more information.
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.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
ERTMS User Group, UNISIG. ERTMS/ETCS System requirements specification. Version 2.2.2 (2002), http://www.aeif.org/ccm/default.asp
Faber, J., Meyer, R.: Model checking data-dependent real-time properties of the European Train Control System. In: FMCAD, pp. 76–77. IEEE Computer Society Press, Los Alamitos (2006)
Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning 33(3-4), 221–249 (2004)
Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Information and Computation 204(10), 1453–1492 (2006)
Hermanns, H., Jansen, D.N., Usenko, Y.S.: From StoCharts to MoDeST: a comparative reliability analysis of train radio communications. In: Workshop on Software and Performance, pp. 13–23. ACM Press, New York (2005)
Hoenicke, J., Maier, P.: Model-checking of specifications integrating processes, data and time. In: Fitzgerald, J.A., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, Springer, Heidelberg (2005)
Hoenicke, J., Olderog, E.-R.: CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic Journal of Computing 9(4), 301–334 (2003)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Hoenicke, J.: Combination of Processes, Data, and Time. PhD thesis, University of Oldenburg, Germany (2006)
Jacobs, S., Sofronie-Stokkermans, V.: Applications of hierarchic reasoning in the verification of complex systems. ENTCS (special issue dedicated to PDPAR 2006), 15 pages (to appear, 2007)
Mahony, B.P., Dong, J.S.: Overview of the semantics of TCOZ. In: IFM, pp. 66–85. Springer, Heidelberg (1999)
Meyer, R., Faber, J., Rybalchenko, A.: Model checking duration calculus: A practical approach. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 332–346. Springer, Heidelberg (2006)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS 1(2), 245–257 (1979)
Roscoe, A.W.: Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)
Smith, G.: The Object Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)
Smith, G.: An integration of real-time Object-Z and CSP for specifying concurrent real-time systems. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 267–285. Springer, Heidelberg (2002)
Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) Automated Deduction – CADE-20. LNCS (LNAI), vol. 3632, pp. 219–234. Springer, Heidelberg (2005)
Sofronie-Stokkermans, V.: Interpolation in local theory extensions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 235–250. Springer, Heidelberg (2006)
Sühl, C.: An overview of the integrated formalism RT-Z. Formal Asp. Comput 13(2), 94–110 (2002)
Trowitzsch, J., Zimmermann, A.: Using UML state machines and petri nets for the quantitative investigation of ETCS. In: VALUETOOLS, pp. 1–34. ACM Press, New York (2006)
Zhou, C., Hansen, M.R.: Duration Calculus. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Faber, J., Jacobs, S., Sofronie-Stokkermans, V. (2007). Verifying CSP-OZ-DC Specifications with Complex Data Types and Timing Parameters. In: Davies, J., Gibbons, J. (eds) Integrated Formal Methods. IFM 2007. Lecture Notes in Computer Science, vol 4591. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73210-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-73210-5_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73209-9
Online ISBN: 978-3-540-73210-5
eBook Packages: Computer ScienceComputer Science (R0)