Skip to content

Commit 9d1c8e3

Browse files
Fabien-ChouteauFabien-Chouteau
committed
First version of the Railway Software Booklet
1 parent a0f741d commit 9d1c8e3

35 files changed

+4294
-2
lines changed

‎content/booklets/adacore-technologies-for-railway-software/chapters/annex.rst‎

Lines changed: 244 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,244 @@
1+
.. include:: ../../../global.txt
2+
3+
Technology Annex
4+
================
5+
6+
This annex summarizes how AdaCore's tools and technologies support the various
7+
techniques and measures defined in Annex\ |nbsp|\ D of |en-50128|.
8+
The qualification status for tools, and certifiability for run-time libraries,
9+
are also noted.
10+
11+
.. index:: single: Ada language; Support for Annex D techniques (summary)
12+
13+
Ada Programming Language
14+
------------------------
15+
16+
See :ref:`Railway_SW_Ada`.
17+
18+
Qualification
19+
~~~~~~~~~~~~~
20+
21+
Although there is no qualification of a language *per se*, the Ada language
22+
is standardized through an official process managed by an ISO committee,
23+
IEC/ISO 8652.
24+
AdaCore's Ada compilers and tools have reference and user documentation
25+
that precisely describes the expected behavior, including the effects
26+
of implementation-defined features.
27+
28+
Annex D References
29+
~~~~~~~~~~~~~~~~~~
30+
31+
* D.2 Analyzable Programs
32+
* D.4 Boundary Value Analysis
33+
* D.14 Defensive Programming
34+
* D.18 Equivalence Classes and Input Partition Testing
35+
* D.24 Failure Assertion Programming
36+
* D.33 Information Hiding / Encapsulation
37+
* D.34 Interface Testing
38+
* D.35 Language Subset
39+
* D.38 Modular Approach
40+
* D.49 Strongly Typed Programming Languages
41+
* D.53 Structured Programming
42+
* D.54 Suitable Programming Languages
43+
* D.57 Object Oriented Programming
44+
* D.60 Procedural Programming
45+
46+
47+
GNAT Pro Assurance Toolsuite
48+
----------------------------
49+
50+
.. index:: single: GNAT Pro Assurance; Qualification
51+
.. index:: single: Tool qualification; GNAT Pro Assurance
52+
53+
Qualification
54+
~~~~~~~~~~~~~
55+
56+
.. rubric:: GNAT Pro compiler family
57+
58+
The GNAT Pro compilers for Ada and for C are qualified at class T3.
59+
AdaCore can provide documentation attesting to various aspects such as
60+
service history, development standard, and testing results.
61+
This documentation has been submitted and accepted in past certification
62+
activities.
63+
T3 qualification material can also be developed for the GNAT Pro for C++ and
64+
GNAT Pro for Rust compilers.
65+
66+
Since compilers are large and complex pieces of software, bugs can be
67+
detected (and subsequently corrected) after a particular version has been
68+
chosen. Following the requirements stated in 6.7.4.11, however, a corrected
69+
version of the compiler cannot be deployed without specific justification.
70+
AdaCore offers a dedicated service |ndash| GNAT Pro Assurance |ndash| on a
71+
specified version of the technology, which provides critical problem fixes
72+
(or workaround suggestions) as well as detailed descriptions of the changes.
73+
Using GNAT Pro Assurance, a customer can integrate a corrected version of
74+
a specific compiler release into their development infrastructure
75+
without the risk of regressions from unwanted updates.
76+
77+
See :ref:`Railway_SW_GNAT_Pro_Assurance`.
78+
79+
.. index:: single: GNATstack; Tool qualification
80+
.. index:: single: Tool qualification; GNATstack
81+
82+
.. rubric:: GNATstack
83+
84+
GNATstack can be qualified as a class T2 tool.
85+
86+
.. index:: single: Light Profile; Certification material
87+
.. index:: single: Light-Tasking Profile; Certification material
88+
89+
Run-Time Certification
90+
~~~~~~~~~~~~~~~~~~~~~~
91+
92+
Certification material up to SIL 4 can be developed for the Light and
93+
Light-Tasking run-time libraries.
94+
95+
See :ref:`Railway_SW_Configurable_Run-Time_Libraries`.
96+
97+
.. index:: single: GNAT Pro Assurance; Support for Annex D techniques (summary)
98+
99+
Annex D References
100+
~~~~~~~~~~~~~~~~~~
101+
102+
* D.10 Data Flow Analysis
103+
* D.15 Coding Standards and Style Guide
104+
* D.18 Equivalence Classes and Input Partition Testing
105+
* D.35 Language Subset
106+
107+
108+
SPARK Language and Toolsuite
109+
----------------------------
110+
111+
See :ref:`Railway_SW_SPARK`.
112+
113+
.. index:: single: SPARK Pro toolsuite; Qualification
114+
.. index:: single: Tool qualification; SPARK Pro toolsuite
115+
116+
Qualification
117+
~~~~~~~~~~~~~
118+
119+
The SPARK Pro toolsuite can be qualified at class T2.
120+
121+
.. index:: single: SPARK technology; Support for Annex D techniques (summary)
122+
123+
Annex D References
124+
~~~~~~~~~~~~~~~~~~
125+
126+
The SPARK language and toolset can contribute to the deployment or
127+
implementation of the following techniques:
128+
129+
* D.2 Analyzable Programs
130+
* D.4 Boundary Value Analysis
131+
* D.10 Data Flow Analysis
132+
* D.14 Defensive Programming
133+
* D.18 Equivalence Classes and Input Partition Testing
134+
* D.24 Failure Assertion Programming
135+
* D.28 Formal Methods
136+
* D.29 Formal Proof
137+
* D.34 Interface Testing
138+
* D.35 Language Subset
139+
* D.38 Modular Approach
140+
* D.57 Object Oriented Programming
141+
142+
GNAT Static Analysis Suite
143+
--------------------------
144+
145+
**This section will be completed after review of the content for the
146+
various GNAT SAS tools. CodePeer is no longer a branded tool, and
147+
in any event there is an issue with its qualification status
148+
since it is not sound.**
149+
150+
See :ref:`Railway_SW_GNAT_Static_Analysis_Suite`.
151+
152+
Defects and Vulnerability Analysis
153+
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
154+
155+
**This section will be deleted (and re-titled), or else adapted as needed**
156+
157+
.. index:: single: Defects and Vulnerability Analysis; Qualification
158+
.. index:: single: Tool qualification; Defects and Vulnerability Analysis
159+
160+
161+
Qualification
162+
^^^^^^^^^^^^^
163+
164+
GNAT SAS's defects and vulnerability analysis tool can be qualified at
165+
class T2.
166+
It has a long cross-industry track record and has been qualified under other
167+
standards in the past, such as DO-178B/C as a verification tool/TQL5.
168+
169+
.. index:: single: Defects and Vulnerability Analysis; Support for Annex D techniques (summary)
170+
171+
Annex D References
172+
^^^^^^^^^^^^^^^^^^
173+
174+
GNAT SAS's defects and vulnerability analysis tool can contribute to the
175+
deployment or implementation of the following techniques:
176+
177+
* D.2 Analyzable Programs
178+
* D.4 Boundary Value Analysis
179+
* D.8 Control Flow Analysis
180+
* D.10 Data Flow Analysis
181+
* D.14 Defensive Programming
182+
* D.18 Equivalence Classes and Input Partition Testing
183+
* D.24 Failure Assertion Programming
184+
* D.32 Impact Analysis
185+
186+
Basic Static Analysis tools
187+
~~~~~~~~~~~~~~~~~~~~~~~~~~~
188+
189+
The basic tools are GNATcheck and GNATmetric.
190+
191+
.. index:: single: GNATcheck; Qualification
192+
.. index:: single: Tool qualification; GNATcheck
193+
.. index:: single: GNATmetric; Qualification
194+
.. index:: single: Tool qualification; GNATmetric
195+
196+
Qualification
197+
^^^^^^^^^^^^^
198+
199+
These tools can be qualified at class T2.
200+
GNATcheck has been qualified under other standards as well,
201+
such as DO-178B/C as a verification tool/TQL5.
202+
203+
.. index:: single: GNATcheck; Support for Annex D techniques (summary)
204+
.. index:: single: GNATmetric; Support for Annex D techniques (summary)
205+
206+
Annex D References
207+
^^^^^^^^^^^^^^^^^^
208+
209+
* D.2 Analyzable Programs
210+
* D.14 Defensive Programming
211+
* D.15 Coding Standard and Style Guide
212+
* D.35 Language Subset
213+
* D.37 Metrics
214+
215+
216+
GNAT Dynamic Analysis Suite
217+
---------------------------
218+
219+
This suite comprises GNATtest, GNATemulator, GNATcoverage, GNATfuzz, and TGEN.
220+
221+
See :ref:`Railway_SW_GNAT_Dynamic_Analysis_Suite`.
222+
223+
.. index:: single: GNATtest; Qualification
224+
.. index:: single: Tool qualification; GNATtest
225+
.. index:: single: GNATemulator; Qualification
226+
.. index:: single: Tool qualification; GNATemulator
227+
.. index:: single: GNATcoverage; Qualification
228+
.. index:: single: Tool qualification; GNATcoverage
229+
230+
Qualification
231+
~~~~~~~~~~~~~
232+
233+
GNATtest, GNATemulator and GNATcoverage can be qualified at class T2.
234+
GNATcoverage has been qualified under other standards as well,
235+
such as DO-178B/C as a verification tool/TQL5.
236+
237+
.. index:: single: GNATtest; Support for Annex D techniques (summary)
238+
.. index:: single: GNATemulator; Support for Annex D techniques (summary)
239+
.. index:: single: GNATcoverage; Support for Annex D techniques (summary)
240+
241+
Annex D References
242+
~~~~~~~~~~~~~~~~~~
243+
244+
* D.50 Structure Based Testing

‎content/booklets/adacore-technologies-for-railway-software/chapters/bibliography.rst‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
.. include:: ../../../global.txt
2+
3+
.. only:: builder_html or builder_epub
4+
5+
Bibliography
6+
============
7+
8+
.. bibliography::

0 commit comments

Comments
 (0)