Abstract
Model checking of real-time systems with respect to Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. This task is difficult to automate. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to real world applications. Our algorithm significantly extends the subset of DC that can be handled. It decomposes DC specifications into sub-properties that can be verified independently. The decomposition bases on a novel distributive law for DC. We implemented the algorithm as part of our tool chain for the automated verification of systems comprising data, communication, and real-time aspects. Our translation facilitated a successful application of the tool chain on an industrial case study from the European Train Control System (ETCS).
This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS) and the Graduate School “TrustSoft” (GRK 1076/1). See http://www.avacs.org and http://www.trustsoft.org .
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.G.: The power of reachability testing for timed automata. Theoretical Computer Science 300(1-3), 411–475 (2003)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Bouajjani, A., Lakhnech, Y., Robbana, R.: From duration calculus to linear hybrid automata. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 196–210. Springer, Heidelberg (1995)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Dierks, H., Lettrari, M.: Constructing test automata from graphical real-time requirements. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 433–453. Springer, Heidelberg (2002)
ERTMS User Group, UNISIG. ERTMS/ETCS System requirements specification. Version 2.2.2 (2002), http://www.aeif.org/ccm/default.asp
Fränzle, M.: Model-checking dense-time duration calculus. Formal Aspects of Computing 16(2), 121–139 (2004)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Hansen, M.: DC with nominals. Personal communication (March 2006)
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232–244. ACM Press, New York (2004)
Hermanns, H., Jansen, D.N., Usenko, Y.S.: From StoCharts to MoDeST: a comparative reliability analysis of train radio communications. In: WOSP, pp. 13–23. ACM Press, New York (2005)
Hoenicke, J., Maier, P.: Model-checking of specifications integrating processes, data and time. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 465–480. Springer, Heidelberg (2005)
Hoenicke, J., Meyer, R., Faber, J.: PEA toolkit home page (2006), http://csd.informatik.uni-oldenburg.de/projects/epea.html
Hoenicke, J., Olderog, E.-R.: CSP-OZ-DC: A combination of specification techniques for processes, data and time. NJC 9 (2002)
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 (to appear, 2006)
Krishna, S.N., Pandya, P.K.: Modal strength reduction in quantified discrete duration calculus. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 444–456. Springer, Heidelberg (2005)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
Pandya, P.K.: Interval duration logic: Expressiveness and decidability. ENTCS 65(6) (2002)
Ravn, A.P.: Design of Embedded Real-Time Computing Systems. PhD thesis, Technical University of Denmark (1994)
Rybalchenko, A.: ARMC (2006), http://www.mpi-inf.mpg.de/~rybal/armc
Smith, G.: The Object-Z Specification Language. Kluwer, Dordrecht (2000)
Uppaal home page. University of Aalborg and University of Uppsala (1995-2005), http://www.uppaal.com
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 332–344 (1986)
Zhou, C., Hansen, M.R.: Duration Calculus. Springer, Heidelberg (2004)
Zimmermann, A., Hommel, G.: Towards modeling and evaluation of ETCS real-time communication and operation. JSS 77(1), 47–54 (2005)
Zhou, C., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: STACS 1993. LNCS, vol. 665, pp. 58–68. Springer, Heidelberg (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meyer, R., Faber, J., Rybalchenko, A. (2006). Model Checking Duration Calculus: A Practical Approach. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds) Theoretical Aspects of Computing - ICTAC 2006. ICTAC 2006. Lecture Notes in Computer Science, vol 4281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11921240_23
Download citation
DOI: https://doi.org/10.1007/11921240_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48815-6
Online ISBN: 978-3-540-48816-3
eBook Packages: Computer ScienceComputer Science (R0)