AdaCore: SPARK Pro 16 helps reduce certification effort for safety-critical systems

AdaCore announced the latest release of its SPARK Pro integrated development and verification environment, bringing a sound and mathematics-based static analysis technology to the challenges of software verification for high-assurance systems. SPARK Pro 16 provides enhanced coverage of SPARK 2014 language features and now supports the Ravenscar tasking profile, thus extending the benefits of formal verification methods to a safe subset of Ada 2012 concurrent programming features. As another improvement SPARK Pro 16 can generate counterexamples to verification conditions that cannot be proved, thus making it easier for developers to find defects in the functional code or in the supplied contracts. SPARK Pro 16 also improves the handling of bitwise (modular) operations, and the product’s proof engine now includes the Z3 SMT solver.

The SPARK Pro technology, which has been jointly developed by AdaCore and its partner Altran, can prove SPARK program properties ranging from absence of run-time errors (exceptions) to compliance with a formally defined requirements specification. SPARK Pro thereby helps reduce the cost of software verification and simplifies the task of certifying the software against safety or security standards. The technology is sound; that is, there are no “false negatives”: if SPARK Pro reports that a program is free of a certain kind of error, then that error cannot occur. It also has a very low “false positive” rate, which is important in practice, and its efficient SMT solver technology scales up for usage in large projects. The SPARK language and toolset can be used from the outset on new projects or introduced incrementally into an existing project, allowing a “hybrid” verification approach that combines formal methods with traditional testing techniques.

SPARK Pro provides the foremost language, toolset, and design discipline for engineering high-assurance software. It combines the SPARK language and verification tools with AdaCore’s GNAT Programming Studio (GPS) and GNATbench Integrated Development Environments.

The SPARK Pro toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness, including proofs of the absence of run-time errors, which can then be used to meet the requirements of safety and security certification schemes, such as DO-178B and DO-178C (airborne systems), EN 50128 (railway systems), and the Common Criteria. SPARK Pro is especially applicable in the context of the Formal Methods supplement to DO-178C.

More Information...

Latest News from AdaCore

AdaCore: new Versions of GNAT Pro, CodePeer, QGen and SPARK Pro
AdaCore: new version of model-based development and verification toolset QGen 2.1
AdaCore releases GNAT Pro 7.4
AdaCore: SPARK Pro 16 helps reduce certification effort for safety-critical systems

WSI's OLED Professional innovations create more value for You.

WSI are the PMOLED manufacturer and our factory located in Chun-Nan in Taiwan. Our products are the market leader and pioneer in PMOLED module, including the monochrome, area colors and full color one...


SKIPPER UBT21 - a Bluetooth 4.0 USB serial adapter for industrial and medical use

SKIPPER UBT21 is a Bluetooth 4.0 USB serial adapter for industrial and medical use. It incorporates a Bluetooth Dual-Mode Stack, supports ranges of up to 300 meters and transferrates of 720 kbit/s (ne...


Three of a kind - Versatility based on Low Power ARM Cortex-A15

At this year's Embedded World, MEN has presented three low power, ARM Cortex-A15-based solutions on different form factors: a VMEbus SBC, an industrial box PC and a COM Express Mini module. All so...


Enabling Embedded IoT

Eurotech, a long-time leading provider of embedded systems and a global leader in IoT enablement, showed its new modules and Multi-service IoT Gateways at Embedded World 2017. The newly introduced Eu...


PLS’ UDE and new UAD2next allow more powerful trace analysis of embedded multicore systems

The new Universal Debug Engine 4.8 from PLS Development Tools offers a bunch of new and improved features for trace analysis of embedded multicore systems. With the new access device UAD2next PLS cont...


Disruptive technologies

Rahman Jamal, Global Technology & Marketing Director, National Instruments, talks about disruptive technologies in the consumer world, but also in measurement, automation, and the embedded industr...


AdaCore Announces Availability of QGen Debugger at Embedded World 2017

Jose Ruiz, technical lead at AdaCore for the company's QGen automatic code generator toolset for model-based development, discusses that product and explains what differentiates it from other prod...


SECO IoT roadmap: from the proof of concept to the market

During Embedded World 2017 Gianluca Venere, SECO Director of Global Sales, leads us to discover the company's Industrial IoT roadmap showcased at SECO's main booth, along with the latest UDOO ...


Internet of Chocolate

HCC show off an embedded chocolate vending machine using MQTT to connect to a broker in the cloud. There is an important message behind this cool demo – security and reliability of embedded soft...