Skip to main content
SpringerLink
Log in

Verification Architectures: Compositional Reasoning for Real-Time Systems

  • Conference paper
Integrated Formal Methods (IFM 2010)

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

Included in the following conference series:

Abstract

We introduce a conceptual approach to decompose real-time systems, specified by integrated formalisms: instead of showing safety of a system directly, one proves that it is an instance of a Verification Architecture, a safe behavioural protocol with unknowns and local real-time assumptions. We examine how different verification techniques can be combined in a uniform framework to reason about protocols, assumptions, and instantiations of protocols. The protocols are specified in CSP, extended by data and unknown processes with local assumptions in a real-time logic. To prove desired properties, the CSP dialect is embedded into dynamic logic and a sequent calculus is presented. Further, we analyse the instantiation of protocols by combined specifications, here illustrated by CSP-OZ-DC. Using an example, we show that this approach helps us verify specifications that are too complex for direct verification.

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

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  2. Butler, M.J.: A CSP Approach To Action Systems. Ph.D. thesis, University of Oxford (1992)

    Google Scholar 

  3. Damm, W., Hungar, H., Olderog, E.R.: Verification of cooperating traffic agents. Int. J. Control. 79(5), 395–421 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  4. de Roever, W.P., et al.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge (2001)

    MATH  Google Scholar 

  5. D’Errico, L., Loreti, M.: Assume-Guarantee Verification of Concurrent Systems. In: Field, J., Vasconcelos, V.T. (eds.) COORDINATION 2009. LNCS, vol. 5521, pp. 288–305. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed patterns: TCOZ to timed automata. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 483–498. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. ERTMS User Group, UNISIG: ERTMS/ETCS System requirements specification (2002), http://www.aeif.org/ccm/default.asp (version 2.2.2)

  8. Faber, J., Jacobs, S., Sofronie-Stokkermans, V.: Verifying CSP-OZ-DC specifications with complex data types and timing parameters. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 233–252. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Faber, J.: Verification Architectures: Compositional reasoning for real-time systems. Reports of SFB/TR 14 AVACS 65 (2010), http://www.avacs.org

  10. Fischer, C.: Combination and Implementation of Processes and Data: from CSP-OZ to Java. Ph.D. thesis, University of Oldenburg (2000)

    Google Scholar 

  11. Gentzen, G.: Untersuchungen über das logisches Schließen. Mathematische Zeitschrift 1, 176–210 (1935)

    Article  MathSciNet  MATH  Google Scholar 

  12. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  13. He, J.: Process simulation and refinement. Form. Asp. Comput. 1(3), 229–241 (1989)

    MATH  Google Scholar 

  14. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International, Englewood Cliffs (1985)

    MATH  Google Scholar 

  15. Hoenicke, J.: Combination of Processes, Data and Time. Ph.D. thesis, University of Oldenburg (2006)

    Google Scholar 

  16. Klebanov, V., Rümmer, P., Schlager, S., Schmitt, P.H.: Verification of JCSP programs. In: Broenink, J.F., Roebbers, H.W., Sunter, J.P.E., Welch, P.H., Wood, D.C. (eds.) CPA. CSES, vol. 63, pp. 203–218. IOS Press, Amsterdam (2005)

    Google Scholar 

  17. Knudsen, J., Ravn, A.P., Skou, A.: Design verification patterns. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol. 4700, pp. 399–413. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Larsen, K.G., Xinxin, L.: Compositionality through an operational semantics of contexts. J. Log. Comput. 1(6), 761–795 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  19. Mahony, B.P., Dong, J.S.: Blending object-Z and timed CSP: An introduction to TCOZ. In: ICSE, pp. 95–104 (1998)

    Google Scholar 

  20. Metzler, B., Wehrheim, H., Wonisch, D.: Decomposition for compositional verification. In: Liu, S., Maibaum, T.S.E., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 105–125. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Meyer, R., Faber, J., Hoenicke, J., Rybalchenko, A.: Model checking duration calculus: A practical approach. Form. Asp. Comput. 20(4-5), 481–505 (2008)

    Article  MATH  Google Scholar 

  22. Platzer, A.: A temporal dynamic logic for verifying hybrid system invariants. In: Artemov, S., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 457–471. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  23. Platzer, A., Quesel, J.D.: Logical verification and systematic parametric analysis in train control. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 646–649. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  24. Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  25. RAISE Language Group: The RAISE Specification Language. BCS Practitioner Series. Prentice Hall International, Englewood Cliffs (1992)

    Google Scholar 

  26. Roscoe, A.: Theory and Practice of Concurrency. Prentice Hall International, Englewood Cliffs (1998)

    Google Scholar 

  27. Smith, G.: An integration of real-time object-Z and CSP for specifying concurrent real-time systems. In: Butler, M.J., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 267–285. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  28. Sühl, C.: An overview of the integrated formalism RT-Z. Form. Asp. Comput. 13(2), 94–110 (2002)

    Article  MATH  Google Scholar 

  29. Sun, J., Liu, Y., Dong, J.S.: Model checking CSP revisited: Introducing a process analysis toolkit. In: ISoLA 2008. CCIS, vol. 17, pp. 307–322. Springer, Heidelberg (2008)

    Google Scholar 

  30. Taibi, T.: Design Pattern Formalization Techniques. IGI Publishing (2007)

    Google Scholar 

  31. Wehrheim, H.: Behavioural subtyping in object-oriented specification formalisms. University of Oldenburg, Habilitation (2002)

    Google Scholar 

  32. Woodcock, J.C.P., Cavalcanti, A.L.C.: A concurrent language for refinement. In: Butterfield, A., Pahl, C. (eds.) IWFM 2001. BCS Elec. Works. in Computing (2001)

    Google Scholar 

  33. Zhou, C., Hansen, M.R.: Duration Calculus. Springer, Heidelberg (2004)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Oldenburg, Germany

    Johannes Faber

Authors
  1. Johannes Faber
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. INRIA Nancy-Grand Est & LORIA, Bâtiment B, équipe MOSEL, 615 rue du Jardin Botanique, 54602, Villers-lès-Nancy cédex, France

    Dominique Méry  & Stephan Merz  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Faber, J. (2010). Verification Architectures: Compositional Reasoning for Real-Time Systems. In: Méry, D., Merz, S. (eds) Integrated Formal Methods. IFM 2010. Lecture Notes in Computer Science, vol 6396. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16265-7_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16265-7_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16264-0

  • Online ISBN: 978-3-642-16265-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation