Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
The Risk Assessment of ERTMS-Based Railway Systems from a Cyber Security Perspective: Methodology and Lessons Learned Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Abstract Software Specifications and Automatic Proof of Refinement

verfasst von : Claire Dross, Yannick Moy

Erschienen in: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel The PERF Approach for Formal Verification
Nächstes Kapitel S3: Proving the Safety of Critical Systems
Fußnoten
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.
 
Literatur
1.
EN 50128:2011 railway applications - communication, signalling and processing systems - software for railway control and protection systems (2011)
2.
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefMATH
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)
4.
Barnes, J.: Ada 2012 Rationale (2012)
5.
Barnes, J.: SPARK: The Proven Approach to High Integrity Software. Altran Praxis (2012)
6.
Boulanger, J.-L. (ed.): Formal Methods Applied to Industrial Complex Systems: Implementation of the B Method. Wiley, New York (2014)
7.
Burdy, L., Meynadier, J.-M.: Automatic refinement. In: FM 1999 Workshop - Applying B in an Industrial Context: Tools, Lessons and Techniques (1999)
8.
Chalin, P.: Engineering a sound assertion semantics for the verifying compiler. IEEE Trans. Softw. Eng. 36(2), 275–287 (2010)CrossRef
9.
Clarke, D., Noble, J., Wrigstad, T. (eds.): Aliasing in Object-Oriented Programming: Types, Analysis, and Verification. Springer, Heidelberg (2013)
10.
Comar, C., Kanig, J., Moy, Y.: Integrating formal program verification with testing. In: Proceedings of ERTS (2012)
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)CrossRef
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)
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
14.
Huisman, M., Klebanov, V., Monahan, R. (eds.): Int. J. Softw. Tools Technol. Transf., special issue, VerifyThis 2012, vol. 17 (2015)
15.
Koenig, J., Leino, K.R.M.: Programming language features for refinement. Submitted to EPTCS (2015)
16.
Lammich, P.: Refinement based verification of imperative data structures. In: Proceedings of the Conference on Certified Programs and Proofs (2016)
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
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)MathSciNetCrossRef
19.
McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)CrossRefMATH
20.
Meyer, B.: Object-Oriented Software Construction, 1st edn. Prentice-Hall Inc., Upper Saddle River (1988)MATH
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)
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)
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)CrossRef
Metadaten
Titel
Abstract Software Specifications and Automatic Proof of Refinement
verfasst von
Claire Dross
Yannick Moy
Copyright-Jahr
2016
Buch
Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification

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

Electronic ISBN: 978-3-319-33951-1

Copyright-Jahr: 2016

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

Premium Partner

    Bildnachweise