Skip to main content
SpringerLink
Log in

Formal Specification and Automated Verification of Safety-Critical Requirements of a Railway Vehicle with Frama-C/Jessie

  • Conference paper
  • First Online:
FORMS/FORMAT 2010

Abstract

Formal verification of software provides a higher level of assurance than classical software testing. In this paper, we report on our experience with the Frama-C/Jessie verification tool in the railway domain. We analyse safety-critical requirements of a railway vehicle, formalize them using the ANSI/ISO-C Specification Language (ACSL) and achieve automated proofs to verify that the implementation satisfies the formal specification. The main requirement for the successful application of Frama-C in the railway domain is its qualification according to EN 50128.

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 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover 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. CEA LIST, Laboratory of Applied Research on Software-Intensive Technologies, http://www-list.cea.fr/gb/index_gb.htm

  2. Marché, C., Moy, Y.: Jessie Plugin Tutorial, Boron Version, http://frama-c.com/jessie/jessie-tutorial.pdf, (2010)

  3. Baudin, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, Version 1.4, http://framac.cea.fr/download/acsl_1.4.pdf, (2009)

  4. Souyris, J., Favre-Felix, D.: Proof of properties in avionics, IFIP Congress Topical Sessions, pages 527-536, (2004)

    Google Scholar 

  5. Jim Woodcock, et al.: Formal Methods: Practice and Experience, ACM Computing Surveys, Volume 41, Issue 4 (October 2009)

    Google Scholar 

  6. Burghardt, J., Gerlach, J., Hartig, K., Soto, J., Weber, C.: ACSL By Example, Towards a Verified C Standard Library, http://www.first.fraunhofer.de/owx_download/acsl-by-example-5_1_0.pdf, (2010)

  7. Correnson, L., Cuoq, P., Puccetti, A., Signoles, J.: Frama-C User Manual, Boron Release, http://frama-c.com/download/user-manual-Boron-20100401.pdf, (2010)

  8. Alt-Ergo Theorem Prover, http://alt-ergo.lri.fr/.

  9. Barrett, C., Tinelli, C.: CVC3, In Proceedings of the 19th International Conference on Computer Aided Verification (CAV’07), Volume 4590 of Lecture Notes in Computer Science, pages 298-302, (2007)

    Google Scholar 

  10. Simplify Theorem Prover, http://secure.ucd.ie/products/opensource/Simplify/.

  11. Dutertre, B., de Moura, L.: The YICES SMT Solver, http://yices.csl.sri.com/tool-paper.pdf

  12. de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver, Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary, http://research.microsoft.com/projects/z3/z3.pdf, (2008)

Download references

Acknowledgments

This work was completed within the DEVICE-SOFT project, which is supported by the Programme Inter Carnot Fraunhofer of the Federal Ministry of Education and Research (BMBF) (Grant 01SF0804) and the Agence Nationale de la Recherche (ANR).

Author information

Authors and Affiliations

  1. Fraunhofer FIRST, Berlin, Germany

    Kerstin Hartig, Jens Gerlach & Juan Soto

  2. Institute of Railway Technology, IfB GmbH, Berlin, Germany

    Jürgen Busse

Authors
  1. Kerstin Hartig
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jens Gerlach
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Juan Soto
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jürgen Busse
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kerstin Hartig .

Editor information

Editors and Affiliations

  1. FB 7 Maschinenbau, LS Regelungs- und, TU Braunschweig, Langer Kamp 8, Braunschweig, 38106, Germany

    Eckehard Schnieder

  2. , Department of Control and Transport, Budapest University of Technology and Ec, Bertalan L.u.2., Budapest, 1111, Hungary

    Geza Tarnai

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hartig, K., Gerlach, J., Soto, J., Busse, J. (2011). Formal Specification and Automated Verification of Safety-Critical Requirements of a Railway Vehicle with Frama-C/Jessie. In: Schnieder, E., Tarnai, G. (eds) FORMS/FORMAT 2010. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14261-1_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14261-1_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14260-4

  • Online ISBN: 978-3-642-14261-1

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation