SPARK Pro by AdaCore
Software Validation and Verification
Product Description
SPARK Pro is an Integrated Development Environment for High-Assurance software, comprising Altran Praxis’ SPARK language and toolset integrated into AdaCore’s GNAT Programming Studio (GPS). The SPARK Pro tools help prevent, detect, and eliminate defects early in a system’s life cycle, as the source code is developed. Frontline support is provided through GNAT Tracker, AdaCore’s web-based support system.
Designed by Praxis, SPARK is an Ada subset extended with a contract language that allows a program’s specification to be precisely expressed and verified. The SPARK language is especially suitable for applications where correct operation is vital for reasons of safety, security, or both. The SPARK toolset performs static (before run time) verification that is unrivalled in terms of its soundness, low false-alarm rate, depth, and efficiency. The toolset also generates evidence for correctness that can be used to build a constructive assurance case to meet the requirements of industry regulators and certification schemes.
Benefits
Standards
SPARK Pro meets or exceeds the requirements of all high-assurance software standards, including DEF STAN 00-56, DO-178B, IEC 61508, and the Common Criteria. It is likewise expected to exceed the requirements of the forthcoming DO-178C standard.
Processes
SPARK’s zero-tolerance approach to defects is compatible with all mature high-assurance software processes, including CMM, Six Sigma, Agile Methods, and the SEI’s PSPSM and TSPSM.
Ada compatibility
SPARK toolsets are available for Ada 83, Ada 95, and Ada 2005. Since all SPARK language features are legal constructs in the corresponding version of Ada, a SPARK program can be compiled by any compiler implementing that version of the Ada standard. SPARK Pro does not require a subscription to GNAT Pro.
Correctness by Construction
The SPARK language supports the Correctness-by-Construction concept that is based on expecting requirements to change, eliminating errors before testing, developing incrementally, and writing software that is easy to verify.
Features
Soundness
Analysis by the SPARK tools has no “false negatives”. For example, if the tools indicate that no potential out-of-range index errors were detected, then none will occur when the program is run.
Precision / Completeness
Analysis by the SPARK tools minimizes the number of “false alarms” (also known as “false positives”), in which a problem that is reported is in fact not an error at all. With SPARK the incidence of such false alarms is significantly lower than with traditional languages and static analysis tools.
Depth
SPARK checks for deep and subtle bugs, including run-time errors such as buffer overflow and arithmetic overflow, and can even verify that application-specific safety and security properties are not violated.
Efficiency
The algorithms used by the SPARK tools scale up for usage on large programs.
Modularity
SPARK is a modular language, and the SPARK tools can work incrementally during system development. There is no need to wait until a program is complete before obtaining useful results.
Market Segment(s)
- Embedded
ARM Processor(s)
- Cortex-A53
- Cortex-A57
- ARMv8
Search Options
