Skip to main content
SpringerLink
Log in
Book cover

International Conference on Reliability, Safety, and Security of Railway Systems

RSSRail 2016: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification pp 215–230Cite as

Abstract Software Specifications and Automatic Proof of Refinement

  • Conference paper
  • First Online:

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

Abstract

It is common practice in critical software development, and compulsory in railway software developed according to EN 50128 standard, to separate software specification from software implementation. Verification activities should be performed to ensure that the latter is a correct refinement of the former. When the specification is formalized, for example in B method, the refinement relation can even be formally proved. In this article, we present how a similar proof of refinement can be performed at the level of the programming language used for implementation, using the SPARK technology. We describe two techniques to specify abstractly the behavior of a software component in terms of mathematical structures (sequences, sets and maps) and a methodology based on the SPARK tools to prove automatically that an efficient imperative implementation is a correct refinement of the abstract specification.

Work partly supported by the Joint Laboratory ProofInUse (ANR-13-LAB3-0007, http://www.spark-2014.org/proofinuse) and project VECOLIB (ANR-14-CE28-0018) of the French national research organization.

This is a preview of subscription content, 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 EPUB and 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

Learn about institutional subscriptions

Notes

  1. 1.

    http://www.adacore.com/codepeer.

  2. 2.

    http://www.adacore.com/gnatpro/toolsuite/gps/.

  3. 3.

    http://www.adacore.com/gnatpro/toolsuite/gnatbench/.

  4. 4.

    http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html#ghost-code.

  5. 5.

    http://docs.adacore.com/spark2014-docs/html/lrm/subprograms.html#ghost-entities.

  6. 6.

    The results presented in this article can be reproduced with SPARK GPL 2016, which will be available in June 2016 at http://libre.adacore.com. The source code of the examples is available in the SPARK public repository at https://forge.open-do.org/anonscm/git/spark2014/spark2014.git, under testsuite/gnatprove/tests/allocators.

References

  1. EN 50128:2011 railway applications - communication, signalling and processing systems - software for railway control and protection systems (2011)

    Google Scholar 

  2. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  3. Abrial, J.-R.: Formal methods in industry: achievements, problems, future. In: Proceedings of the 28th International Conference on Software Engineering, ICSE 2006, pp. 761–768. ACM, New York (2006)

    Google Scholar 

  4. Barnes, J.: Ada 2012 Rationale (2012)

    Google Scholar 

  5. Barnes, J.: SPARK: The Proven Approach to High Integrity Software. Altran Praxis (2012)

    Google Scholar 

  6. Boulanger, J.-L. (ed.): Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method. Wiley, New York (2014)

    Google Scholar 

  7. Burdy, L., Meynadier, J.-M.: Automatic refinement. In: FM 1999 Workshop - Applying B in an Industrial Context: Tools, Lessons and Techniques (1999)

    Google Scholar 

  8. Chalin, P.: Engineering a sound assertion semantics for the verifying compiler. IEEE Trans. Softw. Eng. 36(2), 275–287 (2010)

    Article  Google Scholar 

  9. Clarke, D., Noble, J., Wrigstad, T. (eds.): Aliasing in Object-Oriented Programming: Types, Analysis, and Verification. Springer, Heidelberg (2013)

    Google Scholar 

  10. Comar, C., Kanig, J., Moy, Y.: Integrating formal program verification with testing. In: Proceedings of ERTS (2012)

    Google Scholar 

  11. Delahaye, D., Dubois, C., Marché, C., Mentré, D.: The BWare project: building a proof platform for the automated verification of B proof obligations. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 290–293. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  12. Dross, C., Efstathopoulos, P., Lesens, D., Mentré, D., Moy, Y.: Rail, space, security: three case studies for SPARK 2014. In: Proceedings of ERTS (2014)

    Google Scholar 

  13. Dross, C., Fumex, C., Gerlach, J., Marché, C.: High-level functional properties of bit-level programs: formal specifications and automated proofs. Research Report 8821, Inria, December 2015

    Google Scholar 

  14. Huisman, M., Klebanov, V., Monahan, R. (eds.): Int. J. Softw. Tools Technol. Transf., special issue, VerifyThis 2012, vol. 17 (2015)

    Google Scholar 

  15. Koenig, J., Leino, K.R.M.: Programming language features for refinement. Submitted to EPTCS (2015)

    Google Scholar 

  16. Lammich, P.: Refinement based verification of imperative data structures. In: Proceedings of the Conference on Certified Programs and Proofs (2016)

    Google Scholar 

  17. Ledinot, E., Blanquart, J.-P., Astruc, J.-M., Baufreton, P., Boulanger, J.-L., Comar, C., Delseny, H., Gassino, J., Leeman, M., Quéré, P., Ricque, B.: Joint use of static and dynamic software verification techniques: a cross-domain view in safety critical system industries. In: Proceedings of the 7th European Congress on Embedded Real Time Software and Systems (ERTS\(^2\) 2014), Toulouse, France, 5–7 February, 2014

    Google Scholar 

  18. Marché, C.: Verification of the functional behavior of a floating-point program: an industrial case study. Sci. Comput. Program. 96(3), 279–296 (2014)

    Article  MathSciNet  Google Scholar 

  19. McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)

    Book  MATH  Google Scholar 

  20. Meyer, B.: Object-Oriented Software Construction, 1st edn. Prentice-Hall Inc., Upper Saddle River (1988)

    MATH  Google Scholar 

  21. O’Neill, I.: SPARK - a language and tool-set for high-integrity software development. In: Industrial Use of Formal Methods: Formal Verification. Wiley (2012)

    Google Scholar 

  22. Ostroff, J., wei Wang, C., Kerfoot, E., Torshizi, F.A.: ES-verify: a tool for automated model-based verification of object-oriented code. In: Formal Methods 2006. Poster (2006)

    Google Scholar 

  23. Tafat, A., Boulmé, S., Marché, C.: A refinement methodology for object-oriented programs. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 153–167. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

Download references

Acknowledgements

We would like to thank Claude Marché, David Mentré, Piotr Trojanek as well as the anonymous reviewers for their useful comments.

Author information

Authors and Affiliations

  1. AdaCore, 46 Rue d’Amsterdam, 75009, Paris, France

    Claire Dross & Yannick Moy

Authors
  1. Claire Dross
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yannick Moy
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yannick Moy .

Editor information

Editors and Affiliations

  1. ClearSy, Aix en Provence, France

    Thierry Lecomte

  2. Siemens AG, Braunschweig, Niedersachsen, Germany

    Ralf Pinger

  3. Newcastle University, Newcastle upon Tyne, United Kingdom

    Alexander Romanovsky

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Dross, C., Moy, Y. (2016). Abstract Software Specifications and Automatic Proof of Refinement. In: Lecomte, T., Pinger, R., Romanovsky, A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2016. Lecture Notes in Computer Science(), vol 9707. Springer, Cham. https://doi.org/10.1007/978-3-319-33951-1_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-33951-1_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-33950-4

  • Online ISBN: 978-3-319-33951-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation