diff --git a/content/booklets/adacore-technologies-for-airborne-software/chapters/analysis.rst b/content/booklets/adacore-technologies-for-airborne-software/chapters/analysis.rst index 59f6bc126..9de909b44 100644 --- a/content/booklets/adacore-technologies-for-airborne-software/chapters/analysis.rst +++ b/content/booklets/adacore-technologies-for-airborne-software/chapters/analysis.rst @@ -524,7 +524,7 @@ embedded systems; and Ada's low-level facilities, which allow the programmer to specify target-specific representations for data types (including the bit layout of fields in a record, and the values for enumeration elements). Further information on features that contribute -to safe software may be found in :cite:p:`Barnes_Brosgol_2015`. +to safe software may be found in :footcite:p:`Barnes_Brosgol_2015`. In summary, Ada's benefits stem from its expressive power, allowing the developer to specify the needed functionality or to constrain the @@ -1076,7 +1076,7 @@ AdaCore tools and the Ada language. * A project using a C codebase can incrementally introduce Ada or SPARK. Ada has standard support for interfacing with C, SPARK can be combined with C (with checks at the interfaces) - :cite:p:`Kanig_Ochem_Comar_2016`, and AdaCore's :index:`GNAT Pro Common + :footcite:p:`Kanig_Ochem_Comar_2016`, and AdaCore's :index:`GNAT Pro Common Code Generator` compiles a SPARK-like subset of Ada into C (for use on processors lacking an Ada compiler). C projects can thus progressively adopt higher-tier languages without losing the @@ -1470,7 +1470,7 @@ VxWorks 6 Cert, Lynx178, PikeOS) as well as bare metal configurations, for a wide range of processors (such as PowerPC and ARM). The Ada language helps reduce the risk of introducing errors during -software development (see :cite:p:`Black_et_al_2011`). This is +software development (see :footcite:p:`Black_et_al_2011`). This is achieved through a combination of specific programming constructs together with static and dynamic checks. As a result, Ada code standards tend to be shorter and simpler than C code standards, since @@ -1976,7 +1976,7 @@ the outcome of the two tests is different. In the general case, the MC/DC criterion for a decision with n conditions requires n+1 tests, instead of 2\ :sup:`n`. For more -information about MC/DC, see :cite:p:`Hayhurst_et_al_2001`. +information about MC/DC, see :footcite:p:`Hayhurst_et_al_2001`. .. index:: GNATcoverage .. index:: single: Structural code coverage; GNATcoverage @@ -3326,7 +3326,7 @@ requirements, and this may be appropriate for some critical kernel modules. (A description of how SPARK may be introduced into a project at various levels, depending on the system's assurance requirements, may be found in a booklet co-authored by AdaCore and Thales -:cite:p:`AdaCore_Thales_2020`.) Since subprogram pre- and postcondition +:footcite:p:`AdaCore_Thales_2020`.) Since subprogram pre- and postcondition contracts often express low-level requirements, some low-level requirements-based testing may be replaced by formal proofs as described in the |do-333| Formal Methods supplement to |do-178c|. @@ -4162,3 +4162,10 @@ in this manner, completeness of verification is ensured. The only remaining activity is to check that the PDI instance value complies with the system configuration. + + +.. only:: builder_html + + .. rubric:: Bibliography + +.. footbibliography:: diff --git a/content/booklets/adacore-technologies-for-airborne-software/chapters/bibliography.rst b/content/booklets/adacore-technologies-for-airborne-software/chapters/bibliography.rst deleted file mode 100644 index b2dcb2903..000000000 --- a/content/booklets/adacore-technologies-for-airborne-software/chapters/bibliography.rst +++ /dev/null @@ -1,6 +0,0 @@ -.. only:: builder_html or builder_epub - - Bibliography - ============ - -.. bibliography:: diff --git a/content/booklets/adacore-technologies-for-airborne-software/chapters/introduction.rst b/content/booklets/adacore-technologies-for-airborne-software/chapters/introduction.rst index 16aa937d9..22e48dde7 100644 --- a/content/booklets/adacore-technologies-for-airborne-software/chapters/introduction.rst +++ b/content/booklets/adacore-technologies-for-airborne-software/chapters/introduction.rst @@ -13,9 +13,9 @@ satisfy various objectives of the standards. Many of the advantages of AdaCore's products stem from the software engineering support found in the Ada programming language, including features (such as contract-based programming) introduced in Ada\ |nbsp|\ 2012 -:cite:p:`ISO_IEC_2012`. Other advantages draw directly from the -formally analyzable SPARK subset of Ada :cite:p:`AdaCore_Altran_2020`, -:cite:p:`Dross_2022`, :cite:p:`Chapman_et_al_2024`. As a result, this +:footcite:p:`ISO_IEC_2012`. Other advantages draw directly from the +formally analyzable SPARK subset of Ada :footcite:p:`AdaCore_Altran_2020`, +:footcite:p:`Dross_2022`, :footcite:p:`Chapman_et_al_2024`. As a result, this document identifies how Ada and SPARK contribute toward the development of reliable software. AdaCore personnel have played key roles in the design and implementation of both of these languages. @@ -105,3 +105,10 @@ or technique is introduced, it's important to open a discussion with AdaCore and the designated authority to confirm its acceptability. The level of detail in the process description provided in the project plans and standard is a key factor in gaining acceptance. + + +.. only:: builder_html + + .. rubric:: Bibliography + +.. footbibliography:: diff --git a/content/booklets/adacore-technologies-for-airborne-software/chapters/standards.rst b/content/booklets/adacore-technologies-for-airborne-software/chapters/standards.rst index cdb4f29c8..321559137 100644 --- a/content/booklets/adacore-technologies-for-airborne-software/chapters/standards.rst +++ b/content/booklets/adacore-technologies-for-airborne-software/chapters/standards.rst @@ -11,7 +11,7 @@ Overview "Every State has complete and exclusive sovereignty over the airspace above its territory." This general principle was codified in Article 1 of the Convention on International Civil Aviation (the "Chicago -Convention") in 1944 :cite:p:`ICAO_1944`. To control the airspace, +Convention") in 1944 :footcite:p:`ICAO_1944`. To control the airspace, harmonized regulations have been formulated to ensure that the aircraft are airworthy. @@ -28,7 +28,7 @@ Operating Performance Standards" (MOPS) and a set of recognized |do-254| for Complex Electronic Hardware. *DO-178C/ED-12C - Software Considerations in Airborne Systems and -Equipment Certification* :cite:p:`RTCA_EUROCAE_2011` |mdash| was issued in +Equipment Certification* :footcite:p:`RTCA_EUROCAE_2011` |mdash| was issued in December 2011, developed jointly by RTCA, Inc., and EUROCAE. It is the primary document by which certification authorities such as the FAA, EASA, and Transport Canada approve all commercial software-based @@ -79,7 +79,7 @@ The |do-178c| document suite comprises: in other application domains. Details on how to use these standards in practice may be found in -:cite:p:`Rierson_2013`. +:footcite:p:`Rierson_2013`. .. index:: Design Assurance Level (DAL), Software level @@ -237,8 +237,8 @@ target computer, the other objectives of EOC verification may be satisfied by formal analysis. This is a significant added value. However, employing formal analysis to replace tests is a new concept in the avionics domain, with somewhat limited experience in -practice thus far (see :cite:p:`Moy_et_al_2013` for further -information). As noted in :cite:p:`Moy_2017`, a significant issue is +practice thus far (see :footcite:p:`Moy_et_al_2013` for further +information). As noted in :footcite:p:`Moy_2017`, a significant issue is how to demonstrate that the compiler generates code that properly preserves the properties that have been formally demonstrated for the source code. Running the integration tests both with and without the @@ -270,3 +270,10 @@ Certification credit for using formal proofs is summarized in :align: center SPARK contributions to verification objectives + + +.. only:: builder_html + + .. rubric:: Bibliography + +.. footbibliography:: diff --git a/content/booklets/adacore-technologies-for-airborne-software/chapters/tools.rst b/content/booklets/adacore-technologies-for-airborne-software/chapters/tools.rst index 8cab71b45..4578a9bc0 100644 --- a/content/booklets/adacore-technologies-for-airborne-software/chapters/tools.rst +++ b/content/booklets/adacore-technologies-for-airborne-software/chapters/tools.rst @@ -30,8 +30,8 @@ for contract-based programming in the form of subprogram pre- and postconditions and type invariants) were added in the Ada 2012 version of the language standard, and a number of features to increase the language's expressiveness were introduced in Ada 2022 (see -:cite:p:`ISO_IEC_2012`, :cite:p:`Barnes_Brosgol_2015`, -:cite:p:`Barnes_2014`, :cite:p:`ISO_IEC_2022` for information about +:footcite:p:`ISO_IEC_2012`, :footcite:p:`Barnes_Brosgol_2015`, +:footcite:p:`Barnes_2014`, :footcite:p:`ISO_IEC_2022` for information about Ada). The name *Ada* is not an acronym; it was chosen in honor of Augusta @@ -199,7 +199,7 @@ additional OOP features including Java-like interfaces and traditional Ada is methodologically neutral and does not impose a distributed overhead for OOP. If an application does not need OOP, then the OOP features do not have to be used, and there is no run-time penalty. -See :cite:p:`Barnes_2014` or :cite:p:`AdaCore_2016` for more details. +See :footcite:p:`Barnes_2014` or :footcite:p:`AdaCore_2016` for more details. .. index:: single: Ada language; Concurrent programming @@ -264,7 +264,7 @@ With its emphasis on sound software engineering principles, Ada supports the development of high-integrity applications, including those that need to be certified against safety standards such |do-178c| for avionics, CENELEC EN 50716:2023 for rail systems, and -security standards such as the Common Criteria :cite:p:`CCDB_2022`. +security standards such as the Common Criteria :footcite:p:`CCDB_2022`. Key to Ada's support for high-assurance software is the language's memory safety; this is illustrated by a number of features, including: @@ -358,7 +358,7 @@ cross-domain solutions. The SPARK language has been stable over the years, with periodic enhancements. The 2014 version of SPARK represented a major revision -(see :cite:p:`McCormick_Chapin_2015`), incorporating contract-based +(see :footcite:p:`McCormick_Chapin_2015`), incorporating contract-based programming syntax from Ada 2012, and subsequent upgrades included support for pointers (access types) based on the Rust ownership model. @@ -399,7 +399,7 @@ Ease of Adoption User experience has shown that the language and the SPARK Pro toolset do not require a steep learning curve. Training material such as -AdaCore's online AdaLearn course for SPARK :cite:p:`Learn` can +AdaCore's online AdaLearn course for SPARK :footcite:p:`Learn` can quickly bring developers up to speed; users are assumed to be experts in their own application domain such as avionics software and do not need to be familiar with formal methods or the proof technology @@ -1122,3 +1122,10 @@ eliminating the need for manual input. GNATdashboard fits naturally into a continuous integration environment, providing users with metrics on code complexity, code coverage, conformance to coding standards, and more. + + +.. only:: builder_html + + .. rubric:: Bibliography + +.. footbibliography:: diff --git a/content/booklets/adacore-technologies-for-airborne-software/conf.ini b/content/booklets/adacore-technologies-for-airborne-software/conf.ini index 2d8e5e897..5b1be81dd 100644 --- a/content/booklets/adacore-technologies-for-airborne-software/conf.ini +++ b/content/booklets/adacore-technologies-for-airborne-software/conf.ini @@ -2,4 +2,4 @@ title=AdaCore Technologies for Airborne Software author=Frédéric Pothon \\and Quentin Ochem version=2.1 -bibtex_file=references.bib \ No newline at end of file +bibtex_file=references.bib diff --git a/content/booklets/adacore-technologies-for-airborne-software/index.rst b/content/booklets/adacore-technologies-for-airborne-software/index.rst index 566a1c579..45a55e712 100644 --- a/content/booklets/adacore-technologies-for-airborne-software/index.rst +++ b/content/booklets/adacore-technologies-for-airborne-software/index.rst @@ -158,4 +158,3 @@ booklet. AdaCore Tools and Technologies Overview Compliance with DO-178C / ED-12C Guidance: Analysis Summary of contributions to DO-178C/ED-12C objectives - Bibliography diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/annex.rst b/content/booklets/adacore-technologies-for-railway-software/chapters/annex.rst index 5140e9fe7..62d80742f 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/annex.rst +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/annex.rst @@ -235,10 +235,3 @@ Annex D References ~~~~~~~~~~~~~~~~~~ * D.50 Structure Based Testing - - -.. only:: builder_html - - .. rubric:: Bibliography - -.. footbibliography:: diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/cenelec.rst b/content/booklets/adacore-technologies-for-railway-software/chapters/cenelec.rst index afaa0dcb3..2d8b53fb5 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/cenelec.rst +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/cenelec.rst @@ -149,7 +149,7 @@ and technologies: * Support tools and languages (sub-clause 6.7) |mdash| see :ref:`Railway_SW_tool-qualification` below. -As shown in :cite:`Railway_SW_Boulanger_Schön_2007`, for software applications the +As shown in :footcite:p:`Railway_SW_Boulanger_Schön_2007`, for software applications the assessment process involves demonstrating that the software application achieves its associated safety objectives. @@ -340,7 +340,8 @@ referred to here as "tool qualification", and provides details on what needs to be performed and/or supplied. (The standard does not use a specific term for this process, but the "tool qualification" terminology from the airborne software standards -|do-178c| :cite:`Railway_SW_RTCA_EUROCAE_2011a` and |do-330| :cite:`Railway_SW_RTCA_EUROCAE_2011b` +|do-178c| :footcite:p:`Railway_SW_RTCA_EUROCAE_2011a` and |do-330| +:footcite:p:`Railway_SW_RTCA_EUROCAE_2011b` is appropriate.) .. index:: Tool classes @@ -388,7 +389,7 @@ standard by also specifying the lifecycle phase that is relevant for each sub-clause. The steps shown indicate the requirements to be met and reflect the additional effort needed as the tool level increases; for further information, please see -:cite:`Railway_SW_Boulanger_2015`, Chapter 9. +:footcite:p:`Railway_SW_Boulanger_2015`, Chapter 9. .. .. figure:: ../images/table1.png diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/introduction.rst b/content/booklets/adacore-technologies-for-railway-software/chapters/introduction.rst index 90019865d..138540956 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/introduction.rst +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/introduction.rst @@ -13,11 +13,12 @@ and also a normative process based on certification standards. In Europe, these standards are issued and maintained by CENELEC (European Committee for Electrotechnical Standardization). This document explains the usage of AdaCore's technologies in conjunction -with |en-50128|:2011 :cite:`Railway_SW_CENELEC_2011` |mdash| +with |en-50128|:2011 :footcite:p:`Railway_SW_CENELEC_2011` |mdash| *Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems* |mdash| as modified by amendments -|en-50128|/A1 :cite:`Railway_SW_CENELEC_2020a` and |en-50128|/A2 :cite:`Railway_SW_CENELEC_2020b`. +|en-50128|/A1 :footcite:p:`Railway_SW_CENELEC_2020a` and |en-50128|/A2 +:footcite:p:`Railway_SW_CENELEC_2020b`. (For ease of exposition, the 2011 edition of the standard, as modified by the A1 and A2 amendments, will simply be referred to as |en-50128|.) @@ -31,19 +32,20 @@ standards: .. index:: EN 50126 -* |en-50126|-1 :cite:`Railway_SW_CENELEC_2017b` |mdash| +* |en-50126|-1 :footcite:p:`Railway_SW_CENELEC_2017b` |mdash| *Railway applications - The specification and demonstration of reliability, availability, maintainability and safety (RAMS) - Part 1: Generic RAMS - process* (subsequently modified by |en-50126|-1/A1 :cite:`Railway_SW_CENELEC_2024`) + process* (subsequently modified by |en-50126|-1/A1 + :footcite:p:`Railway_SW_CENELEC_2024`) -* |en-50126|-2 :cite:`Railway_SW_CENELEC_2017c` |mdash| +* |en-50126|-2 :footcite:p:`Railway_SW_CENELEC_2017c` |mdash| *Railway applications - The specification and demonstration of reliability, availability, maintainability and safety (RAMS): Part 2: systems approach to safety* .. index:: EN 50129 -* |en-50129| :cite:`Railway_SW_CENELEC_2018` |mdash| +* |en-50129| :footcite:p:`Railway_SW_CENELEC_2018` |mdash| *Railway applications - Communication, signalling and processing systems - Safety related electronic systems for signalling* @@ -61,8 +63,8 @@ relate to software's role in the safety of a railway system: .. index:: EN 50657 -* |en-50657|:2017 :cite:`Railway_SW_CENELEC_2017a` as modified by amendment - |en-50657|/A1 :cite:`Railway_SW_CENELEC_2023a` |mdash| +* |en-50657|:2017 :footcite:p:`Railway_SW_CENELEC_2017a` as modified by amendment + |en-50657|/A1 :footcite:p:`Railway_SW_CENELEC_2023a` |mdash| *Railways applications - Rolling stock applications - Software on Board Rolling Stock* @@ -75,7 +77,7 @@ relate to software's role in the safety of a railway system: .. index:: EN 50716 -* |en-50716|:2023 :cite:`Railway_SW_CENELEC_2023b` |mdash| +* |en-50716|:2023 :footcite:p:`Railway_SW_CENELEC_2023b` |mdash| *Railway Applications - Requirements for software development* This standard is a successor to |en-50128| and |en-50657|, @@ -149,12 +151,14 @@ processes defined by the CENELEC railway standards. AdaCore's technologies can be used at all Safety Integrity Levels, from Basic Integrity to |sil4|. At lower levels, the full Ada language is suitable, independent of platform. At higher levels, specific subsets will be needed, -for example the :index:`Ravenscar Profile` (:cite:`Railway_SW_Burns_et_al_2004`, -:cite:`Railway_SW_McCormick_Chapin_2015`) for concurrency support with analyzable -semantics and a reduced footprint, or the :index:`Light Profile` -:cite:`Railway_SW_AdaCore_Web_UG_Cross` for a subset with no run-time library +for example the :index:`Ravenscar Profile` +(:footcite:p:`Railway_SW_Burns_et_al_2004`, +:footcite:p:`Railway_SW_McCormick_Chapin_2015`) for concurrency support with +analyzable semantics and a reduced footprint, or the :index:`Light Profile` +:footcite:p:`Railway_SW_AdaCore_Web_UG_Cross` for a subset with no run-time library requirements. At the highest level (|sil4|) the SPARK language -(:cite:`Railway_SW_McCormick_Chapin_2015`, :cite:`Railway_SW_AdaCore_Altran_2020`) and its +(:footcite:p:`Railway_SW_McCormick_Chapin_2015`, +:footcite:p:`Railway_SW_AdaCore_Altran_2020`) and its verification toolsuite enable mathematical proof of properties including correct information flow, absence of run-time exceptions, and, for the most critical code, correctness of the implementation against a formally diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-2.csv b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-2.csv index 85ddb6f15..8829416f7 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-2.csv +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-2.csv @@ -40,7 +40,7 @@ C or assembly." Language Subset,D.35,|mdash|,HR,Yes,"Ada is designed to support \ subsetting, possibly under the control of specific runtimes, GNATcheck, or \ with SPARK. Another possibility is to follow the recommendations in \ -:cite:`Railway_SW_ISO_IEC_1998`." +:footcite:p:`Railway_SW_ISO_IEC_1998`." Object-Oriented Programming,"Table A.22, D.57",R,R,Yes,"If needed, Ada \ supports all the usual paradigms of object-oriented programming, in addition \ to safety-related features such as the :index:`Liskov Substitution Principle`." diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/technology.rst b/content/booklets/adacore-technologies-for-railway-software/chapters/technology.rst index 279e41d3b..abed8c2b0 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/technology.rst +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/technology.rst @@ -1226,7 +1226,8 @@ here it will be a value from either :ada:`Base_Class` or :ada:`Subclass`. Storage for :ada:`X` is reserved on the stack, and the invocation :ada:`P (X)` will dispatch to the appropriate version of :ada:`P`. -The booklet :cite:`Railway_SW_AdaCore_2016` provides additional information on how to use +The booklet :footcite:p:`Railway_SW_AdaCore_2016` provides additional information +on how to use object-oriented features in a certified context. .. index:: single: Annex D; Procedural Programming (D.60) @@ -1239,3 +1240,10 @@ Procedural Programming (D.60) Ada implements all the usual features of procedural programming languages, with a general-purpose data type facility and a comprehensive set of control constructs. + + +.. only:: builder_html + + .. rubric:: Bibliography + +.. footbibliography:: diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/tools.rst b/content/booklets/adacore-technologies-for-railway-software/chapters/tools.rst index d440b600f..53334d32a 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/tools.rst +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/tools.rst @@ -34,10 +34,10 @@ Additional features (including support for contract-based programming in the form of subprogram pre- and postconditions and type invariants) were added in the Ada 2012 version of the language standard, and a number of features to increase the language's expressiveness were -introduced in Ada 2022 (see :cite:`Railway_SW_ISO_IEC_2016`, -:cite:`Railway_SW_Barnes_Brosgol_2015`, -:cite:`Railway_SW_Barnes_2014`, -:cite:`Railway_SW_ISO_IEC_2022` for information about Ada). +introduced in Ada 2022 (see :footcite:p:`Railway_SW_ISO_IEC_2016`, +:footcite:p:`Railway_SW_Barnes_Brosgol_2015`, +:footcite:p:`Railway_SW_Barnes_2014`, +:footcite:p:`Railway_SW_ISO_IEC_2022` for information about Ada). .. index:: Lovelace (Augusta Ada), Babbage (Charles), Byron (Lord George) @@ -209,7 +209,8 @@ traditional :ada:`obj.op(...)` operation invocation notation. Ada is methodologically neutral and does not impose a distributed overhead for OOP. If an application does not need OOP, then the OOP features do not have to be used, and there is no run-time penalty. -See :cite:`Railway_SW_Barnes_2014` or :cite:`Railway_SW_AdaCore_2016` for more details.. +See :footcite:p:`Railway_SW_Barnes_2014` or +:footcite:p:`Railway_SW_AdaCore_2016` for more details. .. index:: single: Ada language; Concurrent programming @@ -276,8 +277,9 @@ High-Integrity Systems With its emphasis on sound software engineering principles, Ada supports the development of high-integrity applications, including those that need to be certified against safety standards such |en-50128| for rail systems, -|do-178c| :cite:`Railway_SW_RTCA_EUROCAE_2011a` for avionics, and security standards -such as the Common Criteria :cite:`Railway_SW_CCDB_2022`. +|do-178c| :footcite:p:`Railway_SW_RTCA_EUROCAE_2011a` +for avionics, and security standards +such as the Common Criteria :footcite:p:`Railway_SW_CCDB_2022`. Key to Ada's support for high-assurance software is the language's memory safety; this is illustrated by a number of features, including: @@ -379,7 +381,8 @@ software, and cross-domain solutions. The SPARK language has been stable over the years, with periodic enhancements. The 2014 version of SPARK represented a major revision -:cite:`Railway_SW_McCormick_Chapin_2015`, :cite:`Railway_SW_AdaCore_Altran_2020`), +:footcite:p:`Railway_SW_McCormick_Chapin_2015`, +:footcite:p:`Railway_SW_AdaCore_Altran_2020`), incorporating contract-based programming syntax from Ada 2012, and subsequent upgrades included support for pointers (access types) based on the Rust ownership model. @@ -421,7 +424,8 @@ Ease of Adoption User experience has shown that the language and the SPARK Pro toolset do not require a steep learning curve. Training material such as AdaCore's online -AdaLearn course for SPARK :cite:`Railway_SW_AdaCore_AdaLearn` can quickly bring +AdaLearn course for SPARK +:footcite:p:`Railway_SW_AdaCore_AdaLearn` can quickly bring developers up to speed; users are assumed to be experts in their own application domain such as railway software and do not need to be familiar with formal methods or the proof technology implemented by the toolset. @@ -519,13 +523,14 @@ Language and Tool Support GNAT Pro Assurance for Ada supports all versions of the Ada language standard as well as multiple versions of C (C89, C99, and C11). It provides an Integrated Development Environment -(see :ref:`Railway_SW_Integrated_Development_Environments`), a comprehensive toolsuite +(see :ref:`Railway_SW_Integrated_Development_Environments`), +a comprehensive toolsuite including a visual debugger, and an extensive set of libraries and bindings. Details on the GNAT Pro for Ada toolchain may be found in -:cite:`Railway_SW_AdaCore_Web_UG_Native`. +:footcite:p:`Railway_SW_AdaCore_Web_UG_Native`. AdaCore's GNAT project facility, based on a multi-language builder for systems organized into subsystems and libraries, is documented in -:cite:`Railway_SW_AdaCore_Web_GPR`. +:footcite:p:`Railway_SW_AdaCore_Web_GPR`. .. index:: single: GNAT Pro Assurance; Configurable Run-Time Libraries @@ -540,7 +545,7 @@ Configurable Run-Time Libraries Two specific GNAT-defined run-time libraries have been designed with certification in mind and are known as the Certifiable Profiles -(see :cite:`Railway_SW_AdaCore_Web_UG_Cross`): +(see :footcite:p:`Railway_SW_AdaCore_Web_UG_Cross`): * *Light Profile* @@ -823,9 +828,11 @@ GNATcheck provides: * Style checks that allow developers to control indentation, casing, comment style, and nesting level. -AdaCore's :index:`GNATformat` tool :cite:`Railway_SW_AdaCore_Web_GNATformat`, which +AdaCore's :index:`GNATformat` tool +:footcite:p:`Railway_SW_AdaCore_Web_GNATformat`, which formats Ada source code according to the GNAT coding style -:cite:`Railway_SW_AdaCore_Coding_Style`, can help avoid having code that violates +:footcite:p:`Railway_SW_AdaCore_Coding_Style`, +can help avoid having code that violates GNATcheck rules. GNATformat is included in the GNAT Pro for Ada toolchain. GNATcheck comes with a query language (LKQL, for Language Kit Query Language) @@ -869,7 +876,8 @@ Principle) that can be used to demonstrate consistency of class hierarchies. Testing a private subprogram is outside the scope of GNATtest but can be implemented by defining the relevant testing code in a private child of the package that declares the private subprogram. -Additionally, hybrid verification can help (see :ref:`Railway_SW_Hybrid_Verification`): +Additionally, hybrid verification can help (see +:ref:`Railway_SW_Hybrid_Verification`): augmenting testing with the use of SPARK to formally prove relevant properties of the private subprogram. @@ -1005,7 +1013,8 @@ Critical fixes to GNAT Pro for Rust are upstreamed to the Rust community, and critical fixes made by the community to upstream Rust tools are backported as needed to the GNAT Pro for Rust code base. Additionally, the Assurance edition of GNAT Pro for Rust includes the -"sustained branch" service (see :ref:`Railway_SW_Sustained_Branches`) that strikes the +"sustained branch" service (see :ref:`Railway_SW_Sustained_Branches`) that +strikes the balance between tool stability and project flexibility. .. index:: Integrated Development Environments (IDEs) @@ -1111,3 +1120,10 @@ their software's technical debt, and eliminating the need for manual input. GNATdashboard fits naturally into a continuous integration environment, providing users with metrics on code complexity, code coverage, conformance to coding standards, and more. + + +.. only:: builder_html + + .. rubric:: Bibliography + +.. footbibliography:: diff --git a/content/booklets/adacore-technologies-for-railway-software/index.rst b/content/booklets/adacore-technologies-for-railway-software/index.rst index 045b0237f..cd6ee4dee 100644 --- a/content/booklets/adacore-technologies-for-railway-software/index.rst +++ b/content/booklets/adacore-technologies-for-railway-software/index.rst @@ -134,7 +134,7 @@ As editor of this revised edition, I would like to thank Vasiliy Fofanov (AdaCore) for his detailed and helpful review and suggestions. For up-to-date information on AdaCore support for developers of rail -software, please visit :cite:`Railway_SW_AdaCore_Web_Rail`. +software, please visit :footcite:`Railway_SW_AdaCore_Web_Rail`. | Ben Brosgol, AdaCore | September 2025