Systerel implements a formal verification approach through SPARK/Ada.
Today, the latter is applied to the railway sector (EN5018 standard) on applications with volumes ranging from 20KLOC to 400KLOC.
The objectives to be achieved on these legacy codes are to verify that:
1. The data flow is in agreement with the information provided.
2. The semantics of the operations are in agreement with the available or expressed semantics.
3. The code does not raise exceptions (AoRTE).
This approach is in addition to the strategy implemented by Systerel over the last 6 years concerning the conduct to be followed on legacy Ada porting.
But SPARK/Ada does not only apply to legacy code. This technology takes its full scope on new developments generally made in Ada2012.
Its implementation is then simplified and can be done with a reasonable learning curve.
The adoption of SPARK will then contribute in the long term:
1. To structural quality,
2. To functional quality,
3. To maintainability (Contracts –> test oracles),
4. To the satisfaction of the Safety and Security requirements,
5. As a “technical” aestheticism.Our Ada Expertise