AdaCore’s tools and services are the ideal choice for developing large, long-lived, Air Traffic Management systems, where rigorous software safety, security and reliability standards must be met.
Air travel has increased dramatically since the U.S. federal government deregulated the airline industry in the 1970s. This has put excessive pressure on the air traffic control system to handle a large number of flights while avoiding delays and collisions. To help air traffic controllers track and communicate with aircraft, the FAA and NASA have developed modern software, upgraded existing host computers and voice communications systems and instituted full-scale GPS capabilities. Their mission: to provide the safest, most efficient aerospace system in the world.
AdaCore has years of experience working with customers on ground-based Air Traffic Management systems. We have a deep understanding of the complexities of the development process and tools needed to ease the workflow and manage costs of applications often exceeding a million lines of code and being maintained over decades.
GNAT Pro Assurance
GNAT Pro Assurance supports all versions of the Ada language standard (from Ada 83 to Ada 2012), and C support is an optional add-on. A full toolsuite is supplied, as well as a configurable run-time library and several specific run-times that are especially suited to high-assurance systems. It includes a specialized service known as sustained branches, which allows a project to continue its use of a specific version of the technology, including upgrades to repair critical issues.
SPARK Pro
SPARK Pro is a language and toolset specifically designed for developing applications where correct operation is vital for safety or security. The SPARK Pro toolset offers static verification that is unrivaled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness that can be used to meet the requirements of safety and security certification schemes.
GNAT Static Analysis Suite
GNAT SAS helps developers gain a deep understanding of their code and build more reliable and secure software systems. It features an Ada source code analyzer that detects run-time and logic errors. It assesses potential bugs and vulnerabilities before program execution, serving as an automated peer reviewer, helping to find errors easily at any stage of the development life-cycle. It helps you improve the quality of your code and makes it easier for you to perform safety and/or security analysis.
GNATcoverage
GNATcoverage allows coverage analysis of both object code (instruction and branch coverage), and Ada or C language source code (Statement, Decision and Modified Condition/Decision Coverage - MC/DC)
Ada a Strategic Technology
Because of its preeminence in high-availability and high-reliability domains, the Ada programming language has become a strategic technology in developing and sustaining both airborne and ground-based systems.
SPARK, a subset of the Ada language whose programs are amenable to formal analysis, is another top choice. SPARK is geared toward the development and verification of high-integrity software used in systems where predictable and highly reliable operation is essential. The SPARK language helps developers design and implement applications that demand safety, security, or business integrity. The UK’s Next Generation ATC IFACTS system includes over 200 KLOC of SPARK source code, from which over 120,000 verification conditions are generated to prove freedom from exceptions.
Customer Projects: ATM
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.