SPARK and Standards

SPARK is not designed to meet the requirements of any one standard.

We firmly believe that software which has been produced in line with our Correctness-by-Construction approach should be able to meet the requirements of any standard.

SPARK has a proven track record in projects working to the most demanding standards in the software industry. These include:

RTCA DO-178B. SPARK proved to be a significant technical and commercial success in the development of the Lockheed C130J.

UK Def. Stan. 00-55. Praxis implemented SHOLIS – the first system to meet the requirements of 00-55 – almost entirely in SPARK. As far as we know, SPARK is the only language that meets the requirements of 00-55 for safety-critical software.

CENELEC 50128. This standard is the rail industry's instantiation of the generic 61508 standard safety-critical software. Several of our customers are using SPARK in meeting the stringent requirements of this standard.

ITSEC and Common Criteria. These standards deal with the development of high-security systems. Praxis used SPARK in the development of the MULTOS CA, which was designed to meet the requirements of ITSEC level E6. Again, SPARK is the only widely used language that we believe meets the ITSEC and Common Criteria implementation requirements.