SPARK Projects

Recent work based on the SPARK language includes:
Mondex International, System Software Development

Praxis undertook the detailed design, coding and testing of a system to support the security of a smart card operating system. The operating system enables a number of different applications or products to be held on the smartcard at the same time, separately and securely, and makes the applications platform independent. Over 100,000 lines of SPARK Ada code were written to ITSEC E6 security standard.

The system runs over a network of NT workstations and is implemented in SPARK Ada, Visual C++ and SQL Server. The system interfaces to specialist cryptographic hardware.

For more information, please see the paper "Industrial Experience with SPARK".

Power Magnetics and Electronics Systems Limited (formerly known as Thorn Automation),
Development of a Safety Critical Helicopter Landing System (SHOLIS)

Praxis was awarded a sub-contract from Thorn Automation (now PMES) to produce the application software for a real-time, embedded, microprocessor-based system which displays whether ship/helicopter parameters are within prescribed safe operating limits for the Ministry of Defence (MoD).

SHOLIS was developed in two phases. In Phase 1, a prototype system was designed and developed which allowed MoD personnel to assess and approve the MMI. Phase 2 involved the design and manufacture of a full pre-production system, with the safety-critical software being developed to meet the requirements of Def Stan 00-55 and NES 620.

The system was specified formally using the Z specification language and was developed using SPARK Ada. Pre- and post-conditions for each module were coded as assertions providing a basis for subsequent proof checking. The system was developed on SUN hosts, with Ada cross-compilers to the target architecture.

For more information, please see the papers "Re-engineering a safety-critical system with SPARK and GNORT" and "Is Proof more Cost-effective than Testing?".


Lockheed Martin Aeronautical Systems Company (LMAC),
Hercules II (C-130J) Flight Software Development

LMAC has transformed the Hercules' avionics and other systems to create the Hercules II, or C-130J airlifter. The Operational Flight Program (OFP) software co-ordinates and controls most of the avionics systems and operates and diagnoses the integrated aircraft.

The integrity of the OFP software has been under intensive scrutiny of two of the world's most stringent regulators: the US FAA and the UK Ministry of Defence.

Praxis and Lockheed applied SPARK technology to the development and verification of the OFP software. The code was developed in SPARK Ada and underwent analysis with the Examiner. This provided early visibility of programming error which would otherwise have been detected much later in the testing phase, when correction costs would have been substantially greater.

Praxis has demonstrated that static analysis during implementation can lead to overall cost savings by reducing the amount of testing effort at later stages of the lifecycle. Given that DO-178B requires an extensive and rigorous testing process, this saving is often substantial and leads to much improved time to market.

For more information, please see the paper "SPARK and the C130J Hercules II".