6. Bibliography¶
DO-178C/ED-12C: Software Considerations in Airborne Systems and Equipment Certification. RTCA and EUROCAE, December 2011.
DO-330/ED-215: Software Tool Qualification Considerations. RTCA and EUROCAE, December 2011.
EN 50128: Railway applications – Communications, signalling and processing systems – Software for railway control and protection systems. CENELEC, 2011.
High-Integrity Object-Oriented Programming in Ada, Version 1.4. AdaCore, October 2016. URL: https://www.adacore.com/knowledge/technical-papers/high-integrity-oop-in-ada/.
EN 50126-1: Railway applications - The specification and demonstration of reliability, availability, maintainability and safety (RAMS)- Part 1: Generic RAMS process. CENELEC, October 2017.
EN 50126-2: Railway applications - The specification and demonstration of reliability, availability, maintainability and safety (RAMS)- Part 2: systems approach to safety. CENELEC, October 2017.
EN 50657: Railways applications – Rolling stock applications - Software on Board Rolling Stock. CENELEC, August 2017.
EN 50129: Railway applications - Communication, signalling and processing systems - Safety related electronic systems for signalling. CENELEC, November 2018.
EN 50128/A1: Railway applications – Communications, signalling and processing systems – Software for railway control and protection systems. CENELEC, February 2020.
EN 50128/A2: Railway applications – Communications, signalling and processing systems – Software for railway control and protection systems. CENELEC, July 2020.
SPARK Reference Manual, Release 2020. AdaCore and Altran, 2020. URL: https://www.adacore.com/uploads/techPapers/spark_rm_community_2020.pdf.
Common Criteria for Information Technology Security Evaluation (ISO/IEC 15408). Common Criteria Development Board, 2022. URL: https://www.commoncriteriaportal.org/.
EN 50657/A1: Railways applications – Rolling stock applications - Software on Board Rolling Stock. CENELEC, November 2023.
EN 50716: Railway applications – Requirements for software development. CENELEC, November 2023.
EN 50126-1/A1: Railway applications - The specification and demonstration of reliability, availability, maintainability and safety (RAMS) - Part 1: Generic RAMS process. CENELEC, 2024.
GNAT Coding Style: A Guide for GNAT Developers. AdaCore, 2025. URL: https://gcc.gnu.org/onlinedocs/gnat-style.pdf.
AdaCore. Online training for Ada and SPARK. AdaCore. URL: https://learn.adacore.com/.
AdaCore. AdaCore + Rail. URL: https://www.adacore.com/industries/rail.
AdaCore. GNAT User's Guide Supplement for Cross Platforms. URL: https://docs.adacore.com/live/wave/gnat_ugx/html/gnat_ugx/gnat_ugx.html.
AdaCore. GNAT User's Guide for Native Platforms. URL: https://docs.adacore.com/live/wave/gnat_ugn/html/gnat_ugn/gnat_ugn.html.
AdaCore. GNATformat Documentation. URL: https://docs.adacore.com/live/wave/gnatformat/html/user-guide/.
AdaCore. GPRbuild and GPR Companion Tools User's Guide. URL: https://docs.adacore.com/gprbuild-docs/html/gprbuild_ug.html.
AdaCore. Online training for Ada and SPARK. URL: https://learn.adacore.com/.
AdaCore. High-Integrity Object-Oriented Programming in Ada. AdaCore, 2016. URL: https://www.adacore.com/knowledge/technical-papers/high-integrity-oop-in-ada/.
AdaCore and Altran. PARK Reference Manual, Release 2020. AdaCore, 2020. URL: https://www.adacore.com/uploads/techPapers/spark_rm_community_2020.pdf.
AdaCore and Thales. Implementation Guidance for the Adoption of SPARK. AdaCore, 2020. URL: https://www.adacore.com/books/implementation-guidance-spark.
John Barnes. Programming in Ada 2012. Cambridge University Press, 2014.
John Barnes. Programming in Ada 2012. Cambridge University Press, 2014.
John Barnes and Ben Brosgol. Software, an invitation to Ada 2012. AdaCore, 2015. URL: https://www.adacore.com/books/safe-and-secure-software.
John Barnes and Ben Brosgol. Safe and Secure Software, an invitation to Ada 2012. 2015. URL: https://www.adacore.com/books/safe-and-secure-software.
Paul E. Black, Michael Kass, Michael Koo, and Elizabeth Fong. Source Code Security Analysis Tool Functional Specification. National Institute for Standards and Technology (NIST), 2011.
Jean-Louis Boulanger. CENELEC 50128 and IEC 62279 standards. ISTE-Wiley, London, 2015. URL: https://onlinelibrary.wiley.com/doi/book/10.1002/9781119005056.
Jean-Louis Boulanger and Walter Schön. Assessment of Safety Railway Application. In ESREL 2007 ‐ the 18th European Safety and Reliability Conference. 2007.
Roderick Chapman, Claire Dross, Stuart Matthews, and Yannick Moy. Co-Developing Programs and Their Proof of Correctness. Communications OF The ACM, 2024. URL: https://www.adacore.com/uploads/techPapers/Co-Developing-Programs-and-Their-Proof-of-Correctness.pdf.
Common Criteria. Common Criteria Development Board; *Common Criteria for Information Technology Security Evaluation (ISO/IEC 15408). Common Criteria, 2022. URL: https://www.commoncriteriaportal.org/.
Claire Dross. The Work of Proof in SPARK. AdaCore, 2022. URL: https://www.adacore.com/uploads/techPapers/222293-adacore-spark-press-paper-v3.pdf.
Kelly J. Hayhurst, Dan S. Veerhusen, John J. Chilenski, and Leanna K. Rierson. A Practical Tutorial on Modified Condition / Decision Coverage. NASA, 2001. URL: https://shemesh.larc.nasa.gov/fm/papers/Hayhurst-2001-tm210876-MCDC.pdf.
ICAO. Convention on International Civil Aviation. ICAO, 1944. URL: https://www.icao.int/publications/documents/7300_orig.pdf.
ISO/IEC. Ada Language Reference Manual, Language and Standard Libraries. AdaIC, 2012. URL: https://www.adaic.org/ada-resources/standards/ada12/.
ISO/IEC. Ada Language Reference Manual, Language and Standard Libraries. AdaIC, 2022. URL: https://www.adaic.org/ada-resources/standards/ada22/.
Johannes Kanig, Quentin Ochem, and Cyrille Comar. Bringing SPARK to C developers. ERTS, 2016.
John W. McCormick and Peter C. Chapin. Building High Integrity Applications with SPARK. Cambridge University Press, 2015.
John W. McCormick and Peter C. Chapin. Building High Integrity Applications with SPARK. Cambridge University Press, 2015.
Yannick Moy. Formal program verification in avionics certification. Military Embedded, 2017. URL: https://militaryembedded.com/avionics/safety-certification/formal-program-verification-avionics-certification.
Yannick Moy, Emmanuel Ledinot, Hervé Delseny, Virginie Wiels, and Benjamin Monate. Testing or Formal Verification: DO-178C Alternatives and Industrial Experience. IEEE, 2013.
RCTA. Software Considerations in Airborne Systems and Equipment Certification. RCTA, 2011. URL: https://my.rtca.org/productdetails?id=a1B36000001IcmqEAC.
Leanna Rierson. Developing Safety-Critical Software: A Practical Guide for Aviation Software and DO-178C Compliance. CRC Press, 2013.
Alan Burns, Brian Dobbing and Tullio Vardanega. Guide for the use of the Ada Ravenscar Profile in high integrity systems. Ada Letters, June 2004.
ISO/IEC JTC1/SC22. Working Draft 3.6 - Programming Languages - Guide for the Use of the Ada Programming Language in High Integrity Systems. ISO/IEC PDTR 15942, International Organization for Standardization, August 1998. URL: https://www.open-std.org/JTC1/SC22/WG9/n350.pdf.
ISO/IEC JTC1/SC22. Ada Reference Manual, Language and Standard Libraries. International Organization for Standardization, 2016. ISO/IEC 8652:2012(E) with Technical Corrigendum 1. URL: https://www.adacore.com/documentation/ada-2012-reference-manual.
ISO/IEC JTC1/SC22. Ada Reference Manual, 2022 Edition, Language and Standard Libraries. International Organization for Standardization, 2022. URL: https://www.adacore.com/documentation/ada-2022-reference-manual.