Customer Projects: SPARK Pro
NVIDIA
AdaCore enhances security-critical firmware with NVIDIA
NVIDIA plans to upgrade select security-critical firmware software, rewriting it from C to Ada and SPARK to increase verification efficiencies to achieve compliance with the functional safety standard ISO-26262.
QinetiQ
Security and Defence Contractor QinetiQ Selects AdaCore’s Mentorship Service to Upgrade to the Latest Version of the SPARK Technology
QinetiQ is looking to SPARK to address software tool obsolescence by modernising the development environment for its Trials Control System (TCS).
DENSO
DENSO Using SPARK Technology for Automotive Research Project
AdaCore and the University of Nagasaki successfully completed a joint research project for DENSO, Application of Formal Methods to Help Achieve Freedom from Interference, with the goal of simplifying the development of safety-critical automotive applications in an ISO 26262 context.
TOYOTA ITC
TOYOTA ITC Japan Selects SPARK Pro Language and Toolset for High-Reliability Research Project
TOYOTA InfoTechnology Center (ITC) Japan selected the SPARK language and SPARK Pro toolset for a research project to develop a vehicle component implementation that can be proven to be free of run-time errors.
Secunet
SPARK Pro Adopted by secunet
To develop a robust multi-level security workstation, Secunet Security Networks chose the SPARK Pro development environment. The security station concurrently handles information of different security domains, maintains confidentiality and integrity of all processed data, and enforces Multiple Independent Levels of Security (MILS) on a single hardware platform.
NATS
GNAT Pro Chosen for UK’s Next Generation ATC System
iFACTS is the future of air traffic control. The combination of Praxis’ experience in critical systems engineering and the high integrity of SPARK Ada enabled the development of this vitally important and sophisticated system.
Vermont Technical College
SPARK Going to the Moon
The GNAT Pro and SPARK language toolsets have been selected for the Lunar IceCube project by Vermont Technical College. Lunar IceCube is a 6-Unit CubeSat mission sponsored by NASA through their NextSTEP initiative. The mission will prospect for water and other lunar volatiles in all forms (solid, liquid, and vapor) from a highly elliptical orbit with a low point of 100 kilometers (60 miles) where the data will be gathered, and a high point of 5,000 kilometers (3,100 miles).
JTEKT
Electric Power Steering System Supplier JTEKT Selects SPARK Pro for Safety-Critical Automotive Software
JTEKT demonstrated how to leverage the SPARK Ada language subset and formal methods to facilitate unit testing and verification of the system’s C code to ensure that it was correct.
Security. Built In.
The SPARK language - drawing on its roots in Ada - and SPARK analyses - SPARK Flow and SPARK Proof - work together to make your code secure.
SPARK Pro prevents or detects important classes of security bugs - including those that lead to many of the top 10 weaknesses cataloged in the CWEs. Unlike most languages, in which making mistakes that lead to security bugs is too easy, the SPARK language provides memory safety out of the box - including freedom from buffer overruns. SPARK Proof extends this core memory safety to include freedom from memory leaks.
Safety. From the Ground Up.
The SPARK language and SPARK analyses work together to
make your code safer.
SPARK Pro starts with a firm foundation - the SPARK language - to provide safety. Unlike most programming tools, in which misusing features like pointers, dynamic memory allocation, and user-raised exceptions is too easy, SPARK Flow and SPARK Proof prove that code recovers from exceptions correctly, is free from runtime errors, and uses pointers and dynamic memory correctly. So you can be certain that your code will work correctly in its initial application and can confidently reuse your code in new applications.
Better Software. Lower Cost.
The SPARK language and SPARK analyses work together to prevent or detect many kinds of bugs automatically - before you even build and test your software.
SPARK Pro guarantees that many classes of bugs are prevented or detected during software development. And you can take this assurance even further by writing your specifications as contracts and proving that your code satisfies them. The result is software with an exceptionally low defect density. Since bugs introduced during software development are exponentially more expensive to fix in later phases - like integration testing, acceptance testing, or deployment - you save time and money over the lifetime of your application.
Verification. Without Testing.
SPARK Proof provides formal verification that is automatic, reproducible, and integrated into the software development process. In many software applications - especially low-level, embedded applications like firmware - testing is impractical or impossible for some parts of the code. But once you've used the SPARK language to capture your specifications as contracts, SPARK Proof will prove that your code satisfies its contract. So you can be sure your software is correct, even when testing is impossible. Even while your software is changing.
SPARK Pro streamlines verification activities.
Future Proof.
The SPARK language allows you to capture your specifications as contracts so that you can prove that your code satisfies them. Unlike most programming languages, for which specifications must be written in natural language and are disconnected from the code, when your SPARK specifications change, you'll know immediately where you need to update your SPARK code. And as you change your code - for example, to optimize your algorithms - you can be sure the changes still satisfy the contracts. So you never have to worry about your specifications and your code getting out of sync.
SPARK Pro prevents the drift between specification and code.
Easy to Use.
The SPARK language is used for both software implementation and contracts. And the SPARK language scales with you from SPARK Flow to SPARK Proof. So once you learn SPARK, the full power of SPARK Pro is at your disposal. You can learn more about the SPARK language in the Intro to SPARK course at learn.adacore.com.
SPARK Pro's error and warning messages are verbose, linked to detailed explanations, and offer suggestions for fixes whenever possible. Moreover, SPARK is fully integrated into GNAT Studio and VS Code. So you can get actionable feedback about your code, right from your development environment.
It’s never been easier to get started using formal methods.
Easy to Adopt.
The SPARK language is designed to offer safety and security out of the box. So you could adopt SPARK Pro and stop at just using the SPARK language. But we think you’ll want to go further, to get the most out of SPARK Pro as possible.
SPARK Flow offers additional guarantees on top of the SPARK language at no additional cost, reporting problems with data initialization or use. You can take SPARK Flow further by describing your intended data and information flows; SPARK Flow will tell you if your implementation matches your intent.
SPARK Proof takes the guarantees further, but does require more effort. Using the SPARK language, you describe your software’s intent through the provision of contracts. Depending on the complexity of your contracts and software, you may have to use the SPARK language to describe how your software works towards the fulfillment of the contract.
Writing code that proves in SPARK is harder than just writing code. Just like writing code in a statically-typed language is harder than writing code in a dynamically-typed language. That’s why SPARK Pro offers the incremental approach to adoption described above - so you can decide how far you want to push your adoption of SPARK Pro on a unit-by-unit basis.
No matter what you decide, SPARK will be there every step of the way.
Easy to Scale.
SPARK Pro is sound, precise, and modular. So it doesn't experience exponential growth as software gets bigger. SPARK is ready to run on developer machines as well as in DevSecOps pipelines and supports rapid analysis by sharing proof state across instances. So SPARK is ready to scale from small programs to full-size industrial applications - all with the same ease of use.
Relevant Analyses.
SPARK Flow and SPARK Proof analyze the SPARK language directly - without relying on simplifying abstractions that introduce semantic differences between the code and the proof.
The semantics of SPARK contracts are the same as the semantics of the SPARK language, unlike many formal methods that interpret the semantics of the code differently from the actual operational semantics of the code. Integers are machine integers with upper and lower bounds. Arrays are Ada arrays. Floats are IEEE floating-point numbers. And operators - like equality - may be overridden with user-provided semantics. SPARK is aware of and reasons about all of these details and more. So you can be sure that the proof results are really relevant to the code that will execute on your target. You can even retain your contracts and execute them at runtime. You've never had this much assurance that your software is correct.