The gnatcheck tool can be used to enforce coding conventions and find interesting or suspicious code patterns by analyzing Ada source programs with respect to a set of rules supplied at tool invocation. This manual describes the complete set of predefined rules that gnatcheck can take as input as well as how to write custom rules via the LKQL language.
This guide contains a general description of gnatstack, a framework for computing and analyzing stack usage for the different subprograms in the application and extracting worst case values prior to execution time.
This manual contains useful information in writing programs using the GNAT compiler. It includes information on implementation dependent characteristics of GNAT, including all the information required by Annex M of the standard.
This page gives access to the main GNATemulator documentation. GNATemulator is an efficient and flexible tool that provides integrated, lightweight target emulation.
This User's Guide describes how to use the GNATbench Ada plug-in for Windriver Workbench. Specific help is provided for configuring projects, building systems, and debugging.
This User's Guide describes how to use the GNATbench Ada plug-in for Eclipse. Specific help is provided for configuring projects, building systems, and debugging.
This is the main documentation for GNATcoll, a library providing a number of modules that can be reused in your own applications to add extra features or help implementation.
This is a short guide for using the AUnit test framework. AUnit is an adaptation of the Java JUnit (Kent Beck, Erich Gamma) and C++ CppUnit (M. Feathers, J. Lacoste, E. Sommerlade, B. Lepilleur, B. Bakker, S. Robbins) unit test frameworks for Ada code.
The CodePeer Static Analysis tool may be used with any standard Ada compiler, scans for numerous CWE software errors, and supports all versions of Ada.
GNAT Pro Assurance offers developers the chance to freeze on a stable version of the GNAT technology - essential for long-lived projects or certification.
SPARK Discovery is a preview of the full capabilities of SPARK Pro, making the SPARK formal verification language and toolset available to all GNAT users.
A SPARK Pro demo showing highlights and updates to the SPARK language and our SPARK Pro product range and toolsuite, all invokable through the GPS IDE.
Demos highlighting CodePeer's capability to check for software fragilities, scan for CWE errors, and using the tool in DO-178B and EN 50128 certification.
GNATtest (based on AUnit) helps automate processes for developing and managing the large number of test cases needed for verifying large software systems.
AWS is a library that can be embedded in your application allowing communition with the web and permitting Ada programs to exchange information via HTTP.
GNATstack enables Ada/C/C++ software development teams to accurately predict the maximum size of the memory stack required for an embedded application.
The GNATbench IDE supports both stand-alone Eclipse and also Workbench, the Wind River Systems (WRS) extension to Eclipse for embedded systems development.
No-cost toolset (binary distribution of the GNAT toolset, add-ons and libraries) and support designed to give educators the tools they need to teach Ada.
The GNAT Academic Program with over 200 members links teachers of Ada the world over and provides a way for members to exchange knowledge and resources.
AdaCore provides targeted tools and services to customers in industries with a need for safety and security. Learn more about our industries and customers.
Use GtkAda for portable, efficient GUI-driven applications in Ada. It provides bindings to Gtk+, Glib, Cairo, and Pango as well as a number of widgets.
GNATcoverage helps assess a testing campaign’s completeness by providing sound analysis and evidence that all of the code has been sufficiently exercised.
AdaCore provides onsite support and custom development services for projects requiring specialized expertise (tool integration, new platform ports, etc.).
This course provides an introduction to programming in Ada. It explains Ada’s (including Ada 2012) features, emphasizing how to construct reliable systems.
This course shows how to use AdaCore tools to improve overall code quality, testing, and debugging. It also presents a number of GNAT compiler options.
This course shows how to use GNAT Studio for advanced editing and debugging, invoking the full toolchain, managing projects, and how to customize the tool.
The course explains the rationale of SPARK 2014 and shows how to use the SPARK Pro Toolset both in new projects and in the context of existing systems.
12 September 2017 AdaCore and Altran have announced their renewed sponsorship of the annual High Integrity Software Conference, which takes place in Bristol on 17th October 2017. Now in its fourth year, the mission of the High Integrity Software Conference is to share challenges, best practice and experiences between software engineering practitioners engaged in complex systems. The conference is endorsed by official supporters BAE Systems and Jaguar Land Rover and plays host to a number of industrial exhibitors.
20 September 2016 — AdaCore and Altran have announced their renewed sponsorship of the annual High Integrity Software Conference, which takes place in Bristol on 1 November 2016.
Commemorating Lady Ada’s 200th birthday, AdaCore’s detailed graphic summarizes her life and accomplishments, recaps milestones and resources for programming language named in her honor
NEW YORK and PARIS, July 2, 2015. With great sadness, AdaCore announces the passing of Robert Dewar, company President and one of its founders. Dr. Dewar succumbed to cancer on June 30, 2015. He had a distinguished career as a Professor of Computer Science at New York University (NYU), played a key role in the design and implementation of the Ada programming language, and founded AdaCore, along with four colleagues, in 1994. He served as its CEO until 2012 and as its President until his death.
Advanced static analysis tool for Ada has been qualified under DO-178B and EN50128, adds support for IEEE 754 floating point semantics and enhances support for project files
New tool helps Ada developers keep technical debt in check, supports quality assurance activities, integrates and aggregates results of AdaCore’s static and dynamic analysis tools
Automatic code review and validation tool meets rigorous industry software verification standards; provides trusted reliability for Ada developers in safety-critical applicationsNEW YORK, PARIS and BRISTOL, October 23, 2014, High Integrity Software Conference, Bristol, UK -- AdaCore today announced that its CodePeer advanced static analysis tool for the automated review and validation of Ada source code has been qualified as a software verification tool for developers in both avionics and railway industries.CodePeer assesses the program before execution to find errors efficiently and early in the development life cycle. Using advanced mathematics, CodePeer analyzes every line of software, considering every possible input and every path through the program. It performs impact and vulnerability analysis when existing code is modified, and, using control-flow, data-flow and other advanced static analysis techniques, it detects problems that would otherwise require labor-intensive debugging.“In safety-critical domains, developers need very strong assurances that the tool they’re using to assess their code is reliable, can be trusted, and will substantially reduce the need for manual code review,” says Arnaud Charlet, CodePeer Product Manager and Technical Director at AdaCore. “CodePeer has been through rigorous industry-specific tests for avionics and railway that fully affirm its value and reliability in these and other safety-critical development environments.”
NEW YORK, PARIS and BRISTOL, October 23, 2014, High Integrity Software Conference, Bristol, UK – AdaCore today announced that its GNAT Pro cross-development environment has been selected by the Polytechnic University of Madrid (Universidad Politécnica de Madrid / UPM), for the UPMSat-2 UNION satellite project’s real-time on-board and ground control software. The 50kg micro-satellite, scheduled to be launched in Q4 2015, will provide a technology demonstration platform for the university from a sun-synchronous orbit nearly 600 km above Earth.
NEW YORK and PARIS, September 25, 2013 – AdaCore today launched AdaCore University - a free, web-based resource center for anyone interested in learning about, or how to program in, the Ada programming language. The new website offers pre-recorded courses and other learning materials on Ada, with access to AdaCore’s GNAT Ada toolset for writing and running example programs. It also utilizes the latest in website design and learning tool features. Students at all levels of experience and expertise can begin writing programs quickly and can proceed at their own pace.
SAN JOSE, Calif., NEW YORK and PARIS, April 23, 2013 – Design West Conference – AdaCore and Altran today announced TOYOTA InfoTechnology Center (ITC) Japan’s selection of the SPARK language and SPARK Pro toolset for a high-reliability software research project. The goal of the project is to show that software requirements can be transformed into an implementation that can be proven to be free of run-time errors. This will have the key advantage of providing ultra-low-defect software for higher reliability in a vehicle component. An added benefit is the reduction of development and maintenance effort, since the formal approach being used can give mathematical assurance to a variety of correctness properties, reducing the need for certain types of testing and eliminating the need for post-deployment corrections.
SAN JOSE, Calif., NEW YORK and PARIS, April 23, 2013 – Design West Conference – AdaCore today announced the release of CodePeer 2.2, the advanced static analysis tool that helps developers detect potential run-time and logic errors in Ada programs. CodePeer is able to find non-trivial problems by systematically analyzing every possible input and path through the program, and can be employed very early in the development cycle to identify defects when they are the least costly to repair.
PARIS, NEW YORK, December 17, 2012 – Paris Space Week 2012- AdaCore today announced that Terma A/S has selected the GNAT Pro Safety-Critical development environment to develop onboard software for the Atmosphere-Space Interactions Monitor (ASIM) that will be mounted on the Columbus module of the International Space Station. Terma will useGNAT Pro Safety-Critical combined with the GNATemulator and GNATcoverage dynamic testing tools to develop and test the application prior to deployment on the actual LEON 3 embedded processor.
BOSTON, December 4, 2012 - ACM SIGAda HILT Conference - AdaCore today announced the successful usage of its Code Traceability Analysis for DO-178B by Rockwell Collins in the certification of the Integrated Display System (IDS) for a large, next-generation, commercial aircraft. The Traceability Analysis package is part of the evidence needed to satisfy the DO-178B objectives for structural code coverage at Level A, the highest (most stringent) level for avionics software safety.
NEW YORK, PARIS, and CEDAR RAPIDS, Iowa, September 17, 2012 - Design East Boston 2012 - AdaCore today announced the successful usage of its SPARK Pro and GNAT Pro High-Security products by Rockwell Collins in the development of the SecureOne™ Guard, a high assurance cross domain guard for military tactical systems. The SecureOne Guard has strict requirements for reliability and security. In order to meet these needs, Rockwell Collins selected SPARK Pro and GNAT Pro High-Security as key development tools for the project.
PARIS, NEW YORK, June 20, 2012 - SG PARIS 2012 Conference - AdaCore today announced that SmartSide, a Paris-based company providing Smart Metering and Smart Grid management solutions, has adopted the Ada programming language and AdaCore’s GNAT Pro development environment for the implementation of their Smart Devices platform. SmartSide offers multi-energy meter data management systems. Distribution Network Operators use SmartSide technology to optimize their Smart Grid networks through the secure, reliable, highly-interoperable and business-oriented Smart Energy Core platform.
PARIS, NEW YORK, and GÖTEBORG. June 12th, 2012 – Ada Europe Conference - AdaCore today announced that Saab Electronic Defence Systems (Sweden) has adopted the CodePeer static analyzer tool for use on the GIRAFFE project. This advanced static analysis tool helps developers detect potential run-time and logic errors in Ada programs. By mathematically analyzing every line of software, and considering every possible input and every path through the program, CodePeer can be used very early in the development lifecycle to identify problems when defects are much less costly to correct.
SAN JOSE, Calif., NEW YORK and PARIS, March 26, 2012 – Design West Conference – AdaCore, provider of tools and expertise for the mission-critical, safety-critical, and security-critical software communities, today announced that Embraer Defense and Security has selected the GNAT Pro Ada development environment from AdaCore as a primary tool set to develop the Operation Flight Program for the AMX Modernization program. GNAT Pro will be used along with Wind River’s VxWorks real-time operating system (RTOS) as the foundation to develop this critical software system on the AMX Modernization effort.
NEW YORK, PARIS and TOULOUSE, France, November 29, 2011 - Certification Together Conference – AdaCore, provider of Ada tools and expertise for the mission-critical, safety-critical, and security-critical software communities, today announced that Eurocopter has chosen the GNAT Pro High-Integrity Edition for development of an ARINC-653 demonstrator for military helicopters. The demonstrator will provide military interfaces and operational functions within a time- and memory-partitioned ARINC-653 architecture.
NEW YORK, PARIS and NUREMBURG, Germany, March 1, 2011 – Embedded World Conference - AdaCore, provider of tools and expertise for the mission-critical, safety-critical, and security-critical software communities, today announced that Airbus Military has successfully certified the Airbus Military Aerial Refueling Boom System (ARBS) on the A330 Multi Role Tanker Transport (MRTT). The certification was simplified by the use of the qualified GNATcheck tool to verify conformance to the software coding standard required by the ARBS project. Verification of conformance was undertaken as part of the DO-178B level A Software Verification Process.
AdaCore Releases First Non-Intrusive Coverage Tool to Fully Support All Levels of Safety CertificationNew GNATcoverage tool provides advanced program coverage analysis on both object code and source code
NEW YORK and PARIS, September 21, 2010 – Embedded Systems Conference BostonAdaCore, a leading supplier of Ada development tools and support services, today announced a comprehensive set of tools and support services for projects where Ada is used in conjunction with other programming languages. Available with GNAT Pro 6.3, the latest release of AdaCore’s Ada Development Environment, the solutions include tools and libraries to handle the various ways in which multi-language systems are designed and constructed.
NEW YORK and PARIS, August 23, 2010 – With each new model year, cars are becoming more dependent on microprocessors and complex software, challenging the auto industry to ensure that these systems are secure, safe, and reliable. According to AdaCore, this challenge is not being met: security and safety issues are not being properly considered at the start of the automotive system design cycle, but are instead being addressed as an afterthought. A recent paper from Rutgers University and the University of South Carolina, detailing preventable security flaws of in-car wireless networks, confirms AdaCore’s thesis.
AMSTERDAM, NEW YORK and PARIS, March 24, 2010 – Avionics Europe 2010 – AdaCore today announced that global display company Barco has developed an advanced business jet avionics display system using the AdaCore GNAT Pro Ada development environment. Barco selected the GNAT Pro High Integrity Edition, along with the Traceability Kit, running on Wind River’s VxWorks 653 RTOS in order to meet the highest levels of safety standard DO-178B.
New York and Newcastle, United Kingdom, September 22, 2008 – SAFECOMP 2008 - AdaCore, provider of the highest quality Ada tools and support, today welcomed the 150th member to the GNAT Academic Program (GAP), demonstrating the success of the company’s grass-roots initiative created to help bring Ada to the forefront of university study.
NEW YORK and PARIS – September 9, 2008 – AdaCore, provider of the highest quality Ada tools and support, today announced the appointment of Ada expert Stephen Baird to the company’s GNAT Pro implementation team. In this role, he will participate in the development and enhancement of the GNAT Pro technology, and provide expert support for AdaCore customers.
NEW YORK, AMSTERDAM, Netherlands, and BANGALORE, India, March 5, 2008 – Avionics 2008 - AdaCore, provider of the highest quality Ada tools and support services, today announced that the Indian Aeronautical Development Establishment (ADE) has chosen AdaCore’s GNAT Pro High-Integrity Edition for DO-178B Ada environment to be used by AdaCore’s partner Mistral Solutions to create new safety-critical flight control systems that will underpin advanced Indian defense programs.
TOULOUSE, France and NEW YORK - January 30, 2008 – Embedded Real-time Software (ERTS) Conference - AdaCore, provider of the highest quality Ada tools and support services, today announced the availability of GNATcheck, an integrated coding standard verification tool within the GNAT Pro development environment. GNATcheck meets the growing need for automated verification in safety-critical avionics systems, particularly those systems that need to satisfy the DO-178B standard. Developed by RTCA and EUROCAE, DO-178B defines the guidelines for development of aviation software in both the US and Europe and is being increasingly adopted by other related sectors, such as air traffic control and military applications.
FAIRFAX, Va., November 6, 2007 - SIGAda 2007 - AdaCore, provider of the highest quality Ada tools and support services, today announced the upcoming release of GNAT Programming Studio (GPS) 4.2. This Ada-oriented IDE (Integrated Development Environment) accompanies AdaCore’s GNAT Pro toolset on most platforms.
FAIRFAX, Va., November 6, 2007 - SIGAda 2007 - AdaCore, provider of the highest quality Ada tools and support services, today announced that Raytheon has delivered the Ship Self-Defense System (SSDS) Mk 2 using GNAT Pro for LynxOS within its multi-language software development environment. SSDS Mk 2 is a combat system that integrates and coordinates the sensors and weapons systems aboard a US Naval vessel to provide a coherent tactical picture for situational awareness, command and controls, and quick-reaction self-defense. It is a single-source baseline that supports multiple system configuration modifications (MODs) for large deck ship classes (aircraft carriers and amphibious ships). GNAT Pro was specifically used on the SSDS Mk 2 to support Ada application development on the Intel processors and the LynxOS operating system.
PARIS and NEW YORK, October 29, 2007 - AdaCore, provider of the highest-quality Ada tools and support services, today announced its participation as a member of the TOPCASED Project (Toolkit in Open Source for Critical Applications & System Development).
BOSTON, Mass. – September 18, 2007 – Embedded Systems Conference - AdaCore, provider of the highest quality Ada tools and support services, today announced another successful deployment of a mission-critical system using its GNAT Pro development environment. AAI Services Corporation utilized GNAT Pro as part of an overall upgrade to the U.S. Air Force T25 Simulator for Electronic Combat Training (SECT) system. The T25 SECT system is a software-based training aid that uses interactive combat laboratory exercises and simulated training missions to teach the principles of electronic countermeasures. As part of the upgrade, AAI Services updated one processor on the system’s student station from an SGI VME-based computer to a single board computer running Windows. The original software for the updated processor was ported to a different host and a new development station was added to the existing Training System Support Center.
BOSTON, Mass. – September 18, 2007 – Embedded Systems Conference – AdaCore, provider of the highest quality Ada tools and support services, today announced the immediate availability of GNATstack, a static analysis tool that helps developers predict the maximum stack usage requirements for their applications. GNATstack is available separately or as part of AdaCore’s GNAT Pro High-Integrity Edition products, supporting development for DO-178B, DO-278 and other related safety-critical standards.
BOSTON, Mass., September 18, 2007 - Embedded Systems Conference - AdaCore, provider of the highest-quality Ada tools and support services, today announced its second High-Integrity Edition product GNAT Pro High-Integrity Edition for Servers. The High-Integrity Family was first introduced in June of 2007 with the release of High-Integrity Edition for DO-178B, a product that supports safety-critical avionics and similar standards used in embedded software development. The new GNAT Pro High-Integrity Edition for Servers is fashioned to directly support DO-278, ESARR 4 and 6 and CAP670/SW01, the US, European and UK ground Air Traffic Management (ATM) safety-critical standards. Its capabilities can also be used to support any safety-critical, mission-critical or high reliability system requirements to run on a native platform.
PARIS and NEW YORK - September 10, 2007 - AdaCore, provider of the highest quality Ada tools and support services, today announced that its flagship GNAT Pro development environment is now available for Microsoft’s® .NET Framework. GNAT Pro's launch on .NET broadens AdaCore’s expanding portfolio of Microsoft platforms, which already includes releases for Windows 2000®, Windows 2003®, Windows XP®, and Windows Vista®. Now users of all major Microsoft platforms can also reap the productivity and reliability gains enabled by the Ada language from within the .NET Framework. This especially benefits those creating mission-critical applications, across a broad range of domains, including communications, financial software, and other enterprise systems.
NEW YORK and TAMPA, Fl., June 19, 2007 - Systems & Software Technology Conference – AdaCore, provider of the highest quality Ada tools and support services, today announced that Praxis has selected AdaCore’s GNAT Pro for the implementation of the UK’s next-generation Interim Future Area Control Tools Support (iFACTS) air traffic control system for its client NATS.
NEW YORK, May 14, 2007 - AdaCore, provider of the highest quality Ada tools and services, today announced that it has joined the Eclipse Foundation as an Add-In-Provider. This membership level allows AdaCore to participate in the development of the Eclipse ecosystem, and to offer the breadth of their Ada expertise to the Eclipse community as a whole. Eclipse is an important part of AdaCore's corporate and product strategy. The company tapped into the growing popularity of the Eclipse framework early on, adding an Eclipse plug-in to the company's comprehensive GNAT Pro Ada tool-suite last year. And the company continues to provide customers with the latest technology available with the recent major upgrade to its GNATbench plug-in, offering new capabilities to support Eclipse 3.2, the latest version of the popular open source platform for integrating software tools for application development.
SAN JOSE, Calif. - April 3, 2007 - Embedded Systems Conference - AdaCore, provider of the highest quality Ada tools and support services, announced the future availability of GNATbench Version 2.0, a major enhancement to its GNATbench Eclipse-based plug-in, which supports native (standard) Eclipse and Wind River’s Eclipse-based Workbench software development environments. GNATbench Version 2.0 has been upgraded with new capabilities to support Eclipse 3.2, the latest version of the popular open source platform for integrating software tools for application development. The upgrade provides development teams using the Eclipse 3.2 framework with advanced Ada language support and a fully integrated GNAT Pro Ada toolset to facilitate multi-language development, sophisticated editing, browsing, debugging, and comprehensive compilation.
NEW YORK and AMSTERDAM, Netherlands, March 7, 2007 - Avionics Exhibition and Convention - Saab, one of the world’s leading high-technology companies, today signed a corporate wide licensing agreement with AdaCore. Saab will adopt AdaCore’s GNAT Pro development environment for projects across the organisation and will standardise on GNAT Pro.
NEW YORK and AMSTERDAM, Netherlands, March 7, 2007 - Avionics Exhibition and Convention - AdaCore, provider of the highest quality Ada tools and support, announces the first to market Ada 2005 language development environment, with the release of GNAT Pro version 6.0.1. Ada 2005, ISO/IEC 8652, was formally approved by ISO SC22/WG9 in January 2007. From the start AdaCore has actively participated in the ISO language standard revision process. This has enabled us to be at the forefront in supporting our customers and their use of the new Ada 2005 language standard.
NEW YORK, January 22, 2007 – AdaCore, the leading Ada technology supplier, today announced the appointment of Gregory A. Gicca as the Director of Safety and Security Product Marketing. In this role Mr. Gicca will help plan, guide, and promote AdaCore’s GNAT Pro product offerings for the safety-critical and high-security sectors.
New York and Paris, December 12, 2006 – AdaCore joins The Boeing Company, Smiths Aerospace and Wind River Systems in celebrating the successful first flight of the C-130 Avionics Modernization Program (AMP) aircraft, which took place on September 19. AdaCore serves as a key member of Smiths Aerospace’s development team for the C-130 AMP’s Mission Processor (MP). The MP provides primary computing capability for the cockpit display generation, and extensive video processing, which supports the manipulation and distribution of new and legacy video sources to all aircraft displays. The U.S. Air Force initiated the C-130 AMP to standardize configurations, lower the cost of ownership, and increase survivability of its aging C-130 aircraft. It is the most comprehensive C-130 avionics modification ever conducted.
NEW YORK, NY, USA - AdaCore today announced its latest technology addition - a stand-alone version of the company’s GNATbench plug-in that integrates Ada into native (standard) Eclipse. GNATbench offers the familiar Eclipse “look and feel” when utilizing GNAT Pro’s leading-edge compiler, tools and capabilities, and supports both all-Ada and mixed-language development. With one simple plug-in, GNATbench lets Eclipse users access the benefits of GNAT Pro Ada to develop more reliable applications with fast, predictable performance and at lower cost.
ORLANDO, FL, USA - Today at the Wind River Worldwide User Conference AdaCore announced that its flagship GNAT Pro Ada development environment now supports the latest versions of the Wind River® VxWorks Simulator, a prototyping and simulation tool for VxWorks® 6 and VxWorks 653 applications in the Wind River“ Workbench development suite. VxWorks Simulator (formerly known as VxSIMTM) enables application development and testing without the need for target hardware – either before hardware is available, or to reduce the number of targets required, thereby lessening development cost. It is fully integrated into the Wind River Workbench development suite for execution of VxWorks applications, allowing complete configuration, execution and debugging control through standard interfaces on the host platform.
SALT LAKE CITY, UT, USA - Today at the Systems & Software Technology Conference AdaCore announced that Hamilton Sundstrand has chosen AdaCore’s GNAT Pro as the Ada development environment for the software running in their Air Conditioning Pack airborne software configuration, which regulates cabin air temperature on the 787 aircraft. As part of the contract, AdaCore will adapt its flagship GNAT Pro Ada development environment to generate code for the 787 Pack Control Unit’s designated MPC5554 microcontroller, and provide support for this new, specialized configuration.
NEW YORK, NY, USA - AdaCore today introduced the latest and most versatile version of its GNAT Programming Studio (GPS) product, a sophisticated software development environment for the Ada programming language.
NEW YORK, NY, USA - AdaCore, a leading Ada technology supplier, today announced the appointment of Ada expert Robert A. Duff to the company’s core technical team. Mr. Duff will be responsible for designing and implementing enhancements to the GNAT Pro Ada Development Environment.
NEW YORK, NY, USA - AdaCore, a Wind River leading Ada technology supplier, today announced a GNAT Pro plug-in developed specifically for the Wind River® Workbench development suite. Especially suited for large, embedded, real-time applications running VxWorks® RTOS, AdaCore's GNATbench solution combines the reliability of Ada development and compilation technology with Wind River's popular Eclipse-based, open device software development framework. The result is a fully integrated Ada toolset that enhances Workbench to facilitate multi-language development, sophisticated editing, browsing, debugging, and comprehensive compilation for advanced VxWorks systems creation.
NEW YORK, NY, USA - AdaCore, a Wind River leading Ada technology supplier, today announced that its industry-leading GNAT Pro Ada development environment will support version 6 of Wind River's VxWorks® RTOS. Developed in conjunction with Wind River, AdaCore's GNAT Pro for VxWorks 6 is targeted to the Wind River® General Purpose Platform on the PowerPC, from Windows, GNU/Linux and Solaris host environments.
PARIS, FRANCE - AdaCore, the leader in Ada solutions, today announced GNAT Pro Ada development tool suite support for Freescale Semiconductor, Inc.'s high-performance AltiVec® instruction set. The ability to access AltiVec instructions from Ada was initiated by MBDA, a world leading, global missile systems company. MBDA wanted to combine the potential power of AltiVec with the 'formality' of Ada. By adopting Ada, the programming language best suited for safety-critical, high-reliability applications, MBDA is supporting its own stated priority to "deliver the highest product reliability while developing innovative customized solutions."
NEW YORK, NY, USA - AdaCore announced today the availability of its GNAT Pro Ada development environment on Intel® Itanium® 2-based HP Integrity servers running either the HP-UX or Linux operating systems. With GNAT Pro, Ada users can take full advantage of the performance, security, and flexibility offered by the HP servers. And Ada users with applications running on the AlphaServer and PA-RISC platforms can look forward to a smooth transition to HP-UX 11i and Linux on HP's Integrity servers.
PARIS, FRANCE - GNAT Pro for ERC32, a flexible cross-compilation environment supporting the Ravenscar tasking profile on top of a bare ERC32 computer, is now available. It is designed for mission-critical real-time space applications, including those that have to meet safety standards.
NEW YORK, NY - AdaCore today announced the first implementation of the upcoming new version of the Ada programming language. Known as Ada 2005 and anticipated for official international standardization under ISO next year, the new definition advances the state-of-the-art in programming language design while meeting the goal of compatibility with earlier versions of Ada.
NEW YORK, NY, USA - AdaCore joins Boeing, Smiths Aerospace, and Wind River Systems in celebrating the maiden flight of Boeing’s advanced aerial refueling tanker, the Italian Air Force KC-767A, which took place on May 21, 2005. AdaCore serves as a key member of Smiths Aerospace’s development team for the tanker’s mission control system (MCS), which manages the aircraft’s unique flight guidance, navigation, and communications capabilities. The Italian Air Force was Boeing’s first KC-767 customer, ordering four of the world's newest and most advanced tankers.
PARIS, FRANCE - Maintenance of high-availability systems (e.g., servers) requires the ability to modify, enhance, or correct parts of the application without needing to shut down and re-link the entire system. This is relatively straightforward in an interpreted or virtual-machine based language such as Java, in which new code is loaded upon demand. In a language with static executable images this capability can be realized though dynamically loaded / linked libraries ("DLLs"). However, in practice this causes problems, because the protocol for invoking subprograms in a DLL is very low-level and sacrifices type safety.
NEW YORK, NY, USA - AdaCore today introduced Ada Answers, a web portal aimed at providing managers and software developers with a comprehensive knowledge base about Ada, the programming language most often used to implement high-integrity, safety-critical and real-time systems.
AdaCore (New York) and CodeSourcery (Granite Bay, CA) have partnered to create the G++/GNAT Pro Joint Edition, the first open-source development environment for native and embedded applications that use both Ada and C++ programming languages. The G++/GNAT Pro Joint Edition is based on a combination of several GNU-based, open-source technologies – AdaCore’s GNAT Pro Ada toolsuite, and CodeSourcery's G++ Pro compiler. The result is a full-featured, modern IDE that includes source editors, configuration management facilities, source-level debuggers, source navigation and queries, and user extensibility. It is ideal for complex, mission-critical systems that must efficiently unite software developed in Ada and C++.
NEW YORK, NY, USA - As part of the 5.03 release, AdaCore is pleased to announce the availability of the GNAT Pro toolsuite for the Mac OS X and Mac OS X Server platforms, Apple's award-winning UNIX-based operating system.
NEW YORK, NY, USA - Ada is no longer the best-kept secret in software development. Users are taking notice, and GNAT Pro was nominated for 'Product of the year' in the category 'Enterprise Linux Application'. Despite competing against products that are much better known and that have a much broader user base, GNAT Pro finished in a tie for 3rd place with Novell's SUSE Linux Enterprise Server 9.
NEW YORK, NY, USA - AdaCore is proud to announce that its flagship product, GNAT Pro has been nominated for 'Product of the Year' in Jupiter Media's Datamation Awards. Our distinguished co-nominees are Mozilla's Firefox, VMWare's Workstation and Novell's SUSE Linux Enterprise Server. The Datamation Product of the Year 2005 Awards recognize Datamation readers' choices for achievement and innovation in enterprise software and hardware products.
PARIS, FRANCE - AdaCore is pleased to announce that it will be presenting the following papers and tutorials at Ada Europe 2005 which takes place this June in York, England:
NEW YORK, NY USA / PARIS, FRANCE - As part of the Ada Academic Program, AdaCore is pleased to announce a joint initiative with Praxis Critical Systems Ltd. AdaCore's GNAT Academic Program (GAP) will be linked to the Praxis Academic Support Programme - a fully supported professional SPARK toolset offered free-of-charge to university faculty members for teaching and/or research. SPARK is a high-integrity subset of the Ada programming language. The SPARK Examiner checks conformance of code against the rules of SPARK, performs flow analysis and can generate Verification-Conditions for full formal proof of SPARK source code. In conjunction with the SPADE Simplifier and the SPADE Proof Checker, Praxis provides a suite of tools capable of aiding the development, testing and verification of high integrity systems written in SPARKAda.
NEW YORK, NY, USA - Ada Core Technologies, the leader in Ada 95 solutions and providers of the GNAT Pro Ada development tool suite, today announced it is expanding its support agreement with Silicon Graphics (NYSE: SGI). The new agreement will include the development and support of the GNAT Pro product line on the SGI® Altix® family of superclusters and servers, which feature the 64-bit Intel® Itanium® 2 processor and the Linux® operating system.
Wind River and Ada Core Technologies software will be used in Boeing's new 7E7 Dreamliner, powering the Common Core System, which is the electronics and software backbone of the airplane.Ada Core Technologies' development tool, GNAT Pro High Integrity Edition for AE653, will be integrated into Wind River Platform for Safety Critical ARINC 653Wind River Systems, Inc., the global leader in device software optimization (DSO), and Ada Core Technologies, the global leader in Ada 95 solutions and providers of the GNAT Pro Ada development tool suite, today announced that AdaCore's GNAT Pro High-Integrity Edition for AE653 has been selected as the Ada environment for the Wind River Platform for Safety Critical ARINC 653, to be used in the Boeing 7E7 Dreamliner Program.
NEW YORK, NY, USA - Ada Core Technologies, leader in Ada 95 technology and providers of the GNAT Pro Ada development toolsuite, today announced that it has entered into a distribution agreement with Dedicated Systems Australia Pty Ltd, a distributor providing Australia and New Zealand with world-class software and hardware solutions in the real-time and embedded computing markets with a special focus on defense and communications. This collaboration will not only provide our Pacific Rim customers with a fully integrated Ada solution for native and cross systems, but also bring them the high level of customer attention that is the hallmark of Ada Core Technologies.
SALT LAKE CITY, UT, USA - Software Technology Conference (STC, Salt Lake City) - The Ada Resource Association (ARA) is pleased to announce the addition of its newest member, ACT Europe, which develops components of the GNAT Pro technology for the Ada programming language.
This webinar will show how the Ada language can help you design, implement and verify embedded software that will be reliable, safe and secure, while still meeting its performance requirements.
AdaCore will be attending this event. Ben Brosgol will be giving the talk "Guidance for Introducing Formal Methods into a Software Verification Infrastructure"
Verified Software: Theories, Tools, and Experiments conference. Clement Fumex will be presenting the paper Automating the Verification of Floating-Point Programs.
AdaCore will be attending this event. Yannick Moy will present "Levels of Software Assurance" and the notion of SPARK levels (Stone, Bronze, Silver, Gold), how they were used in Thales experiments and how they map to Altran UK practice, and the underlying techniques that support these (proof of floats using a combination of techniques, ghost code for functional properties).
In this webcast, SPARK experts Yannick Moy and Rod Chapman present the current status of the SPARK solution and explain how it can be successfully adopted in your current software development processes.
Cyrille Comar, co-founder of AdaCore, will be participating on behalf of the company to the panel discussion on DAL modulation on Wednesday 13th September.
Quentin OChem from AdaCore and Flavien Huynh from Squoring Technologies will present the webinar "Managing AdaCore software quality with Squoring and AdaCore tools" Click through to register.
Tucker Taft will present the paper "High-Integrity Multitasking in SPARK: Static Detection of Data Races and Locking Cycles", co-authored by Altran's Florian Schanda and AdaCore's Yannick Moy.
AdaCore will be exhibiting at this event at Booth 217.
AdaCore's Pat Rogers will be presenting a talk on The Practical Development of Safe, Secure, and Reliable Embedded Software on November 11 from 14:45 - 15:15 in the Expo Theater.
AdaCore is a sponsor at this event and Tucker Taft will be presenting the paper "Re-Engineering Abstract Interpretation for Precise, Scalable Whole-Program Verification".
AdaCore will be exhibiting at this event. Pat Rogers will be giving a tutorial on Real-time/Embedded Programming with Ada 2012. Ben Brosgol and Emmanuel Briot will present a tutorial called "When Ada Meets Python: Extensibility through Scripting".
AdaCore will be exhibiting at this event. Matteo Bordin will be presenting “Overview of other generators of the project” and “Model Verification and Code Generation with QGen”.
This webcast will discuss how to select the optimal development tools and processes to ensure the safety, security, and reliability of real-time unmanned aircraft, onboard software, and ground control solutions.
AdaCore is gold sponsor of this event and will be demoing contract-based programming in the context of the Wind River Workbench environment. Michael Friess will be giving the talk "Bring safety on board with contract-based programming and formal verification”.
Quentin Ochem will present the paper "Programming with Contracts - Ada 2012 Tool-Supported Industrial Insights". AdaCore is also a major sponsor of this event.
Processor technology from ARM has become a game changer for multiple industries, delivering high-performance-per-watt processing and high levels of integration to enable system on a chip (SoC) capability in a low-power device. This combination has been ideal for small form factor systems in avionics, automotive, and medical applications. Now embedded designers in these markets are looking at ways to take advantage of ARM technology to enable safety certification via standards such as FAA DO-178C for avionics systems and MISRA for automotive systems. This webcast of industry experts will look at how ARM-based solutions can not only reduce power but easily utilize the integrated peripherals in safety certification solutions across different industries.
Elie Richa will present the paper "Supporting the Testing of Model Transformation Chains with Precondition Construction in Algebraic Graph Transformation".
AdaCore will hold it's annual User Group meeting in Paris, France on September 25 this year. For more details and to register, please visit: http://www.adacore.com/gnatpro-day
Tucker Taft will be giving a talk entitled, "Integrating Test and Proof in the Next Generation Verifiable SPARK Language, Using Contract-Based Programming Features and SMT Solvers."
AdaCore is a major sponsor of this event and will be exhibiting. Thomas Quinot will present the paper, "Lady Ada Mediates Peace Treaty in Endianness War".
AdaCore is lead sponsor of this event. Tucker Taft is presenting an Ada 2012 tutorial and Robert Dewar will give a talk entitled "I'm as Mad as Hell, and I'm Not Going To Take This Anymore!".
AdaCore is exhibiting at this conference (booth #719). Tucker Taft will present the paper, "Systems Programming in the Distributed, Multicore World with Go, Rust, and ParaSail" and Ben Brosgol will give a talk entitled "Object-Oriented Programming for High-Integrity Systems: Pitfalls and How to Avoid Them".
AdaCore is exhibiting at this event- hall 4, booth # 544f . Johannes Kanig will give a talk entitled "Integrating Formal Program Verification with Testing"
AdaCore is a Platinum level sponsor, and AdaCore authors will be presenting a variety of papers and tutorials.
Johannes Känig. Leading-Edge Ada Verification Technologies: Combining Testing and Verification with GNATTest and GNATProve – The Hi-Lite Project (Tutorial)
Tucker Taft. MulticoreProgramming using Divide-and-Conquer and Work Stealing (Tutorial)
Claire Dross, Johannes Känig, and Ed Schonberg. Hi-Lite: The Convergence of Compiler Technology and Program Verification
Vincent Pucci and Ed Schonberg. The Implementation of Compile-Time Dimensionality Checking
Hristian Kirtchev. A Robust Implementation of Ada’s Finalizable Controlled Types
Greg Gicca is presenting a paper “Meeting Top Safety and Security Requirements while Reducing Cost, Size, Weight, and Energy: Achieving High Assurance through a Verifiable Language on a MILS Architecture”.
The Hi-Lite team will present the paper "Maximal and compositional pattern-based loop invariants" and give the talk "The future of formal software verification in avionics".
AdaCore, from time to time, organizes seminars in the Paris offices. If you are interested in a particular talk, please send email to events@adacore.com.
AdaCore will give the following presentation “Source Code as the Key Artifact in Requirement-Based Development: the case of Ada 2012″ – Cyrille Comar, José Ruiz and Yannick Moy, and the following tutorials:
“DO-178C: The Next Avionics Software Safety Standard” – Ben Brosgol “Experimenting with ParaSail – Parallel Specification and Implementation Language” – Tucker Taft
Our partners, Altran Praxis, will give the following tutorials “The Benefits of Using SPARK for High-assurance Software” and “The Use of Proof and Generics in SPARK” – Trevor Jennings and Robin Messer
S. Tucker Taft will be giving a 90 minute lecture "ParaSail: A simplified approach to safe parallel programming" at MIT as part of the Computer Science and Artificial Intelligence Laboratory's (CSAIL) Multicore Software Seminar Series.
Robert Dewar will give a keynote talk “Free Software: A viable model for Commercial Success“. Jose Ruiz will give talks on “Multicore programming support in Ada” and “Programming LEGO MINDSTORMS robots in Ada”.
AdaCore is a platinum sponsor of this event and will give the following talks “Integrating Formal Program Verification with Testing” (Cyrille Comar, Johannes Kanig and Yannick Moy), “Compilation of Heterogeneous Models: Motivations and Challenges” (Matteo Bordin, Tonu Naks, Andres Toom and Marc Pantel), and “Formalization and Comparison of MCDC and Object Branch Coverage Criteria” (Cyrille Comar, Jerome Guitton, Olivier Hainque, Thomas Quinot).
Quentin Ochem will be giving the talk "Lessons to be learned from ultra-paranoid industries (or why software matters)". AdaCore is also exhibiting at this event.
Michael Friess will give a talk "Efficient Safety Critical Systems Development: Is FLOSS the only answer?" in the Open Source Session (15:40-16:20 on Oct 4).
AdaCore is a major sponsor of this event and will be presenting the following paper "Design and Implementation of a Ravenscar Extension for Multiprocessors" by Jose F. Ruiz and Fabien Chouteau.
And the following tutorials:
"Distributed Programming Techniques in Ada" by Thomas Quinot.
"Hard Real-Time and Embedded Systems Programming with Ada" by Patrick Rogers
Roderick Chapman from our partners Altran Praxis will be giving the following tutorial: "SPARK. The Libre Language and Toolset for High-Assurance Software"
AdaCore will be presenting the following paper by Ben Brosgol and Cyrille Comar - An Update on DO-178C: A New Standard for Software Safety Certification.
AdaCore will be presenting the following paper by Greg Gicca and Ben Brosgol - Strategies for Developing Safe and Secure Embedded Systems.
Roderick Chapman from our partners Altran Praxis will be presenting the following paper - Static Code Verification: Issues, Problems and Current Technologies.
Michael Friess will be giving the talk "Efficient Safety Critical Systems Development - Is FLOSS the only answer?" in the FLOSS for Safety related Systems Class (Thursday, March 3, 11:15-12:00). AdaCore is also exhibiting at the event - Booth F224, Hall 11.
This event is jointly organized with the IEEE Control, Aerospace and Electronic Systems Chapter and The University of Adelaide. Robert Dewar will give a talk discussing the topics below:
- Best practices for software design in critical systems. - The suitability of both existing and emerging standards. - An overview of tools and methodologies available to address the certification of such systems, including those available in the open source world. - Legal considerations and security. - A glimpse into the future.
C Support for VxWorks and Bare MetalCodePeer 17 Introduces No False Positives ModeTech Days 2017 Programs Firmed UpDr. John C. Knight: An AppreciationSpotlighting a GAP Member: Georgetown University (Washington, DC)Interview with Yannick MoyFrama-C and SPARK Day 2017Check Out Recent AdaCore Blogs
Make with Ada Prize Winners AnnouncedTech Days 2016 Conducted in Paris and BostonInterview with Quentin OchemVersion 17.1 Product ReleasesSpotlighting a GAP Member: The Australian National University (Canberra)GNAT Pro Supports AddressSanitizer
GNATcoverage Extends Platform Support, Adds FeaturesAdaCore Tech Days 2016Interview with Jamie AyreQGen updateSpotlighting a GAP Member: Technical University of Munich (Germany)Public Ada Training in Boston and ParisAdaCore Sponsoring Ada Programming Competition
In Memoriam: Robert B.K. Dewar, 1945-2015AdaCore Tech Days in Paris and BostonQGen LaunchedAdaCore Blog IntroducedGhost Code in SPARK 2014Ada Course in Paris
Happy 20th Birthday, AdaCore!A Brief History of GNAT Pro 1 AdaCore and Safety CertificationA Brief History of SPARK ProInterview with Robert Dewar and Cyrille ComarA Brief History of CodePeerA Brief History of the GPS and GNATbench IDEsWorkshop on Medical Device Software SecurityUpcoming ReleasesPublic Ada Course, Spring 2015A Brief History of AdaCore and EducationNewsflashConferences/Events
CodePeer 2.3 ReleasedGNATcoverage 1.2 Supports Hardware ProbesCurrent ReleasesIn the PipelineAcademia Corner: Vermont Technical College (US)Interview with Jérôme GuittonGNAT Industrial User DayProduct Spotlight: GNAT Pro Safety-Critical for Railway ApplicationsIntroductory Ada Course from AdaCore and Vector SoftwareConferences/Events
GPS 6.0 ReleasedCurrent ReleasesIn the PipelineAcademia Corner: AdaCore University LauchedInterview with Ben BrosgolGNAT Industrial User DayTechnology Corner: What’s New in SPARK 2014?Conferences/Events
Major New Release of CodePeerGNAT Pro Safety‐Critcal for ARMHi‐Lite Project CompletedCurrent ReleasesIn the PipelineAcademia Corner: Professional Courses from AdaCoreInterview with Valentine ReboulGNAT Pro User DayTechnology Corner: Solving the 4 Endianness Problem with GNATConferences/Events
GPRbuild 2.0 Enhances Support for Multi-Language ProjectsAda 2012 Approved by ISO, Featured on New WebsiteGNAT Industrial User Day Keeps Users InformedCurrent ReleasesIn the PipelineAcademia Corner: Universidad Politécnica de MadridInterview with S. Tucker TaftAdaCore at HILT 2012Technology Corner: Dealing with Integer OverflowConferences/Events
AdaCore and SofCheck Join ForcesAda 2012 Reference Manual Submitted to ISOWho's new at AdaCoreCurrent ReleasesIn the PipelineNew Course on DO-178CAcademia Corner: Kansas State University, USInterview with Nicolas SettonOpen-DO UpdateWebinar ScheduleTechnology Corner: ParasailGNAT Pro User DayConferences/Events
GPS 5.1 Strengthens Multi-Language Support, Tightens CodePeer IntegrationGNATcoverage wins Electron d’Or PrizeCurrent ReleasesIn the PipelineAcademia Corner: University of Southampton,UKInterview with JC BernedoWebinar ScheduleSPARK Prevents Software VulnerabilitiesTechnology Corner: Contract-Based Programming in Ada 2012Conferences/Events
New Tools for Dynamic Analysis of Embedded SystemsAdaCore Awarded Research Funds for New High-Integrity Frameworks/ToolsCurrent ReleasesWebinar ScheduleAcademia Corner: Western Washington UniversityInterview with Olivier HainqueTechnology Corner: GtkAdaAdaCore at Wind River ConferencesConferences/Events
GPS 5.0 Now AvailableGNAT Pro High-Integrity Edition for DO-178BCurrent ReleasesIn the PipelineAcademia Corner: Telecom ParisTechAcademia Corner: University of VirginiaInterview with Steve BairdWebinar ScheduleTechnology Corner: Multi-language Solutions AvailableConferences/Events
CodePeer LaunchedDO-178C Nearing CompletionCurrent ReleasesIn the PipelineWebinar ScheduleAcademia Corner: University of VirginiaInterview with José RuizAdaCore Awarded Grant for Hi-Lite ProjectTechnology Corner: Ada 2012 Nearing CompletionOpen-DO UpdateConferences/EventsAdaCore at Wind River Regional Conferences
GNAT Pro High-Integrity Edition for MILSModel-Based Design Projects UnderwayCurrent ReleasesIn the PipelineAcademia Corner: The Australian National UniversityInterview with Pat RogersWebinar ScheduleContractsConferences/Events
New Release of GNAT Programming StudioContract Award for Coverage Analysis ProjectCurrent ReleasesIn the PipelineAcademia CornerInterview with Emmanuel BriotWebinar ScheduleTechnology Corner:Pragmas Precondition and PostconditionConferences/Events
Gnat Pro High-Integrity Family Expanding to ServersUS Navy Policy Recognizes Open-Source SoftwareCurrent ReleasesIn the PipelineSpotlighting a GAP MemberInterview with Gregory GiccaWebinar ScheduleAdaCore Partner Praxis High Integrity Systems Makes SPARK/Ada a Language to Depend onConferences/Events
What’s New in GNATbench 2.01Major New Air Traffic Control System Using GNAT ProCurrent ReleasesSpotlighting a GAP MemberAda 2005 is an Official ISO Standard!In the PipelineInterview with Arnaud CharletTechnology WebinarsAdaCore Partner Vector Software Helps Certification Effort for DO-178BAdaCore at Conferences
GNAT Pro and Ada 2005 Coming to .NETGNATstack Tool AvailableNew GCC TechnologyWhat’s Coming in GNAT Pro 6.0.1New Version of gprmakeNew Version of GNAT TrackerSpotlighting a GAP MemberAdaCore at ConferencesInterview with Bob DuffPublic Courses at AdaCore New YorkNew Target Platforms for GNAT ProMore Ada 2005 Features Available in GNAT Pro
GNAT Pro for Wind River's VxWorks 6PolyORB 2.0GPS updateGNAT Pro Available on OpenVMS for HP Integrity ServersAJAX in Ada Web ServerStack Usage Analysis ToolInterview with Zepur BlotAdaCore in the NewsPartnership CornerAdaCore at conferences
GNATbench:The Bridge Between GNAT Pro and EclipseFull Steam Ahead with Ada 2005!What’s New with GNAT ProGPS 3.1 Available: Brings Many ImprovementsGNAT Academic Program UpdateInterview with Ed SchonbergAdaCore in the NewsPartnership CornerAdaCore at conferences
GNAT Pro 5.03 ReleaseDynamic Plug-in Loading with AdaIn the PipelineGAP UpdateAdaCore at Ada Europe 2005Interview with Franco GasperoniGNAT Pro Winner of 'Product of the Year'Internationalization in Ada 2005AdaCore at conferences
GNAT Pro High Integrity Edition Selected for Boeing 7E7 page 1A New Look for AdaCoreUpcoming ReleasesThe Ada Academic Initiativewww.ada-answers.com Launches!New GNAT Pro Cross-Compiler for ERC32Interview with Robert DewarMore GNAT Pro Ports on the Way!GNAT Pro Jewel:Scripting in GPSTechnology UpdatesAvailable on SiteAdaCore at ConferencesThe GNAT ProCompany
This case study describes Thales UK’s state-of-the-art non-hull-penetrating optronic mast for the United Kingdom Royal Navy’s new Astute-class submarines, which provides greater flexibility in boat design and improved surface visibility while reducing the probability of detection. The optronic mast is powered by AdaCore partner, Wind River’s VxWorks mission-critical real-time operating system (RTOS) submarine.
The U.S. Navy is using a new ejection seat sequencer that will catapult a pilot and co- pilot (and the seats) out of a damaged F-18, F-14, or T-45 aircraft within 0.2 seconds from the time the ejection handle is pulled.
Approval of aviation software to the guidance of DO-178B/ED-12B and DO-178C/ED-12C [DO178C] requires an applicant to assess the correspondence between source code and object code in certain circumstances. In particular, for Level A software, source code to object code traceability must be established (see paragraph 6.4.4.2b of DO-178C/ED-12C). When the compiler generates object code that is not directly traceable to the source code, additional verifications must be performed. As proposed in the position paper CAST-12 [CAST12], an acceptable approach is to identify that untraceable compiler-generated object code and verify it.
This document analyzes the code generated by the GNAT Pro High-Integrity Edition 7.4.3 compiler hosted on Windows and targeting PowerPC e500v2 ELF identified by the string (issued when using the --version switch):
powerpc-eabispe-gcc (GCC) 4.9.4 20151030 (for GNAT Pro 7.4.3 20161026)
Release 1.0
Document ID: TEC.PB04-045, Issue 1.0
December 16, 2016
This booklet presents a set of guidelines for adopting formal verification in existing projects, codebases and processes. These guidelines are based on five levels of software assurance, in increasing order of benefits and costs. The guidelines were developed jointly by AdaCore and Thales for the adoption of the SPARK language technology at Thales. They do not require a background in mathematical logic or any specialized expertise, and they allow an evolutionary approach to introducing formal methods into an enterprise.
SPARK has a long and successful track record for high-assurance systems. This booklet shows how to exploit its benefits, and understand its costs, on the path to zero-defect software.
The guidance in the DO-178C / ED-12C standard and its associated technology-specific supplements helps achieve confidence that airborne software meets its requirements. Certifying that a system complies with this guidance is a challenging task, especially for the verification activities, but appropriate usage of qualified tools and specialized run- time libraries can significantly simplify the effort. This document explains how a number of technologies offered by AdaCore – tools, libraries, and supplemental services – can help. It covers not only the “core” DO-178C / ED-12C standard but also the technology supplements: Model-Based Development and Verification (DO-331 / ED-218), Object-Oriented Technology and Related Techniques (DO-332 / ED-217), and Formal Methods (DO-333 / ED-216). The content is based on the authors’ many years of practical experience with the certification of airborne software, with the Ada and SPARK programming languages, and with the technologies addressed by the DO-178C / ED-12C supplements
The authors gratefully acknowledge the assistance of Ben Brosgol (AdaCore) for his review of and contributions to the material presented in this document.
Frédéric Pothon, ACG Solutions Montpellier, France
March 2017
This document presents the usage of AdaCore’s technology in conjunction with the CENELEC EN 50128:2011 standard. It describes where the technology fits best and how it can best be used to meet various requirements of the standard.
Written by Jean-Louis Boulanger and Quentin Ochem, for AdaCore
The aim of this booklet is to show how the study of Ada in general, and the features introduced by Ada 2005 and Ada 2012 in particular, can help anyone designing safe and secure software regardless of the programming language in which the software is eventually written. After all, successful implementers of safe and secure software write in the spirit of Ada in any language!
Written by John Barnes with contributions by Ben Brosgol
Frequently, the lack of existing qualifiable COTS tools raises the question whether two separately developed and thus dissimilar tools that satisfy the same operational requirements may be used instead of a single tool, either to avoid the need for qualifying that tool or to serve as an alternative method for tool qualification.
This question may be answered in different ways by different certification authorities, since no guidance or guidelines are provided in the applicable standards, such as DO-178C/ED-12C. DO-330/ED-215 identifies the use of dissimilar tools as an example of “alternative method for tool qualification” but without definition of the actual impact of such approach. DO we have to understand that the use of non-qualified dissimilar tools replaces the need for qualification of a single tool? Is this applicable for all TQL?
This paper presents several use cases based on the type of tools and certification credit, and examines the possible impact on the need for qualification and the applicable Tool Qualification Level of the use of dissimilar tools.
Disclaimer: Discussion of this topic in the Forum for Aeronautical Software (FAS) (see http://www.rtca.org/content.asp?pl=33&sl=170&contentid=170) raised controversial questions and different opinions. Therefore, it was difficult to reach a consensus on an Information Paper. It was decided that this topic is beyond the scope of the FAS working group, and the proposal was withdrawn. This document reflects the author’s point of view, based on his background and experience. It should help readers to provide an acceptable rationale for a software life cycle using dissimilar tools in place of a single qualified tool.
The author, Frédéric Pothon ACG Solutions, and several of the contributors and reviewers participated in the DO-178C/ED-12C working group and subcommittees.
As part of the DO-178C/ED-12C revision effort, a new document Software Tools Qualification Considerations (DO-330/ED-215) was developed. Its goal is both to replace the software tool qualification guidance of DO-178B/ED-12B and also to enable and encourage the use of this “mature” guidance outside the airborne domain. Since it may be used independently, DO-330/ED-215 is not considered as a supplement to DO-178C/ED-12C; it is thus titled differently from the specialized technology supplements.
The purpose of this document is to describe how DO-330/ED-215 impacts the current tool qualification approach of DO-178B/ED-12B and how it provides more relevant guidance for both tool users and tool providers.
We first review the rationale for a Tool Qualification document. But before the application of DO-330/ED-215, a fundamental pre-condition is to establish for the project the tool qualification criteria and the Tool Qualification Levels (TQLs). As an example, we show how DO-178C/ED-12C determines the criteria and TQLs for the airborne domain. In this domain, the criteria are based on the possible impact of a tool error on the software life cycle processes.
We then highlight the main impact of DO-330/ED-215 on current practice, and provide the relevant information to help the reader to apply this new guidance.
Some supporting information is provided in an appendix of DO-330/ED-215. We describe one of the most important topics, addressing the possible certification credit when using a qualified AutoCode Generator (ACG).
The author, Frédéric Pothon ACG Solutions, and several of the contributors and reviewers participated in the DO-178C/ED-12C working group and subcommittees.
This document identifies all the changes in the new release DO-178C/ED-12C, explains their rationale, and highlights the impact of these changes on the various software processes. The author, Frédéric Pothon ACG Solutions, and several of the contributors and reviewers participated in the DO-178C/ED-12C working group and subcommittees.
SPARK is a programming language and formal verification toolset for engineering high-reliability applications. In this document in Japanese, we introduce the fundamental concepts of the SPARK language, and the essential features of the SPARK toolset. This document forms the core part of the complete SPARK User's Guide in English.
Translation to Japanese by Mr. Masao Ito, NIL
SPARK 2014 User’s Guide リリース 18.0w AdaCore and Altran UK Ltd 1 月 18, 2017
Both SPARK and MISRA C are programming languages intended for high-assurance applications, i.e., systems where reliability is critical and safety and/or security requirements must be met. This document summarizes the two languages, compares them with respect to how they help satisfy high-assurance requirements, and compares the SPARK technology to several static analysis tools available for MISRA C with a focus on Frama-C.
Complex model-based tools such as code generators are typically designed as chains of model transformations taking as input a model of a software application and transforming it through several intermediate steps and representations.
The complexity of intermediate models is such that testing is more conveniently done on the integrated chain, with test models expressed in the input language. To achieve a high test coverage, existing transformation analyses automatically generate constraints guiding the generation of test models. However, these so called test objectives are expressed on the complex intermediate models. We propose to back-propagate test objectives along the chain into constraints and test models in the input language, relying on precondition construction in the theory of Algebraic Graph Transformation. This paper focuses on a one-step back-propagation.
This paper describes SPARKSkein - a new reference implementation of the Skein cryptographic hash algorithm, written and verified using the SPARK language and toolset.
The new implementation is readable, completely portable to a wide-variety of machines of differing word-sizes and endian-ness, and “formal” in that it is subject to a proof of type safety. This proof also identified a subtle bug in the original reference implementation which persists in the C version of the code. Performance testing has been carried out using three generations of the GCC compiler. With the latest compiler, the SPARK code offers identical performance to the existing C reference implementation. As a further result of this work, we have identified several opportunities to improve both the SPARK tools and GCC.
Testing or Formal Verification: DO-178C Alternatives and Industrial Experience looks at how to use formal verification instead of testing of software in civilian airplanes (for which DO-178C applies). It is based on the experience of Airbus and Dassault-Aviation in the application of formal verification with the Frama-C platform. In particular it describes:
What the avionics certification standard DO-178C asks in replacement for test coverage, which does not apply when one uses formal verification instead of testing.
How formal verification tools can help with these alternate objectives.
The solutions that Airbus and Dassault-Aviation have implemented to cover these objectives.
This paper is copyrighted by IEEE, and reproduced here with their permission. You can also access it on the IEEE Software website.
Franco Gasperoni's "Thoughts on Ada and Language Technology in Our Times". The paper looks at the origins of Ada, its use in software development, and its key role in mission-critical systems of the 21st century.
This paper’s goal is to provide guidance on how to use Ada’s Object Oriented (OO) features for High-Integrity applications; i.e. high-reliability systems with requirements for safety and/or security which may need to demonstrate compliance with domain-specific certification standards.
Brief Overview
The paper was written by AdaCore experts with extensive experience in this area through their participation in industrial working groups such as EUROCAE’s WG-91, the DO-178C design committee, and ISO’s Ada Rapporteur Group that manages the Ada language standardization process. Another source of experience comes from the support of AdaCore customers, in domains such as aerospace and transportation, since the company’s inception in the mid 1990s. Many customers are using AdaCore tools during their certification process, and some have already completed the highest level of certification with Ada code while extensively using Object Oriented features.
The Object Orientation Concepts chapter summarizes the principal concepts in order to establish the terminology and provide criteria for comparing languages’ approaches. The Object Orientation in Ada chapter introduces Ada’s model for Object Orientation. Readers familiar with Ada 95 can move quickly to the last sections of this chapter, which describe several new features that are being added to the latest revision of language, known as Ada 2012, and which are extremely relevant to safe Object-Oriented programming. The next three chapters – Vulnerabilities and Their Mitigation, Complexity Management, and Safety and Verification Considerations – describe known concerns related to using Object Oriented technology in a High-Integrity environment and discuss recommended solutions. The final chapter, Directions for GNAT Pro Users, starts with a user checklist summarizing the steps we suggest taking when starting out in this area, and then presents the relevant elements and tools of the GNAT Pro technology.
The widespread use of model driven engineering in the development of software-intensive systems, including high- integrity embedded systems, gave rise to a “Tower of Babel” of modeling languages. System architects may use languages such as OMG SysML and MARTE, SAE AADL or EAST-ADL; control and command engineers tend to use graphical tools such as MathWorks Simulink/Stateflow or Esterel Technologies SCADE, or textual languages such as MathWorks Embedded Matlab; software engineers usually rely on OMG UML; and, of course, many in- house domain specific languages are equally used at any step of the development process. This heterogeneity of modeling formalisms raises several questions on the verification and code generation for systems described using heterogeneous models: How can we ensure consistency across multiple modeling views? How can we generate code, which is optimized with respect to multiple modeling views? How can we ensure model-level verification is consistent with the run-time behavior of the generated executable application?
In this position paper we describe the motivations and challenges of analysis and code generation from heterogeneous models when intra-view consistency, optimization and safety are major concerns. We will then introduce Project P and Hi-MoCo - respectively FUI and Eurostars -funded collaborative projects tackling the challenges above. This work continues and extends, in a wider context, the work carried out by the Gene-Auto project. Hereby we will present the key elements of Project P and Hi-MoCo, in particular: (i) the philosophy for the identification of safe and minimal practical subsets of input modeling languages; (ii) the overall architecture of the toolsets, the supported analysis techniques and the target languages for code generation; and finally, (iii) the approach to cross-domain qualification for an open-source, community-driven toolset.
Verification activities mandated for critical software are essential to achieve the required level of confidence expected in life-critical or business-critical software. They are becoming increasingly costly as, over time, they require the development and maintenance of a large body of functional and robustness tests on larger and more complex applications. Formal program verification offers a way to reduce these costs while providing stronger guarantees than testing. Addressing verification activities with formal verification is supported by upcoming standards such as do-178c for software development in avionics. In the Hi-Lite project, we pursue the integration of formal verification with testing for projects developed in C or Ada. In this paper, we discuss the conditions under which this integration is at least as strong as testing alone. We describe associated costs and benefits, using a simple banking database application as a case study.
This paper presents formal results derived from the COUVERTURE project, whose goal was to develop tools to support structural coverage analysis of uninstrumented safety-critical software. After briefly introducing the project context and explaining the need for formal foundations, we focus on the relationships between machine branch coverage and the DO-178B Modified Condition/Decision Coverage (MCDC) criterion. A thorough understanding of those relationships is important, since it provides the foundation for knowing where efficient execution trace techniques can be used to demonstrate compliance with the MCDC criterion. We first present several conjectures that were tested using Alloy models, then provide a formally verified characterization of the situations when coverage of object control-flow edges implies MCDC compliance.
By Tucker Taft, Director of Language Research, AdaCore. CodePeer uses value numbers as part of its static analysis. This is one of the keys to its power and its flexibility. This is a short note that explains how value numbers work in the context of CodePeer, and what advantages they provide.
This paper was originally published in volume 28 of the Ada User Journal in 2007.
Abstract: Dynamic binding, the ability to link at runtime a method call with a subprogram that depends on the class of the object, is strongly discouraged by current standards for avionics airborne systems. This is partly due to dynamic dispatching, the technique commonly used by most OO compilers to implement dynamic binding. In this paper we present some enhancements to the GNAT technology that will help the avionic industry take advantage of the full benefits of the OO techniques with Ada without the inconveniences associated with dynamic dispatching.
At the recent ERTS² 2010 conference held in Toulouse, Thomas Quinot presented this paper entitled “Object and Source Coverage for Critical Applications with the Couverture Open Analysis Framework”. It presents the Couverture approach to object and structural coverage analysis for certified safety-critical applications, in particular in the context of DO-178.
This paper examines the use of Java as a first programming language, in the light of well-established principles of software engineering, and the increasing concern with correctness, performance, and maintainability. We argue that Java is markedly inferior to Ada or C++ as a language for introductory Computer Science courses, and that its widespread use in the training of tomorrow’s software engineers is counterproductive.
This paper examines the use of Java as a first programming language, in the light of well-established principles of software engineering, and the increasing concern with correctness, performance, and maintainability. We argue that Java is markedly inferior to Ada or C++ as a language for introductory Computer Science courses, and that its widespread use in the training of tomorrow’s software engineers is counterproductive.
A recent paper by Franco Gasperoni describing how a Free Software toolset (Coverage) and virtualization technology (QEMU) can be used effectively to assure code coverage in the development of software applications. While an important target use of the coverage toolset is safety-critical embedded applications, the design of the tools allows its use in non safety-critical projects.
Ada 2005 Abstract Interface Types provide a limited and practical form of multiple inheritance of specifications. In this paper we cover the following aspects of their implementation in the GNAT compiler: interface type conversions, the layout of variable sized tagged objects with interface progenitors, and the use of the GNAT compiler for interfacing with C++ classes with compatible inheritance trees.
Many computer applications today involve modules written in different programming languages, and integrating these modules together is a delicate operation. This first requires the availability of formalisms to let programmers denote “foreign” entities like objects and subprograms as well as their associated types. Then, proper translation of what programmers express often calls for significant implementation effort, possibly down to the specification of very precise ABIs (Application Binary Interfaces). Meta-language based approaches a la CORBA/IDL are very powerful in this respect but typically aim at addressing distributed systems issues as well, hence entail support infrastructure that not every target environment needs or can afford. When component distribution over a network is not a concern, straight interfacing at the binary object level is much more efficient. It however relies on numerous low level details and in practice is most often only possible for a limited set of constructs.
Binary level interaction between foreign modules is traditionally achieved through subprogram calls, exchanging simple data types and relying on the target environment’s core ABI. Object Oriented features in modern languages motivate specific additional capabilities in this area, such as class-level interfacing to allow reuse and extension of class hierarchies across languages with minimal constraints. This paper describes work we have conducted in this context, allowing direct binding of Ada extensible tagged types with C++ classes. Motivated by extensions to the Ada typing system made as part of the very recent language standard revision, this work leverages the GCC multi-language infrastructure and implementation of the Itanium C++ ABI. We will first survey the issues and mechanisms related to basic inter-language operations, then present the interfacing challenges posed by modern object oriented features after a brief overview of the Ada, C++, and Java object models. We will continue with a description of our work on Ada/C++ class-level interfacing facilities, illustrated by an example.
Since its inception, a main ob jective of the Ada language has been to assist in the development of large and robust applications. In addition to that, the language also provides support for building safety- critical applications, e.g. by facilitating validation and verification of such programs. The latest revision of the language has brought some addi- tional improvements in the safety area, such as the Normalize Scalars pragma, which ensures an automatic initialization of the non-explicitly initialized scalars. This paper presents Initialize Scalars, an enrichment of the Normalize Scalars concept, and an extended mode to verify at run-time the validity of scalars, both designed for easy use in existing large applications. Their implementation in GNAT Pro (the GNU Ada 95 compiler) is discussed. The practical results obtained on a large Air Traffic Flow Management application are presented.
One of the most important ob ject-oriented features of the new revision of the Ada Programming Language is the introduction of Abstract Interfacesto provide a form of multiple inheritance. Ada 2005 Abstract Interface Types are based on Java interfaces, and as such support inheritance of operation specifications, rather than the general complexity of inheritance of implementations as in full multiple inheritance. Real-time uses of Ada demand efficient and bounded worst-case execution time for interface calls. In addition, modern systems require mixed-language programming. This paper summarizes part of the work done by the GNAT Development Team to provide an efficient implementation of this language feature and simplifies interfacing with C++.
When safety-critical software malfunctions people lives are in danger. When security-critical software is cracked national security or economic activity may be at risk. As more and more software embraces object-oriented programming (OOP) safety-critical and security-critical projects feel compelled to use object-orientation. But what are the guarantees of OOP in terms of safety and security? Are the design goals of OOP aligned with those of safe and secure software (S3) systems? In the following sections we look at key OOP aspects and analyze some of the hazards they introduce with respect to S3 and outline a possible way of addressing these vulnerabilities. Specifically, after a quick overview of OOP in section 2, section 3 deals with inheritance and shows some of its hazards in terms of S3 along with possible remedies. Section 4 focuses on dynamic binding and suggests a safer and more secure implementation than what is conventionally done. Finally, section 5 looks at testing programs with dynamic binding.
The object model of Ada 2005 is well-suited for applications that have to meet certification at various levels. We review the use of Ada in the context of certification, and show that the object-oriented facilities of the current language standard, properly restricted to avoid dynamic dispatching, can already be used without problems under current DO-178B guidelines. We then examine the complications to certification that are presented by dynamic dispatching in a single inheritance model, and show implementation-specific ways of addressing these complications. Finally, we discuss the problems introduced by the use of multiple inheritance. We conclude by showing how, regardless of the extent to which object-oriented idioms are used, Ada provides a safe and efficient vehicle to create certifiable systems.
Below you will find John Barnes booklet that shows how the study of Ada in general and Ada 2005 in particular, is helpful to everyone designing safe and secure software regardless of the programming language in which the software is eventually written.
For the development of mission-critical software, the choice of programming language makes a significant difference in meeting the requirements of exacting safety standards and, ultimately, high-reliability applications.
Ada has a long history of success in the safety-critical domain, with features such as strong typing, that help early error detection, and well-defined semantics. The language has evolved based on user experience, and the forthcoming Ada 2005 standard includes a number of enhancements that will be of particular benefit to developers of high-integrity real-time systems. Relevant features include support for run-time profiles, flexible task-dispatching policies, execution-time clocks and timers, and a unification of concurrency and object-oriented features.
The traditional definition of a safety-critical program is one in which human life depends on the correct operation of the program. If there is a bug in such a program, then death or serious injury can result. Typical examples are signaling systems on trains, avionics control systems, medical instrumentation, and space applications. Since the focus is on human safety, we apply requirements to such programs that essentially require that they be error free.
Ada is at this stage a fairly old language, having been first standardized over twenty years ago. In that time, it has been extensively used, particularly in large critical programs where, to quote Ed Harris in a well known movie, “failure is not an option”. That’s not at all surprising because Ada from its inception has been designed with this kind of reliability in mind.
The forthcoming Ada 2005 standard has been enhanced to better address the needs of the real-time and high-integrity communities. This new standard introduces new restriction identifiers that can be used to define highly efficient, simple, and predictable run-time profiles. Among others, this language revi- sion will standardize the Ravenscar profile, new scheduling policies, and will include execution time clocks and timers. Flexible object-oriented features are also supported without compromising performance or safety.
One of the most important ob ject-oriented features of the new revision of the Ada Programming Language is the introduction of Abstract Interfaces to provide a form of multiple inheritance. Ada 2005 Abstract Interface Types are akin to Java interfaces, and as such support inheritance of specification rather than inheritance of implementation. Ada 2005 interfaces apply as well to tasks and protected types, and provide a classification mechanism for concurrent program- ming that goes considerably beyond the capabilities of Java. This paper summarizes the implementation in the GNAT compiler of the various kinds of interfaces that relate to concurrent programming in Ada 2005. The implementation is efficient, and involves mostly modifications to the com- piler front-end, with virtually minimal impact on run-time structures, beyond those that are in place to support regular interfaces. However, the implementation of interface operations as triggers in selective waits and asynchronous transfers of control proved to be surprisingly delicate and requires additional predefined primitive operations.
This paper describes how GNAT Pro for ERC32 and the Ravenscar profile are suitable for designing and implementing complex on-board software using high-level tasking facilities.The static and simple tasking model defined by the Ravenscar profile allows for a streamlined implementation of the run-time system directly on top of bare machines. The reduced size and complexity of the run time, together with its configurability, makes it suitable for mission-critical space applications in which certification or reduced footprint is needed. Software reliability and predictability is also increased by excluding non-deterministic and non analysable tasking features. Product validation has been achieved by means of a comprehensive test suite intended to check compliance with the Ravenscar profile and Ada standards, and correct be- haviour of specialised features and supplemental tools. with the goal of achieving 100% statement coverage.
This article presents ERB, the ESA Ravenscar Benchmark. ERB aims at providing a synthetic benchmark comparing the efficiency of various Ada Ravenscar implementations and the RTEMS C implementation featuring the native threading model. ERB is original compared to existing Ada benchmarks, such as the ACES or the PIWG, not only because it is the first Ada Ravenscar benchmark, but also because it provides at the same time measurement of exe- cution times and estimate of the memory footprint of the Ada runtime and stack size requirements. ERB intends to become the standard benchmark for embedded Ada Ravenscar applications. To facilitate this, the European Space AgencAdaCore plan to release it under the GNU GPL to interested third parties.
Stack overflows are a major threat to many computer applications and run-time recovery techniques are not always available or appropriate. In such situations, it is of utmost value to prevent overflows from occurring in the first place, which requires evaluating the worst case stack space requirements of an application prior to operational execution time. More generally, as run-time stack areas need memory resources, information on the stack allocation patterns in software components is always of interest. We believe that specialized compiler outputs can be of great value in a stack usage analysis framework and have developed GCC extensions for this purpose. In this paper, we first expand on the motivations for this work, then describe what it consists of so far, future directions envisioned, and experiments results.
This paper describes the design and implementation of GNAT Pro for ERC32, a flexible cross-development environment supporting the Ravenscar tasking model on top of bare ERC32 computers. The static and simple tasking model defined by the Ravenscar profile allows for a streamlined implementation of the run-time system directly on top of bare machines. The reduced size and complexity of the run time, together with its configurability, makes it suitable for mission-critical space applications in which certification or reduced footprint is needed. Software reliability and predictability is also increased by excluding non-deterministic and non analysable tasking features. Product validation has been achieved by means of a comprehensive test suite intended to check com- pliance with the Ravenscar profile and Ada standards, and correct behaviour of specialised features and supplemental tools. Code coverage analysis is also part of the validation campaign, with the goal of achieving 100% statement coverage.
Maintenance of high-availability systems (e.g., servers) requires the ability to modify, enhance, or correct parts of the application without having to stop and re-link the entire system. This capability is relatively straight-forward with interpreted languages or virtual-machine based languages such as Java, in which new code is loaded upon demand. In languages typically implemented with static executable images this capability can be offered though dynamically loaded/linked libraries (“DLLs”). However, in practice it is impractical to make full use of this capability because the protocol for invoking subprograms in a DLL is very low-level and unsafe. In the case of Ada, global coherency requirements and elaboration ordering constraints add an additional degree of complexity over less strict/safe languages. Object-oriented programming makes this approach practical by using dynamic dispatching to invoke dynamically loaded functions with a more robust, high-level protocol. In an OO paradigm, a “plug-in” contains new classes that enrich the class set of the original application. Calls to subprograms in the shared library (plug-in) are done implicitly through dynamic dispatching which is much simpler, transparent to the programmer, type-safe, and more robust. This application note shows how a statically-typed, statically-built, object-oriented language such as Ada can make full use of the notion of dynamic plug-ins á la Java without relying on a comparatively inefficient virtual machine. We build an extensible application and illustrate adding new functionality at run-time, without first stopping execution, using plug-ins. We use GNAT Pro to build the plug-ins and main program on a Windows system. Tailoring to run on Linux or similar operating systems would be straight-forward. Some new features of Ada 2005 are also used in the implementation. Section two describes the structure of the demonstration application and how plug-ins are discovered and loaded. Section three then shows the commands used to build and run the main program and the plug-ins. Section four provides closing remarks.
Transparent system support for software fault tolerance reduces performance in general and precludes application-specific optimizations in particular. In contrast, explicit support – especially at the language level – allows application-specific tailoring. However, current techniques that extend languages to support software fault tolerance lead to interwoven code addressing functional and non-functional requirements. Reflection promises both significant separation of concerns and a malleability allowing the user to customize the language toward the optimum point in a language design space. To explore this potential we compare common software fault tolerance scenarios implemented in both standard and reflective Ada. Specifically, in addition to backward error recovery and recovery blocks, we explore the application of reflection to atomic actions and conversations. We then compare the implementations in terms of expressive power, portability, and performance.
One of the salient object-orientated issues of Ada 2005 are the Abstract Interfaces.Although the concept is not new (it is based on Java interfaces), being Ada a language for reliable and real-time applications its implementation must be efficient and have a bounded worst-case execution time. This paper summarizes parts of the work done by the GNAT Development Team to have an efficient implementation of this language feature.
A concurrent program generally comprises a collection of threads that interact cooperatively, either directly or through shared data objects. In the latter case the sharing needs to be implemented by some mechanism that ensures mutually exclusive access, or possibly “concurrent read / exclusive write”. Ada and the Real-Time Specification for Java have taken different approaches to mutual exclusion. This paper analyzes and compares them with respect to programming style (clarity, encapsulation, avoidance of errors such as deadlock), priority inversion management, expressibility/generality, and efficiency. It also looks at interactions with exceptions and asynchronous transfer of control.
To handle signal processing algorithms such as the Fast Fourrier Transform (FFT) or the Discrete Cosine Transform (DCT) system designers have traditionally resorted to specialized hardware with built- in vector-processing capabilities.With the advent of the Altivec vector extensions for the general-purpose PowerPC processor, developers have the ability to write efficient signal processing code in C and C++. Using Altivec-enabled PowerPCs as an example, this paper explains what can and should be done to write not only efficient, but also clean and reliable vector processing code in Ada.
The latest trend in our industry, “pervasive computing”, predicts the proliferation of numerous, often invisible, computing devices embedded in consumer appliances con- nected to the ubiquitous Internet. Secure, reliable applications combined with simplicity of use will make or break a company’s reputation in this market.
The Java “write once, run anywhere” paradigm, introduced by Sun in the mid- 90s, is embodied in a widely available computing platform targeting pervasive devices. Although the Java Virtual Machine was designed to support the semantics of the Java programming language, it can also be used as a target for other languages.
The Ada 95 programming language is a good match for the Java platform from the standpoint of its portability, security, reliability, and rich feature set. In this article we explain the features that have made Ada the language of choice for software-critical applications and how these features complement the Java programming language while increasing the overall reliability and flexibility of the Java platform.
This article discusses the tools that Ada offers to deal with dynamic memory problems. The article shows how the storage pools mechanism of Ada 95 can be extended to enpower developers when tracking memory leaks and memory corruption in their code. This Ada extension rests on the notion of “checked pools”, i.e. storage pools with an additional Dereference operation. The paper describes how a particular instance of the checked pool, called the “debug pool”, is implemented in the GNAT technology. Performance measurements for the use of debug pools are provided in the context of the Air Traffic Flow Management application at Eurocontrol.
Asynchronous Transfer of Control (“ATC”) is a transfer of control within a thread, triggered not by the thread itself but rather from some external source such as another thread or an interrupt handler. ATC is useful for several purposes; e.g. expressing common idioms such as timeouts and thread termination, and reducing the latency for responses to events. However, ATC presents significant issues semantically, methodologically, and implementationally. This paper describes the approaches to ATC taken by Ada and the Real-Time Specification for Java, and compares them with respect to safety, programming style / expressive power, and implementability / latency / efficiency.
Two independent recent efforts have defined extensions to the Java platform that intend to satisfy real-time requirements. This paper summarizes the major features of these efforts, compares them to each other and to Ada 95’s Real-Time Annex, and argues that their convergence with Ada95 may serve to complement rather than compete with Ada in the real-time domain.
This paper presents recent trends in avionics systems development from bespoke systems through to COTS and emerging Integrated Modular Avionics architectures. The advances in Ada and RTOS technologies are explained and the impact of requirements for RTCA/DO-178B and EUROCAE/ED-12B certification and achievements are presented in the context of the GNAT and VxWorks technologies.
AdaCore is an international company who produce and support the GNAT Professional family of Ada language tools: software suites comprising compilers, debuggers, and other components.
The company has been in business since 1994 and currently markets its products on platforms such as Windows, UNIX / Linux, and on embedded systems such as Tornado/VxWorks and LynxOS. With one or two major releases of each product annually, the company’s livelihood depends on the quality of the software and its support. In many ways AdaCore faces the same issues as other growing software organizations, and this article is intended as a “case study” showing how a combination of automated tools and human management can help meet the QA challenge.
This paper discusses the implementation model for supporting Ada 95 controlled types in the GNAT compiler. After reviewing the semantics of controlled types, we outline the associated implementation problems and describe their solution in GNAT. The design addresses the management of controlled operations on various entities, including dynamically allocated objects, transient objects (function results and aggregates), and composite objects containing controlled components. The interaction of the controlled type features with exceptions is also covered. Finally, we discuss alternative implementation approaches and possible enhancements to the current model.
The purpose of this paper is to describe the design and implementation choices that were made during the development of an Ada binding to the popular Gtk+ graphical toolkit.
Both Ada and Java support concurrent pro- gramming, but through quite different approaches.Ada has built-in tasking features with concurrency semantics, independent of the language’s OOP model, whereas Java’s thread support relies on OOP and is based on special execution properties of methods in several predefined classes. Ada achieves mutual exclusion through protected objects with encapsulated components; Java uses the classical “monitor” construct with “synchronized” methods/blocks. Ada models condition-based synchronization and communication through suspension objects, protected entries, and rendezvous; Java provides the low-level “wait” / “notification” methods. Both languages offer timing control; Ada additionally provides user-specifiable scheduling policies.
Compared to Java, Ada’s concurrency model is less susceptible to deadlock and race conditions. Neither language is intrinsically superior in run-time performance. In some areas Ada’s semantics entail less run-time overhead; in other areas Java may have the advantage.
Ada offers direct support for real-time programming through a combination of facilities in the core language and the Systems Programming and Real-Time Systems Annexes. Java lacks some critical functionality, and its semantics for thread scheduling are not completely defined. Depending on dynamic allocation and garbage collection, Java raises issues of time and space predictability. Work is in progress on making Java more applicable to real-time systems; at present Ada is the more appropriate language
Ada and Java offer comparable Object-Oriented Programming (“OOP”) support, but through quite different approaches in both their general philosophies and their specific features.
Each language allows the programmer to define class inheritance hierarchies and to exploit encapsulation, polymorphism, and dynamic binding. Whereas OOP forms the foundation of Java’s semantic model, OOP in Ada is largely orthogonal to the rest of the language. In Java it is difficult to avoid using OOP; in Ada OOP is brought in only when explicitly indicated in the program. Java is a “pure” OO language in the style of Smalltalk, with implicit pointers and implementation- supplied garbage collection. Ada is a methodology-neutral OO language in the manner of C++ , with explicit pointers and, in general, programmer-controlled versus implementation-supplied storage reclamation. Java uses OOP to capture the functionality of generics (“templates”), exception handling, multi-threading and other facilities that are not necessarily related to object orientation. Ada supplies specific features for generics, exceptions, and tasking, independent of its OO model. Java tends to provide greater flexibility with dynamic data structures and a more traditional notation for OOP. Ada tends to offer more opportunities for optimization and run-time efficiency, and greater flexibility in the choice of programming styles.
AdaCore has developed strategic alliances and partnerships allowing customers to benefit from an ever-increasing complementary range of tools and services.
At the University of Bristol and at the Bristol Robotics Laboratory we want to trust our robots. We develop their control software in Ada/SPARK and verify it using the latest technology from AdaCore. Within the RIVERAS project (Robust Integrated Verification of Autonomous Systems) we aim to create systems that behave predictable even in the face of unpredicted events.
Trustworthy by Design -- Correct by Construction
Today, even vital infrastructures like power grids, classified government networks or company research sites tend to be connected to the Internet to take advantage of remote management and cloud services. Traditional approaches to securing these infrastructures rely on a strict isolation of critical systems from untrusted networks. In the presence of critical networked environments, other strategies are required to prevent unauthorized access which may be gained through the exploitation of errors in the complex software stacks that are used. One solution are component-based high-assurance platforms where untrusted software components are strictly isolated from security-critical functions on one single physical system.
Vermont Technical College successfully launched a lunar cube satellite into orbit. The tiny satellite, measuring only 10 cm x 10 cm x 10 cm and weighing 1.1 kg, was launched into a 500 km earth orbit, where it will remain for about three years to test the systems that will be used for the eventual lunar mission. The CubeSat project is part of NASA’s ELaNa IV program (Educational Launch of Nano-satellites).
IPsec relies on the correct operation of the Internet Key Exchange (IKE) protocol to meet its security goals. The implementation of IKE is a non-trivial task and results in a large and complex code base. This makes it hard to gain a high degree of confidence in the correct operation of the code.
Prof. John Hatcliff and his team at Kansas State University’s Static Analysis and Transformation of Software (SAnToS) Laboratory have found the SPARK language technology to be an ideal research vehicle for exploring novel techniques in formal program verification. The SAnToS team has worked for over a decade on innovative tools that incorporate model checking, symbolic execution, data flow, and program dependence analyses. “We started out using Java”, said Prof. Hatcliff. “But Java is a large language with complex semantics, and it certainly wasn’t designed for, or often used in, safety-critical systems. It was hard for us to produce clean technical results and robust tools with Java, and to apply those tools to interesting safety-critical examples. SPARK has proved to be a much more appropriate base language.”
The DSP group at the University of Udine is developing PPETP (Peer-to-Peer Epi-Transport Protocol), a new streaming protocol based on a peer-to-peer approach that will allow to distribute efficiently live multimedia material to a large number of users. Initially aimed to the specific application of multimedia streaming, the protocol evolved with time and now it can be considered a general-purpose overlay multicast protocol with many features (e.g., efficient use of bandwidth, NAT-traversal built-in procedures, countermeasures against security issues specific to peer-to-peer networks) that make it suitable for efficient multimedia streaming.
At The Australian National University, students from the 2011 class in Concurrent and Distributed Systems provide an example of the high performance code they developed in undergraduate courses. The aim of the demo is to recharge all vehicles in a variable size swarm at an uncontrollable, roaming fuelling globe in a fully distributed manner. Each vehicle runs its own processes and can only communicate with nearby vehicles. It is a great example showing that GNAT is robust enough to serve as a workhorse in large multi-platform undergraduate class where substantial amounts of code is involved.
Dr. Martin C. Carlisle (former director of the Academy Center for Cyberspace Research at the USAF Academy, and now at Carnegie Mellon University) and Dr. Barry Fagin (US Air Force Academy) have developed a secure DNS server using Ada and the SPARK formal methods tool set. IRONSIDES is an authoritative DNS server that is provably invulnerable to many of the problems that plague other servers. It achieves this property through the use of formal methods in its design, in particular the language Ada and the SPARK formal methods tool set. Code validated in this way is provably exception-free, contains no data flow errors, and terminates only in the ways that its programmers explicitly say that it can. These are very desirable properties from a computer security perspective.
At Western Washington University, students are using Ada in senior capstone projects on real-time control of a model railway system. To assist in understanding the complexities of that system, WWU faculty member Martin Osborne has developed a simulator that runs virtual trains on a virtual layout identical to the physical layout in the lab, including all switches and sensors. Use of the simulator during problem analysis has helped students understand the factors to be considered in system specification. In later project stages, the simulator assists in design verification and in more extensive software testing than would be practical with the physical system.
Our purpose at the UPM is to provide a set of tools to fully develop a real-time application in Ada using as target the LEGO® Mindstorms® NXT robotics kit. These tools, working under Linux, provide real-time & embedded systems teachers with an alternative to conventional software models designed in classrooms and labs.
The Telecom Robotics club at Telecom ParisTech (an engineering college in the French Grandes Écoles system) is using Ada and the GNAT technology for its projects.
At the University of Virginia, Ada lies at the core of a comprehensive approach to creating software for safety-critical applications. Dr. John Knight and his student, Xiang Yin, have created a practical approach to formal verification called Echo. In Echo verification, a program written in SPARK Ada is verified to conform to its SPARK annotations using the SPARK tools.
At the Australian National University (ANU), Ada plays an integral part in teaching and research, at both the undergraduate and graduate levels. Dr. Uwe Zimmer has been using Ada, with the GNAT technology on Linux, Windows, Mac, and Embedded MPC5554, in two major courses: Concurrent and Distributed Systems, for Computer Science and Engineering students in their second year; and Real-Time and Embedded Systems, for Computer Science and Engineering students in their last year and for Masters students.
Under the direction of Professors Carl Brandon and Peter Chapin, students at Vermont Technical College are using AdaCore’s GNAT development environment along with Praxis’ SPARK tools on two NASA-sponsored programs with large software components.
Under the direction of Professor Lars Asplund, graduate students at Mälardalen University are designing, building and programming the Dasher robot in a project that is pushing the limits of robotics technology. The software is being developed with AdaCore’s GNAT toolset, furnished to the university under the GNAT Academic Program (GAP), on Wind River Systems’ VxWorks real-time operating system.
After seven years and 160 iterations, the Ada Gem of the Week series is coming to an end. At least in its current format, as it will be replaced by a blog that will still address technical subjects. But more about that later. For this last Gem we want to reflect on what has been a very successful and widely read series.
Perhaps surprisingly, the Ada standard indicates cases where objects passed to out and in out parameters might not be updated when a procedure terminates due to an exception. Let's take an example:
In the previous two Gems, we saw how aspects Static_Predicate and Dynamic_Predicate can be used to state properties of objects that should be respected at all times. This third and final Gem in the series is concerned with an aspect called Type_Invariant.
High-level APIAs mentioned in Part 1, GNAT.Command_Line also provides a higher-level API, where most of the handling is fully automatic. Here is an example of its use, similar to the example discussed in Part 1:
Applications can be configured in multiple ways. Among the most frequent are command-line options, configuration files, and graphical user interfaces. The GNAT technology provides various means to interface with those, respectively Ada.Command_Line and GNAT.Command_Line, GNATCOLL.Config, and GtkAda.
Let's get started...
In the first part of this two-part series we saw that stand-alone shared libraries have the required properties to be used as dynamic plug-ins. In this Gem we explore how to load and unload code dynamically within an Ada application. In essence, the dynamically loaded code is compiled into a shared library, and when this shared library is modified it is reloaded automatically.
In Gem #97, a reference-counting pointer was presented, where a Get function returns an access to the data. This could be dangerous, since the caller might want to free the data (which should remain under control of the reference type). In this Gem, we present a method to prevent the misuse of the result of Get.
The first part of this Gem described why having a Python interface might provide an effective way to customize and extend your application. It also highlighted how the GNAT Components Collection takes care of a good part of the work. This Gem will now go into the technical details of how you can use GNATCOLL.Scripts in practice. The GNATCOLL documentation provides additional details, so please refer to it if you need more information (see GNATColl: GNAT Reusable Components).
The GNAT Components Collection (GNATCOLL) has included, since the beginning, a collection of packages to easily interface your Ada applications with scripting languages. This is the layer used in the GPS IDE to provide extensibility via the GPS shell or Python. The use with the GPS shell is just a toy we initially used to bootstrap the process, and was kept for backward compatibility only. On the other hand, Python is an extensively used object-oriented language that comes with its own run-time library, and can be easily extended in C or Ada.
As we mentioned in the first two parts of this Gem series, GNATCOLL now includes a package that provides support for memory management using reference counting, including taking advantage of the efficient synchronized add-and-fetch intrinsic function on systems where it is available.
In Part 1, we described a reference-counted type that automatically frees memory when the last reference to it disappears. But this type is not task safe: when we decrement the counter, it might happen that two tasks see it as 0, and thus both will try to free the data. Likewise, the increment of the counter in Adjust is not an atomic operation, so it is possible that we will be missing some references.
Memory management is typically a complex issue to address when creating an application, and even more so when creating a library to be reused by third-party applications. It is necessary to document which part of the code allocates memory and which part is supposed to free that memory. As we have seen in a previous Gem, a number of tools exist for detecting memory leaks (gnatmem, GNATCOLL.Memory or valgrind). But of course, it would be more convenient if the memory were automatically managed.
Let's get started...Determining how much stack space should be allocated to tasks is a common memory-management problem. In the absence of tool support, often the only information that developers have is the output EXCEPTION_STACK_OVERFLOW when their program crashes. GNAT offers two basic ways for users to get information on a program's stack usage -- statically or dynamically. This Gem addresses how to obtain data on dynamic stack usage. Measurement of static stack usage will be covered in a later Gem.
Introduction In this series of Ada Gems we propose a set of code archetypes for the development of real-time systems. The code archetypes comply with the restrictions of the Ravenscar Profile, a subset of the Ada language specifically suited for the development of high-integrity real-time systems. The Ravenscar Profile was devised to guarantee that programs written in accordance with it are amenable to static analysis in the time dimension. In fact, the profile excludes all Ada constructs that are exposed to nondeterministic or unbounded execution time. In the space dimension, the profile prohibits the use of constructs that implicitly perform dynamic memory allocation.
Let's get started…
In the previous DSA Gem, we showed how subprograms in a package can be made remotely callable using a pragma Remote_Call_Interface (RCI for short). Each RCI unit is present in only one partition of a distributed application, and any call to a subprogram in such a unit made from another partition is transparently handled by the distribution run-time library.
Let's get started…Input validation consists of checking a set of properties on the input which guarantee it is well-formed. This usually involves excluding a set of ill-formed inputs (black-list) or matching the input against an exhaustive set of well-formed patterns (white-list).
Let's get started…The notions of tainted data and trusted data usually refer to data coming from the user vs. data coming from the application. Tainting is viral, in that any result of a computation where one of the operands is tainted becomes tainted too.
Let's get started…A number of semaphore definitions exist, although the general concept remains as introduced by Dijkstra in 1968. We assume the reader has some familiarity with semaphores and their semantics, and so we will not cover them here. Many books are available for those requiring additional information. See especially Principles of Concurrent and Distributed Programming by M. Ben-Ari.
Let's get started…Unless your coding standard forbids any dynamic allocation, memory management is a constant concern during system development. You might want to limit the amount of memory that your application requires, or you might have memory leaks (allocation chunks that are never returned to the system). The latter is a critical concern for long-running applications.
Let's get started…Unless your coding standard forbids any dynamic allocation, memory management is a constant concern during system development. You might want to limit the amount of memory that your application requires, or you might have memory leaks (allocation chunks that are never returned to the system). The latter is a critical concern for long-running applications.
Let's get started…Error message information leak occurs when secure data is leaked, through error messages, to unauthorised users, and is one of the top twenty-five most dangerous programming errors according to SANS Institute. The general problem is ensuring that information flow adheres to certain policies -- for example, certain data should never be written in an error message to a log file that may be accessible by unauthorised users.
Let's get started…An overflow error occurs when the capacity of a device is exceeded. Overflow errors are a source of quality and security concerns. For instance, when an arithmetic overflow occurs, a calculated value does not fit in its specified size, and the calculation (and the program) just stops. Buffer overflow happens when a process stores data in a buffer outside of the memory that the programmer set aside for it. Buffer overflow errors are widely known to present a vulnerability to malicious hackers, who might exploit the error to sneak their own code onto a victim's disk, storing it outside of the intended buffer.
Let's get started…In this Gem, we will see how the SPARK tools detect any differences between a program's intended behaviour, as specified in its contract, and its actual behaviour, as implemented in the code. Thus the SPARK tools can be used either to find defects in the contract, to find defects in the implementation, to find defects in both, or to show conformance between intended and actual behaviour.
Let's get started…Input validation ensures that your program's input conforms to expectations - for example, to ensure that the input has the right type. But validation requirements can be much more complicated than that. Incorrect input validation can lead to security and safety problems since many applications live in a "hostile" environment and the input might be constructed by an attacker. "It's the number one killer of healthy software..." according to the CWE/SANS list of the top twenty-five most dangerous programming errors.
Let's get started…Every statement should have a purpose. An ineffective statement has no effect on any output variable and therefore has no effect on the behaviour of the code. The presence of ineffective statements reduces the quality and the maintainabiliy of the code. The SPARK Toolset identifies all ineffective statements.
Let's get started…Note: This series of Gems makes references to SPARK and the Tokeneer project, which you can find out more about by visiting http://www.adacore.com/home/products/sparkpro/tokeneer/. See also the SPARK tutorial at http://www.adacore.com/home/products/sparkpro/tokeneer/discovery/.
Let's get started…Like the classical “monitor” concept on which they are based, protected types provide mutually exclusive access to internal variables. Clients can only access these variables indirectly, by means of a procedural interface. This interface is very robust because mutually exclusive access is provided automatically: users cannot forget to acquire the underlying (logical) lock and cannot forget to release it, including when exceptions occur. As a result, encapsulating actions within protected operations is highly recommended.
Let's get started…
In the last Gem, we proved that procedure Linear_Search was free from uninitialized variable accesses and run-time errors, which are safety properties of Linear_Search.
Let's get started…
With Altran and AdaCore now teaming up to offer an integration of SPARK technology inside GPS (see http://www.adacore.com/home/products/sparkpro/), many GPS users will be interested in trying out the proof capabilities of SPARK on their own Ada programs. Of course it's a little more involved than that. SPARK is not only a set of tools for verifying high-assurance systems, but also incorporates a language that must be learned.
Let's get started…When you open GPS initially, it shows a number of views: the Messages window (which can never be closed), the Project View, showing the list of files in your project, the Outline View, which shows the list of subprograms in the current edit, the Scenario View listing the scenario variables in your project, and a Welcome window to help you get started.
Let's get started…GNAT allows for a great deal of flexibility in compiling applications. The traditional method is to use gnatmake on the command line, specifying the list of source directories by using "-I" switches, and letting gnatmake decide which files need to be recompiled. One drawback of this approach is that it only works for Ada files. If your application uses sources written in other languages (which is probably the case for the majority of serious applications), then you need some kind of wrapper around gnatmake. This is typically done via a Makefile: first you recompile C, C++, and other source files using standard Makefile techniques, then invoke gnatmake to handle the Ada sources, and finally (although this can also be done as part of gnatmake) bind and link your application.
Let's get started…In lots of legacy systems that were initially developed with technologies other than GNAT, a single source file might include several Ada units (or both spec and body of a single unit).
Let's get started…One of Ada's key strengths has always been its strong typing. The language imposes stringent checking of type and subtype properties to help prevent accidental violations of the type system that are a common source of program bugs in other less-strict languages such as C. This is done using a combination of compile-time restrictions (legality rules), that prohibit mixing values of different types, together with run-time checks to catch violations of various dynamic properties. Examples are checking values against subtype constraints and preventing dereferences of null access values.
Let's get started…Generating bindings for C++ headers is done using the same options as for C headers, again using the G++ driver. This is because the binding generation tool takes advantage of the full C and C++ front ends readily available with GCC, and then translates its internal representation into corresponding Ada code.
Let's get started…GNAT now comes with a new experimental binding generator for C and C++ headers which is intended to do 95% of the tedious work of generating Ada specs from C or C++ header files. Note that this is still a work in progress, not designed to generate 100% correct Ada specs.
Let's get started…Suppose we have an API (Application Program Interface) on the Ada side that we would like to call from Java. This API may be based on a set of types and functions, for example:
Let's get started…A lot of applications have a need to execute commands on the machine. There are several use cases: a program might wish to wait for a command to complete (for instance the command generates a file that the application then needs to parse); it might spawn a command in the background and continue to execute in the meantime; or it might need to interact with an external application (sending data to its input stream and reading its output).
Let's get started…It is hoped that this booklet will have proved interesting. It has covered a number of aspects of writing reliable software and hopefully has shown that Ada is a good language and source of inspiration to use for programs that matter.
Let's get started…The first thing a program generally has to do is to parse its command line to find out what features a user wants to activate. Standard Ada provides the Ada.Command_Line package, which basically gives you access to each of the arguments on the command line. But GNAT provides a much more advanced package, GNAT.Command_Line, which helps to manipulate those arguments, so that you can easily extract switches, their (possibly optional) arguments and any remaining arguments. Here is a short example of using that package:
Let's get started…For some applications, especially those that are safety-critical or security-critical, it is essential that the program be correct, and that correctness be established rigorously through some formal procedure. For the most severe safety-critical applications the consequence of an error can be loss of life or damage to the environment. Similarly, for the most severe security-critical applications the consequence of an error may be equally catastrophic such as loss of national security, commercial reputation or just plain theft.
Let's get started…Ada allows overloading of subprograms, which means that two or more subprogram declarations with the same name can be visible at the same place. Here, "name" can refer to operator symbols, like "+". Ada also allows overloading of various other notations, such as literals and aggregates.
Let's get started…In real life many activities happen in parallel. Human beings do thing in parallel with considerable ease. Females seem to do this better than males – perhaps because they have to rock the baby while cooking the food and keeping the tiger out of the cave. The male typically just concentrates on one thing at a time such as catching that rabbit for dinner – or trying to fin his in-law’s cave without asking for directions.
Let's get started…A program that doesn't communicate with the outside world in some way is useless although very safe. Such a program might almost be in solitary confinement. A prisoner in solitary confinement is safe in the sense that he cannot hurt other people but he is equally of no use to society either.
Let's get started…In Gems #1 and #2, we showed how the accessibility rules help prevent dangling pointers, by ensuring that pointers cannot point from longer-lived scopes to shorter-lived ones. But what if you want to do that?
Let's get started…The memory of the computer provides a vital part of the framework in which the program resides. The integrity of the memory contents is necessary for the health of the program. There is perhaps an analogy with human memory. If the memory is unreliable then the proper functioning of the person is seriously impaired.
Let's get started…This chapter covers a number of aspects of the control of objects. By objects here we mean both small objects in the sense of simple constants and variables of an elementary type such as Integer and big objects in the sense of Object-Oriented Programming.
Let's get started…Ada 2005 allows the use of anonymous access types in a more general manner, adding considerable power to the object-oriented programming features of the language. The accessibility rules have been correspondingly augmented to ensure safety by preventing the possibility of dangling references. The new rules have been designed with programming flexibility in mind, as well as to allow the compiler to enforce checks statically.
Let's get started…OOP took programming by storm about twenty years ago. Its supreme merit is said to be its flexibility. But flexibility is somewhat like freedom discussed in the Introduction – the wrong kind of flexibility can be an opportunity that permits dangerous errors to intrude.
Let's get started…Ada has the notion of “streams” that are much like those of other languages: sequences of elements comprising values of arbitrary, possibly different, types. Placing a value into a stream is easy using the language-defined “stream attributes”. The programmer simply calls the type-specific attribute routine and specifies the stream and the value. For example, to place an Integer value V into a stream S, one could write the following:
Let's get started…When speaking of buildings, a good architecture is one whose design gives the required strength in a natural and unobtrusive manner and thereby provides a safe environment for the people within. An elegant example is the Pantheon in Rome whose spherical shape has enormous strength and provides an uncluttered space. Many ancient cathedrals are not so successful, and need buttresses tacked on the outside to prop up the walls. In 1624, Sir Henry Wooton summed the matter up in his book, The Elements of Architecture, by saying "Well building hath three conditions – commoditie, firmenes & delight". In modern terms, it should work, be strong and be beautiful as well.
Let's get started…To recap Part 1, protected types add an efficient building block to the tasking facilities of Ada. Mutual exclusion is automatically provided and condition synchronization is directly expressed via entry barriers, all without the expense of task switching. As such, protected types are a natural implementation approach for a circular bounded buffer used in a concurrent programming context. The complete declaration of the generic package and encapsulated protected type are shown below, including now the private part. (We have omitted the comments in the code since we cover them in the description.)
Let's get started…Primitive man made a huge leap forward with the discovery of fire. Not only did this allow him to keep warm and cook and thereby expand into more challenging environments but it also enabled the creation of metal tools and thus the bootstrap to an industrial society. But fire is dangerous when misused and can cause tremendous havoc; observe that society has special standing organizations just to deal with fires that are out of control.
Let's get started…The bounded buffer is a classic concurrent programming component exhibiting asynchronous task interactions. The concept is that of a buffer of a fixed size that is accessed by multiple tasks, some inserting items and some removing them, concurrently and asynchronously. Hence the buffer implementation must be protected against race conditions in which the tasks access the implementation in an interleaved manner and thereby corrupt the representation. In addition to this “mutually exclusive access”, the buffer also requires “condition synchronization”, in which callers are kept waiting until the requested buffer has the necessary state. For example, a task cannot remove an item from a buffer when the buffer is empty. Likewise, an item cannot be put into a buffer when the buffer is full.
Let's get started…Ada is a block-structured language, which means the programmer can nest blocks of code inside other blocks. At the end of a block, all objects declared inside of it go out of scope, meaning they no longer exist, so the language disallows pointers to objects in blocks with a deeper nesting level.
Let's get started…Syntax is often considered to be a rather boring mechanical detail. The argument being that it is what you say that matters but not so much how it is said. That of course is not true. Being clear and unambiguous are important aids to any communication in a civilized world.
Let's get started…The notion of preconditions and postconditions is an old one. A precondition is a condition that must be true before a section of code is executed, and a postcondition is a condition that must be true after the section of code is executed.
Let's get started…The aim of this booklet is to show how Ada 2005 addresses the needs of designers and implementers of safe and secure software. The discussion will also show that those aspects of Ada that make it ideal for safety-critical and security-critical application areas will also simplify the development of robust and reliable software in many other areas.
Let's get started…This Gem presents a basic introduction the Ada Web Server (AWS). The core components of AWS comprise a Web server which supports the HTTP protocol. This Web server can be embedded into any application. Common usages are:
Last week, we discussed the use of derived types and representation clauses to achieve automatic change of representation. More accurately, this feature is not completely automatic, since it requires you to write an explicit conversion. In fact there is a principle behind the design here which says that a change of representation should never occur implicitly behind the back of the programmer without such an explicit request by means of a type conversion.
Let's get started…A powerful feature of Ada is the ability to specify the exact data layout. This is particularly important when you have an external device or program that requires a very specific format. Some examples are:
Let's get started…The Ada standard defines several subprograms related to searching text in a string. In addition, GNAT provides additional packages to search. This gem will cover the various possibilities.
Let's get started…Ada, like many languages, defines a special 'null' value for access types. All values of an access type designate some object of the designated type, except for null, which does not designate any object. The null value can be used as a special flag. For example, a singly-linked list can be null-terminated. A Lookup function can return null to mean "not found", presuming the result is of an access type:
Let's get started…The only characters allowed in an Ada 83 program (for strings, comments, and identifiers) were 7-bit ASCII symbols. That was annoying. In Ada 83 we could not write:
Let's get started…There are two main APIs to parse an XML file. One (the Document Object Model, DOM) reads the file and generates a tree in memory representing the whole document. Typically, because of the amount of operations mandated by the specifications, this tree is several times larger than the document itself, and thus depending on the amount of memory on your machine, it might limit the size of documents your application can read. On the other hand, it provides a lot of flexibility in the handling of these trees.
Let's get started…Data persistence can be achieved in many ways starting as simple as using hand-written code to store and load data into some text files to something as complex as mapping the data into a relational or object database for example.
Let's get started…Since Ada 95 it has been possible to stream any object. Using 'Input/'Output or 'Read/'Write attributes, any object (tagged or not) can be streamed using a binary representation. This means that objects can be written into a file or sent over a socket, for example.
Let's get started…The recent "gems" about pragma No_Return talked a lot about compile-time checks that generate warnings. Indeed, GNAT is capable of generating lots of useful warnings. Here is some advice about how to get the most out of these warnings.
Let's get started…A function should always return a value or raise an exception. That is, reaching the "end" of a function is an error. In Ada, this error is detected in two ways:
Let's get started…Did he ever return,No he never returnedAnd his fate is still unlearn'dHe may ride forever'neath the streets of BostonHe's the man who never returned.-- from "Charlie on the M.T.A."-- by The Kingston Trio
Let's get started…Timers are essential software elements of embedded and real-time systems. Thus, making an intuitive and easy way to create timers helps in the software design process. Ada provides a predefined package named Ada.Real_Time.Timing_Events for doing just that. With this package, a timer, one-shot or periodic one, can be created with a breeze. Furthermore, these timers can be genericized for different durations. Going one step further these generic timers can be combined in a single generic package as shown below along with the test codes. Note that the test codes are pretty crude. However, the output is printed out for each second approximately. Thus, the test results can be checked using one thousand count rule, one thousand one, one thousand two...
Let's get started…Last week we introduced this topic and explored the first of the two designs. The gist of it is that we want to implement a multi-level response to interrupts, in which a protected procedure implements the first-level handler and a task implements the secondary level handling outside of the interrupt context. We use serial communications over a UART (Universal Asynchronous Receiver Transmitter) as the example. In both designs we encapsulate the two levels of the interrupt handling code inside the body of a package named Message_Processor.
Let's get started…Recall that, in Ada, protected procedures are the standard interrupt-handling mechanism. This approach has a number of advantages over the “traditional” use of non-protected procedures. First, normal procedures don’t have a priority, but protected objects can have an interrupt priority assigned and are thus integrated with the overall priority semantics. Execution of entries and procedures within the protected object will execute at that level and only higher-level interrupts can preempt that execution. Thus no race conditions are possible either. Additionally, condition synchronization is expressed directly, via entry barriers, making interaction with other parts of the system easy to express and understand. Finally, protected objects support localization of data and their manipulating routines, as well as localization of multiple interrupt handlers within one protected object when they each need access to the local data.
Let's get started…In the last gem, we used a stack class to demonstrate factory functions (to construct iterator objects), and implemented an assignment operation that dispatched on the type of the target stack. We mentioned in passing that that operation could be implemented by dispatching on the source stack, so let's show how to do that.
Let's get started…On an unusually hot end-of-summer day some years ago, I stepped into the Courant Institute of Mathematical Sciences. It was my first day of class at New York University and my first day with Ada. The heat was pounding and the classroom air-conditioning unit was being repaired.
Let's get started…One of the major changes to the Ada language is the addition of interfaces, stateless types that specify a set of operations. Like a tagged type, you can derive from an interface type, but unlike a tagged type, you can derive from multiple interfaces simultaneously.
Let's get started…IntroductionPulse Width Modulation (PWM) is a common mechanism for encoding analog information on a digital line, and is commonly used in control signals. It consists of generating pulses on the digital line. The width of the pulse, i.e., the time interval during which the signal is high (or low), is proportional to the analog value that is used as a control signal.
Let's get started…
Given that Ada 2005 allows build-in-place aggregates for limited types, the obvious next step is to allow such aggregates to be wrapped in an abstraction — namely, to return them from functions. After all, interesting types are usually private, and we need some way for clients to create and initialize objects.
Let's get started…
Last week, we noted that Ada 2005 allows aggregates for limited types. Such an aggregate must be used to initialize some object (which includes parameter passing, where we are initializing the formal parameter). Limited aggregates are “built in place” in the object being initialized.
AdaCore’s tools and services are the ideal choice for developing large, long-lived Air Traffic Management systems, where safety and security is paramount.
AdaCore provides software developers in the in the Avionics industry with qualified tools and certified runtimes to meet the DO-178C standard requirements.
AdaCore provides qualified tools and certified runtimes to Space industry developers building critical software meeting ECSS certification requirements.
What is ESARR? ESARR 4 is the EUROCONTROL Safety Regulatory Requirement “Risk Assessment and Mitigation in Air Traffic Management". Read here for more.
This guide documents GPR technology, a project framework designed for the description and construction of large multi-language systems organized into subsystems and libraries.
NEW YORK and PARIS and BURLINGTON, Mass., November 15, 2017 – AdaCore Tech Days – AdaCore today announced that MDA, a business unit of Maxar Technologies, has selected the GNAT Pro Assurance Ada development environment for the LEON3 target processor, to produce the software for a Ku-Band communication subsystem that will replace the current version. This critical International Space Station (ISS) subsystem has to work reliably over the long term, a requirement that led MDA to maintain Ada as the implementation language. With GNAT Pro Assurance, a service known as sustained branches allows MDA to continue developing and maintaining their software over the long term using a specific version of the GNAT Pro technology, with access to code generator updates to correct critical issues.
This guide describes the use of GNAT, a compiler and software development toolset for the full Ada programming language. It describes the features of the compiler and tools, and details how to use them to build Ada applications.
This guide describes the use of GNAT Pro, a compiler and software development toolset for the full Ada programming language, in a cross compilation environment.
AdaCore will be exhibiting at this event, Cyrille Comar will present "What is software safety? A journey across domains and safety standards" and "Avionics Certification: Back to Fundamentals with Overarching Properties" and Yannick Moy will present "Safe and Secure Autopilot Software for Drones" and "Lightweight checkers in a new light"
AdaCore will attend and present papers at FOSDEM. Yannick Moy will present “SPARK Language: Historical Perspective & FOSS Development”. Fabien Chouteau will present “Making the Ada_Drivers_Library: Embedded Programming with Ada”. And Raphaël Amiard and Pierre-Marie de Rodat will present “Easy Ada Tooling with Libadalang”.
New GNAT Pro Product LinesGNAT Pro Assurance Selectedfor MDA Space ApplicationDr. Peter Chapin Receives
2017 Robert Dewar AwardSustained BranchesTech Days 2017Make with Ada Winners AnnouncedSPARK DiscoverySpotlighting a GAP Member:
US Air Force Academy (Colorado Springs, CO)Interview with Robert TiceNew Product ReleaseGNAT Pro CCG Expands Ada AvailabilityGNAT Pro on iOS and Android
AdaCore software development and verification tools help Real Heart deliver the high assurance, safety, and reliability that lifesaving medical devices demand.
Ada public training courses target software professionals looking for a practical introduction to the Ada language features, including those in Ada 2012.
Sound Static Analysis for Security: this two-day workshop is focused on decreasing software security vulnerabilities. Sign up today to attend the event.
The Sound Static Analysis for Security Workshop will be held at NIST in Gaithersburg, MD. Accommodations and transport are available at the Holiday Inn
AdaCore technical staff will present the latest news about the company's current and planned product offerings and activities at this free event in Paris.
Ada was designed for use in real-time embedded systems, and is commonly regarded as one of the safest and most secure languages. This makes it particularly relevant for use in mission- and safety-critical applications, where safety standards such as DO-178C require that evidence be provided to demonstrate that hardware/software platforms operate within a required safety level. This evidence can be furnished by the GNAT Pro toolset and the Rapita Verification Suite (RVS), complementary tools that can help ensure software’s safety and adherence to coding guidelines and can collect evidence needed for certification from tests of the software.
Dr. Wheeler will provide an overview of how sound static analysis approaches can facilitate the development of higher quality and more secure software.
Dr. K. Rustan M Leino is a Senior Principal Engineer at Amazon. He is known for his work on formal techniques and tools for verifying software correctness.
Laurent Voisin has been applying formal methods in industry for 20 years. He has gained experience in using formal methods in actual development projects.
Claire has a PhD in computer science specialized in formal proof of programs. She has been working as a software developer and proof expert at AdaCore.
David Cok is a researcher in formal methods and deductive verification, with an emphasis on practical application to industrial software. See his talk.
Rod is working on merging the discipline of traditional high-integrity processes with agile approaches and the philosophy of the Lean Engineering Movement.
Julien Signoles is one of the main developers of Frama-C, a code analysis framework for C code, and the author of E-ACSL, its runtime verification plug-in.
David Mentré focuses his research on Formal Methods as a way to ensure 100% correctness of crucial properties in safety critical systems at a lower cost.
Joe Kiniry will focus on opportunities and challenges in using several Frama-C plugins as compared to comparable tools for other platforms and languages.
Sound Static Analysis for Security: this two-day workshop is focused on decreasing software security vulnerabilities by orders of magnitude, using the strong guarantees that only sound static analysis can provide. The workshop is aimed at developers, managers and evaluators of security-critical projects, as well as researchers in cybersecurity.
Building secure software is a challenging task. It seems that almost every
week we read the news about yet another computer system that has
failed in some way in the face of malicious or accidental misuse. “Cyber
Security” is a wide-ranging field, spanning human factors, hardware
design, sociology, and legal issues, in addition to software engineering.
This booklet summarizes the contribution that the Ada and SPARK
languages and AdaCore’s tools can make to this final area—how to
develop and verify correct and secure software.
Unlike AdaCore’s previous guides to airborne and rail system software,
this booklet does not follow the structure or requirements of a particular
standard—in part because there is no widely used security standard that
is required in practice. Instead it offers a more general treatment of the
problem, but also includes an analysis of how AdaCore’s technologies
help address the weaknesses identified in the MITRE Corporation’s
Common Weakness Enumeration (CWE). The content is based on the
authors’ many years of practical experience in the development of
high-end secure systems, the design of the Ada and SPARK programming
languages, and research into program verification tools.
The booklet is intended for readers who are involved with software at
any level (developers, project managers, procurement personnel) and
who would like to learn how currently available technology can help
address some of the most serious challenges associated with software and
security. Our goal is to provide useful guidance both to those who are
using other languages and are interested in the benefits that Ada offers,
and to existing Ada users who might be confronted with new security
requirements.
This book is a sampling of AdaCore blogs, including some of our
engineers’ ARM project creations! They illustrate how embedded
system developers can take advantage of Ada’s benefits in software
reliability, early error detection, code readability, and maintainability
while still satisfying performance requirements.
The blogs were written by Raphaël Amiard, Jonas Attertun, Arnaud
Charlet, Fabien Chouteau, Tristan Gingold, Anthony Leonardo Gracio,
Johannes Kanig, Jérôme Lambourg, Yannick Moy, Jorge Real,
J. German Rivera, Pat Rogers and Rob Tice.
There is a strong link between software quality and software reliability. By decreasing the probability of imperfection in the software, we can augment its reliability guarantees. At one extreme, software with one unknown bug is not reliable. At the other extreme, perfect software is fully reliable. Formal verification with SPARK has been used for years to get as close as possible to zero-defect software. We present the well established processes surrounding the use of SPARK at Altran UK, as well as the deployment experiments performed at Thales to fine-tune the gradual insertion of formal verication techniques in existing processes. Experience of both long-term and new users helped us define adoption and usage guidelines for SPARK based on five levels of increasing assurance that map well with industrial needs in practice.
Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of human effort required to design adequate formal specifications and to successfully discharge the required proof obligations. To popularize deductive verification in an industrial software development environment, it is essential to provide means to progressively transition from simple and automated approaches to deductive verification. The SPARK environment, for development of critical software written in Ada, goes towards this goal by providing automated tools for formally proving that some code fulfills the requirements expressed in Ada contracts.
In a program verifier that makes use of automatic provers to discharge the proof obligations, a need for some additional user interaction with proof tasks shows up: either to help analyzing the reason of a proof failure or, ultimately, to discharge the verification conditions that are out-of-reach of state-of-the-art automatic provers. Adding interactive proof features in SPARK appears to be complicated by the fact that the proof toolchain makes use of the independent, intermediate verification tool Why3, which is generic enough to accept multiple front-ends for different input languages. This paper reports on our approach to extend Why3 with interactive proof features and also with a generic client-server infrastructure allowing integration of proof interaction into an external, front-end graphical user interface such as the one of SPARK.
AdaCore’s advanced software development and verification tools help enhance the safety and security of automotive, autonomous, and advanced driver-assistance systems while facilitating future technology upgrades and requirements.
Abstract. Handling memory in a correct and efficient way is a step toward safer, less complex, and higher performing software-intensive systems. However, languages used for critical software development such as Ada, which supports formal verification with its SPARK subset, face challenges regarding any use of pointers due to potential pointer aliasing. In this work, we introduce an extension to the Ada language, and to its SPARK subset, to provide pointer types (“access types” in Ada) that provide provably safe, automatic storage management without any asynchronous garbage collection, and without explicit deallocation by the user. Because the mechanism for these safe pointers relies on strict control of aliasing, it can be used in the SPARK subset for formal verification, including both information flow analysis and proof of safety and correctness properties. In this paper, we present this proposal (which has been submitted for inclusion in the next version of Ada), and explain how we are able to incorporate these pointers into formal analyses.
Ada is a state-of-the art programming language used for critical software: fsmall-footprint, real-time embedded systems to large-scale enterprise systems.
The High Integrity Language Technology is focused on the cyber-resilience needs of critical software systems, where such a system must be trusted to maintain a continual delivery of services, as well as ensuring safety in its operations. Such needs have common goals and shared strategies, tools, and techniques, recognizing the multiple interactions between security and safety.
This workshop is designed as a forum for communities of researchers and practitioners from academic, industrial, and governmental settings, to come together, share experiences, and forge partnerships focused on integrating and deploying tool and language combinations to address the challenges of building cyber-resilient software-intensive systems. The workshop will be a combination of presentations and panel discussions, with one or more invited speakers.
AdaCore is an active actor and part of the Organizing and Program Committees.
Libadalang is a library for parsing and semantic analysis of Ada code. It is meant as a building block for integration into other tools (IDE, static-analyzers, etc..). This documentation provides a guide to use Libadalang and references for its various APIs.
Much has been written about impact of IoT. There are new customer requirements, new business models, and competitive pressure all driving change within engineering organizations. These shifting requirements have catalyzed more and more need for connectivity middleware, remote management capabilities and increasing interest in technologies like machine vision and energy harvesting. This document looks at the contributions that Ada can provide in controlling the associated costs.
AdaCore Technologies for Cybersecurity AvailableCodePeer Support for the Common Weakness EnumerationSmaller and More Secure with SPARKAdaCore Training ServicesWorkshop on Sound Static Analysis for SecurityNew Platform SupportAdaCore BlogsInterview with Emma AdbyTech Days 2018Put Some SPARK in Your Ada
The High Integrity Software Conference will take place in Bristol on 6November 2018. Now entering its fifth year, the conference continues to be the premier annual forum for the sharing of challenges, best practice and experience between software engineering practitioners – for software that matters. This mission continues to grow in importance, with 2018 having once again been a year in which software fallibility, cybersecurity breaches and the loss of public trust in autonomous systems have made headlines.
AdaCore offers training, on-site consulting and custom development services for all of our products to help make the most of our technology and expertise.
This is the documentation for the core packages of GNATcoll, a library providing a number of modules that can be reused in your own applications to add extra features or help implementation.
AdaCore will attend and present at FOSDEM 2019. In the Ada devroom, Nicolas Roche will present 'GSH: an Ada POSIX Shell to Speed Up GNU Builds on Windows' and Yannick Moy will present 'Proof of Pointer Programs with Ownership in SPARK'. In the RISC-V devroom, Fabien Chouteau will present 'Alternative languages for safe and secure RISC-V programming'.
V19 Product ReleaseVDC Report: Ada Helps Reduce CostsAdaCore Awarded Air Force Research Contract for System-to-Software Integrity SupportTech Days 2018AdaCore at HIS 2018 ConferenceInterview with Joël BrobeckerAda on General Purpose GPUsAdaCore at Future Airborne Capability Environment (FACETM) Technical Interchange MeetingNew AdaCore OfficeExcerpts from the AdaCore Blogosphere
MISRA C appeared in 1998 as a coding standard for C; it focused on avoiding error-prone programming features of the C programming language rather than on enforcing a particular programming style. The popularity of the C programming language, as well as its many traps and pitfalls, have led to the huge success of MISRA C in domains where C is used for high-integrity software. This success has driven tool vendors to propose many competing implementations of MISRA C checkers. Tools compete in particular on the coverage of MISRA C guidelines that they help to enforce, as it is impossible to enforce the 16 directives and 143 rules (collectively referred to as guidelines) of MISRA C. In particular, 27 rules out of 143 are not decidable, so no tool can always detect all violations of these rules without at the same time reporting "false alarms" on code that does not constitute a violation.
However, static analysis technology is available that can achieve soundness without inundating users with false alarms. One example is the SPARK toolset developed by AdaCore, Altran and Inria, which is based on four principles:
• The base language Ada provides a solid foundation for static analysis through a well-defined language standard, strong typing and rich specification features.
• The SPARK subset of Ada restricts the base language in essential ways to support static analysis, by controlling sources of ambiguity such as side-effects and aliasing.
• The static analysis tools work mostly at the granularity of an individual function, making the analysis more precise and minimizing the possibility of false alarms.
• The static analysis tools are interactive, allowing users to guide the analysis if necessary or desired.
This book presents the SPARK technology – the SPARK subset of Ada and its supporting static analysis tools – through an example-driven comparison with the rules in the widely known MISRA C subset of the C language.
An on-line and interactive version of this document is available at AdaCore's learn.adacore.com site.
In a report on the “Do’s and Don’ts for Software” [1], the Defense Innovation Board in the U.S. advises “Use modern languages and operating systems.... Treat software development as a continuous activity, adding functionality across its life cycle.” The Ada language fully supports these “do’s” with state-of-the-art features and a growing ecosystem, and is helping developers of critical cyber systems worldwide meet the most stringent software assurance requirements while reducing life cycle costs. For systems demanding reliable, secure and safe software, Ada continues to be the logical and cost-effective choice.
The need for safe and secure software — including Medical Device software — is becoming more important as cybersecurity threats in the healthcare sector become more frequent and severe. Beyond increasing the reliability, safety and security of their software, Ada and SPARK programming language adopters are also looking at controlling and reducing costs. Hillrom migrated to Ada and SPARK to verify the safety of the code by formally proving some properties, and improving its efficiency by removing dynamic checks, all the while keeping development and verification costs down. Read the full case study to find out more.
AdaCore technical staff will present the latest news about the company's current and planned product offerings and activities at this free event in Paris.
AdaCore’s technology provides the assurance that medical device developers, regulators, doctors and patients need so they can focus on saving human lives.
AdaCore will be presenting “Verifying High-Assurance FACE™ Components with Ada and SPARK” and is also exhibiting at this event.
The FACE™ TIM is an opportunity for Open Group FACE Consortium members to demonstrate their FACE certified and/or aligned products, present papers on utilization of the FACE Technical Standard, showcase efforts toward developing FACE applications for new war-fighting capabilities, and attend presentations from US Air Force leadership. Hundreds of Army, Navy, and Air Force personnel attend the yearly event, as well as other customer communities looking to learn more about the benefits of the FACE approach.
AdaCore is a Principal in the FACE Consortium and participates actively in the definition of the FACE Technical Standard to ensure Ada’s role in the Safety capability sets.
NORTHPORT AND NEW YORK, N.Y. – June 26, 2019 – Code Dx, Inc., provider of an award-winning application security management solution that automates and accelerates the discovery, prioritization, and risk management of software vulnerabilities, today announced its partnership with AdaCore, a trusted provider of software development and verification tools for the Ada, C, and C++ programming languages.
AdaCore will be presenting "A Qualified Multitasking Solution for Spacecraft Software Development" at this conference organized by the CNES and the ESA.
PARIS & NEW YORK & BRISTOL, UK, 14 August 2019 - AdaCore, a trusted provider of software development and verification tools, today announced the opening of AdaCore Ltd, which will serve as the company’s UK centre-of-excellence for the development of safety- and security-critical software tools.
There is no universal agreement on the order in which the successive bytes constituting a scalar value are stored. Some machines (so-called big-endian architectures) store the most significant byte first, while others (little-endian architectures) adopt the opposite convention. When porting an application across platforms that use different conventions, programmers need to convert data to the appropriate convention, and this may cause difficulties when exact memory layouts need to be preserved (e.g. for communication with legacy systems).
This paper describes the features of the Ada language that help supporting programmers in these situations, identifies some of their shortcomings, and introduces two novel solutions: a code generation approach based on data representation modeling, and a new representation attribute Scalar Storage Order , allowing the byte order convention to be specified for a given composite data structure.
This is a pre-copyedited version of a contribution that appeared in the proceedings of the Ada-Europe 2013 Reliable Software Technologies conference, published by Springer Verlag. The definitive authenticated version is available online via https://doi.org/10.1007/978-3-642-38601-5_5.
AdaCore Turns 25Make with Ada Winners AnnouncedTech Days EU and US Announced for 2019Roadmap Announced for GNAT Pro on Wind River VxWorks 7 SR066xx PlatformsAdaCore Joins RISC-V FoundationNew AdaCore BlogsGNAT Pro Available for C and C++Welcome GNAT Studio!Spotlighting a GAP Member: Institut Supérieur de l’Aéronautique et de l’Espace (Toulouse, France)AdaCore Ltd Is BornFrama-C & SPARK Day Explores Formal Verification MethodsAdaCore Now a Principal Member of the Open Group FACETM ConsortiumTech Day Held in Huntsville, Alabama
AdaCore and Altran today announce their renewed sponsorship of the annual High Integrity Software (HIS) Conference, taking place in Bristol on November 5th, 2019. Now in its sixth year, the event attracts leaders in industry and academia who share the common focus of producing high integrity software. This promises to be the pivotal event as we enter an age of digital dependency, and many aspects of our everyday lives rely on the correct behaviour of software-intensive electronic systems. The event addresses new, current and future challenges and continues to grow year on year. It welcome an international audience, with delegates from continental Europe to Japan. Recognising the need to engage new engineers on this key topic, there are special rates available for those at an early stage of their career.
Adacore emerged as a software company in 1994 after a 15-year involvement of an NYU team in defining and implementing the then-new programming language Ada
AdaCore will be exhibiting at this event. Microchip’s technical experts and partners will be presenting the most innovative space-related products, capabilities, and system solutions in this one-day technology forum. You will see demonstrations of how the interoperation of our latest products can accelerate your development time. You’ll also gain a comprehensive understanding of how Microchip’s Sub-QML and COTS-to-RT components help address the challenges of meeting system performance and reliability goals while also saving costs.
NEW YORK & PARIS & NEWPORT, Wales, September 24, 2019 - UK Space Conference - AdaCore, a trusted provider of software development and verification tools, today announced that the European Space Agency (ESA) has selected AdaCore to provide a qualified multitasking solution for spacecraft software development to support multiple ongoing and future ESA projects.
This is the GNAT Studio User's Guide. GNAT Studio is a complete integrated development environment that gives access to a wide range of tools and integrates them smoothly.
ERTS - Embedded Real Time Systems will celebrate its 10th edition from 29 to 31 January 2020 at Pierre Baudis Congress Center, Toulouse, France ! AdaCore will be sponsoring and exhibiting in the event.
This paper presents initial, positive results from using SPARK to prove critical properties of OpenUxAS, a service-oriented software framework developed by AFRL for mission-level autonomy for teams of cooperating unmanned vehicles. Given the intended use of OpenUxAS, there are many safety and security implications; however, these considerations are unaddressed in the current implementation. AFRL is seeking to address these considerations through the use of formal methods, including through the application of SPARK, a programming language that includes a specification language and a toolset for proving that programs satisfy their specifications. Using SPARK, we reimplemented one of the core services in OpenUxAS and proved that a critical part of its functionality satisfies its specification. This successful application provides a foundation for further applications of formal methods to OpenUxAS.
Extreme miniaturization coupled with increasingly higher computer performance, efficient communication of networked, often also mobile systems – the developers of embedded systems have to meet enormous requirements. The reliability of electronic systems, distributed intelligence, the internet of things and solutions for future themes such as e-mobility and energy efficiency are the main topics right at the top of the agenda for the embedded sector and industry.
Each year the embedded world Exhibition&Conference in Nuremberg offers the embedded community the opportunity to obtain information about new products and innovations, enter into an exchange and to maintain and develop valuable contacts. Around 1.100 exhibitors are presenting state-of-the-art technology in all facets of embedded technologies, from construction elements, modules and complete systems through to operating systems and software, hard and software tools right up to services covering all aspects of embedded systems.
The Safety-Critical Systems Symposium in 2020 comprises three days of presented papers with an industrial focus, including keynote talks, submitted talks, updates from the SCSC working groups and a poster session. There is also a symposium banquet with an after-dinner speaker.
The Symposium is for all of those working in the field of system and functional safety, including engineers, managers, consultants, regulators and assessors. It offers wide-ranging coverage of current safety topics, and a blend of academic research and industrial experience.
ParaSail is a language specifically designed to simplify the construction of programs that make full, safe use of parallel hardware even while manipulating potentially irregular data structures. As parallel hardware has proliferated, there has been an urgent need for languages that ease the writing of correct parallel programs. ParaSail achieves these goals largely through simplification of the language, rather than by adding numerous rules. In particular, ParaSail eliminates global variables, parameter aliasing, and most significantly, re-assignable pointers. ParaSail has adopted a pointer-free approach to defining complex data structures. Rather than using pointers, ParaSail supports flexible data structuring using expandable (and shrinkable) objects implemented using region-based storage management, along with generalized indexing. By eliminating global variables, parameter aliasing, and pointers, ParaSail reduces the complexity for the programmer, while still allowing ParaSail to provide flexible, pervasive, safe, parallel programming for irregular computations. Perhaps the most interesting discovery in this language development effort, based on over six years of use by the author and a group of ParaSail users, has been that it is possible to simultaneously simplify the language, support parallel programming with advanced data structures, and maintain flexibility and efficiency.
Open-source software, or, more accurately, Freely Licensed Open-Source Software (“FLOSS”), at first appears to present a dilemma when adopted as part of a business model. If users are allowed to access, modify and/or redistribute the source code, how does a company protect its intellectual property, and more fundamentally, sell something that can be easily and legally reproduced?
AdaCore has faced this issue since the company’s inception in 1994. Its major commercial product, GNAT Pro Ada, is an Ada development environment based on the Free Software Foundation’s (FSF’s) GNU Compiler Collection (GCC). AdaCore has implemented an Ada compiler front end and companion run-time libraries and tools and has contributed these components to the FSF. In turn, the GNAT Pro Ada compiler incorporates the GCC back end for a variety of target architectures. Leveraging the GCC back end has enabled AdaCore to make Ada available on a wide range of platforms, both native and embedded, at a significantly reduced effort – indeed, that was the technical rationale for choosing GCC and a design goal of GCC itself. But the challenge of this approach is how to generate a sustained and profitable business. AdaCore's 25 years of FLOSS experience offers an explanation and “lessons learned”.
FOSDEM is a free event for software developers to meet, share ideas and collaborate. Every year, thousands of developers of free and open source software from all over the world gather at the event in Brussels.
AdaCore will present at the biggest online Automotive event Scale Up 360° AUTOMOTIVE AI. Rob Tice will be giving a talk on "Beyond the boundaries of C: writing ASIL-4 software with verification-centric language SPARK Ada and Formal Proof".
NEW YORK & PARIS, February 18, 2020 - AdaCore today announced that three of its signature software development/verification tools for Ada, SPARK and C have been qualified under the ISO 26262 and IEC 61508 functional safety standards. AdaCore has over two decades of certification experience in safety-critical domains such as avionics, space, and rail. By completing the qualification process for automotive and industrial standards, the company has shown that its high integrity technologies can meet the demanding assurance requirements of the software-intensive automotive industry.
The size and complexity of software in embedded systems are growing at an astonishing rate. From aircraft and automobiles to medical devices, home appliances, and our homes themselves, products that were once hardware-only are now cyber-physical: they rely on software for much of their functionality. And we rely on that software for the dependability of those systems, especially their safety and security. This increasing complexity is driving technology leaders to adopt formal methods.
ISO 26262 is a functional safety standard for automotive systems and a derivative of the generic IEC 61508 standard for programmable electronic systems.
This is the documentation for GNATcoll binding to Syslog, the system logger on Unix systems. This provides a low level interface to syslog as well as a higher level interface to be used through the GNATCOLL. Traces system, from the GNATCOLL Core packages.
AdaCore recently extended its support of C and C++ toolchains and now supports not only native environments (such as Linux or Windows) but also cross ones such as VxWorks, embedded Linux, and even bare metal (C only at the time of this writing). In a world where most developers have access to a C/C++ toolchain that’s included with hardware or OS environments, this produces a question - what’s the added value of a commercially supported compiler for C and C++?
Webinar on NVIDIA Use of SPARK for Secure FirmwareAdaCore UK Participating in HICLASS ProgramTech Days 2019V20 Product ReleaseAdaCore in SpaceAdaCore Toolsuite for Ada, SPARK, and C Qualified under ISO 26262 and IEC 61508GNAT Ada Targeted to LLVMSpotlighting a GAP Member: Universidad Politécnica de Madrid (Spain)Enhancements to learn.adacore.comBlog Summary: RecordFlux- A Secure SPARK-Based Message Parsing FrameworkGNAT Pro C++ Available for Embedded Applications
AdaCore is the premier sponsor of this event and CEO Franco Gasperoni will be presenting the Welcome Address.
The Open Group and NAVAIR will host this 2nd annual joint FACE™ (Future Airborne Capability Environment) and SOSA™ (Sensor Open Systems Architecture) Consortia Technical Interchange Meeting. AdaCore is the Premier Sponsor of this year’s free, one-day, virtual event offering paper presentations by leading experts from government, industry, and academia on the use of the FACE Technical Standard and related business practices.
This unique event offers a valuable opportunity to learn the latest developments in the FACE and SOSA communities. Attendees will discover new and practical technologies that greatly increase defense program efficiency, accelerate acquisition of the latest capabilities, and improve adaptability in currently fielded systems.
AdaCore has cancelled this year's Tech Day in Paris due to COVID-19. Please check out our Product Roadmap 2020 Videos for information about the most recent updates.
AdaCore has cancelled this year's US Tech Day due to COVID-19. Please check out our Product Roadmap 2020 Videos for information about the most recent updates.
RISC-V is breaking down technical barriers and disrupting traditional microprocessor business models through global collaboration. The RISC-V Global Forum is our opportunity to engage across the community, from start-ups to multi-nationals, from students to luminaries, from deep technical talks to understanding industry momentum.
RTI ConnextCon 2020 is the world’s largest gathering of power Data Distribution Service (DDS) users. It will also serve as a great overview of the DDS standard for both current DDS users and non-DDS users alike.
RISC-V Days Tokyo is the largest RISC-V conference in Japan for suppliers, researchers, and government agencies. In 2020, it will be online so that both presenters, participants in shelter-in-place will be able to participate.
AdaCore will present the webinar “Confident Algorithms with Formal Proof Techniques” as part of ScaleUp 360°Auto Vision - The digital event deep diving into Computer Vision and Sensor Fusion technologies for autonomous vehicle perception.
The development of high integrity software-based systems is always challenging, and in current times it is an engineering discipline that has had to respond rapidly to a changing global environment. In this context, innovation has become even more essential as we respond to changes in the ways we work, changes in the tools we use on a day-to-day basis, and adapt the technologies we produce as we respond rapidly to changing market demands.
Our three speakers from globally recognised companies will present their own perspectives on these challenges – the lessons learnt and how the situation will evolve for their organisations as we move forwards.
AdaCore are co-organisers and sponsors of this conference with our partners, Altran.
AdaCore is participating on both the organizing and program committees for this year's HILT international workshop on safe languages and technologies for structured and efficient parallel and distributed/cloud computing.
This is the sixth in the HILT series of conferences and workshops, sponsored by ACM SIGAda, focused on the use of High Integrity Language Technology to address challenging issues in the engineering of highly complex critical software systems. HILT 2020 will focus on the growing importance of large-scale, highly parallel, distributed and/or cloud applications.
The 2020 event will be virtually co-hosted with SPLASH 2020.
At this year's ESEC/FSE event, AdaCore's Dr. Benjamin Brosgol will presenting his 2019 IEEE Software paper, "How to Succeed in the Software Business While Giving Away the Source Code: The AdaCore Experience."
The ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) is an internationally renowned forum for researchers, practitioners, and educators to present and discuss the most recent innovations, trends, experiences, and challenges in the field of software engineering.
SPARK is both a deductive verification tool for the Ada language and the subset of Ada on which it operates. In this paper, we present a recent extension of the SPARK language and toolset to support pointers. This extension is based on an ownership policy inspired by Rust to enforce non-aliasing through a move semantics of assignment. In particular, we consider pointer-based recursive data structures, and discuss how they are supported in SPARK. We explain how iteration over these structures can be handled using a restricted form of aliasing called local borrowing. To avoid introducing a memory model and to stay in the first-order logic background of SPARK, the relation between the iterator and the underlying structure is encoded as a predicate which is maintained throughout the program control flow. Special first-order contracts, called pledges, can be used to describe this relation. Finally, we give examples of programs that can be verified using this framework.
AdaCore will be sponsoring and exhibiting at this virtual event, which will highlight the continued rapid expansion of the RISC-V ecosystem, presenting both commercial offerings and exciting open-source developments.
Boeing, in partnership with the US Army, AdaCore, CoreAVI, Presagis and Real-Time Innovations (RTI), will demonstrate an integrated FACE Commercial-off-the-Shelf (COTS) solution stack covering cockpit displays, graphics systems and data transport connectivity. This stack enables high mission capability using the world’s latest and most advanced avionics technologies designed to accelerate RTCA DO-178C DAL A safety certification and FACE conformance.
Modernization efforts that require consolidating multiple proven software systems onto a single intelligent edge platform are difficult. Fortunately, there are strategies that allow you to maintain your software integrity and partitioning while taking advantage of cutting edge software development technology. In this webinar, subject matter experts from Wind River and AdaCore will demonstrate how you can map your existing architecture to guest operating systems on hypervisors, by using Wind River’s Helix Virtualization Platforms and software development tools from the compiler experts at AdaCore.
Libadalang is a powerful and modern technology supporting full syntactic analysis of Ada (or SPARK) source code and a comprehensive set of semantic queries
SPARK is a programming language and a set of verification tools designed to meet the needs of high-assurance software development. SPARK is based on Ada, both subsetting the language to remove features that defy verification and also extending the system of contracts by defining new Ada aspects to support modular, constructive, formal verification.
The SPARK Reference Manual is intended as a reference guide for users and implementors of the language. In this context, “implementors” includes those producing both compilers and verification tools.
This is the SPARK Reference Manual for the Community 2020 release of SPARK.
This course introduces you to the Ada language by comparing it to C. It assumes that you have good knowledge of the C language. It also assumes that the choice of learning Ada is guided by considerations linked to reliability, safety or security. In that sense, it teaches you Ada paradigms that should be applied in replacement of those usually applied in C.
This course also introduces you to the SPARK subset of the Ada programming language, which removes a few features of the language with undefined behavior, so that the code is fit for sound static analysis techniques.
This course was written by Quentin Ochem, Robert Tice, Gustavo A. Hoffmann, and Patrick Rogers and reviewed by Patrick Rogers, Filip Gajowniczek, and Tucker Taft.
The embedded world Exhibition & Conference will take place this year as a completely digital event. Both the trade fair and accompanying conferences, the embedded world Conference and the electronic displays Conference, will be held as virtual formats under the name embedded world DIGITAL.
When SEAKR Engineering decided to upgrade its mission-critical data recorder applications to a new hardware platform, they kept their software in Ada. To help them improve the efficiency and reliability of their Ada code, they upgraded their development environment to GNAT Pro.
V21 Product ReleaseProduct VideosAda 202x SupportGNAT Academic Program (GAP) UpdateSupport for Wind River HelixAdaCore in Space — LASP and the CLARREO PathfinderAdaCore and the FACE™ ApproachFifth Annual Make with Ada Programming CompetitionGNATcoverage Extends Source-Based Instrumentation for AdaAda for the Embedded C DeveloperHIS 2020 Virtual ConferenceNew AdaCore Blogs
AdaCore was a sponsor for this 14th annual Workshop on Spacecraft Flight Software. AdaCore Senior Software Engineer Tonu Naks gave a presentation on QGenV: Harnessing Qualified Code Generator for Model Verification.
AdaCore was a Bronze Supporter for the 52nd annual Technical Symposium on Computer Science Education, organized by the ACM Special Interest Group on Computer Science Education (SIGCSE). On Thursday, March 18 from 4:15 PM - 5:30 PM EDT, Dr. Patrick Rogers, a member of AdaCore’s senior technical staff, hosted a 60-minute virtual meeting on “Learning systems programming, hard real-time programming and formal methods with good language support.” AdaCore also showcased its GNAT AcademicProgram.
AdaCore is a Principal Member of The Open Group’s Future Airborne Capability EnvironmentTM (FACE) Consortium. We have been actively involved with the FACE effort since 2012, participating in and contributing to both the Technical and Business Working Groups.
Our objective in the FACE Consortium is to help FACE software suppliers meet assurance requirements for reliability, safety, and security while realizing the portability and reusability benefits that come from FACE conformance. Among the languages that are called out in the FACE Technical Standard – C, C++, Ada and Java – the one that best promotes high assurance coupled with code portability is Ada.
As a software tool provider to the Aerospace and Defense community, we offer products that enable and encourage FACE software suppliers to use Ada for their applications. More specifically, AdaCore’s FACE related products include:
GNAT Pro Ada development environments targeted to RTOSes supplied by FACE Consortium members, such as Wind River’s VxWorks 653 and Lynx Software Technologies’ LynxOS-178;
Efficient run-time libraries that are distributed with our cross-compilation environments and have been deployed in avionics systems certified at the highest Design Assurance Levels (DALs) of software standards such as DO-178B/C; and
Static analysis tools including the formal methods-based and CWE-compatible SPARK Pro toolsuite, the CWE-compatible CodePeer deep static analyzer for Ada, and the GNATcheck coding standard verifier for Ada.
This book summarizes AdaCore’s technologies and shows how they can help avionics suppliers develop and verify high-assurance FACE conformant software. The discussion is based on Edition 3.1 of the FACE Technical Standard and applies also to earlier versions.
This page gives access to theStartup-gen documentation. Startup-gen generates startup files (crt0 and linker script) based on properties of the target device such as: architecture, memory layout, number of interrupts.
Scale Up 360 OSS.5 Europe is the leading digital event on Functional, Operational, and System Safety for L5 Autonomous Driving. Quentin Ochem, AdaCore's Business Development Lead, will give a presentation on Self-Verified Software.
AdaCore's S. Tucker Taft will be a keynote at this year's 25th Ada‐Europe International Conference on Reliable Software Technologies (AEiC 2021). He and AdaCore co-authors will also be giving two talks on "Parallel Programming with Ada and OpenMP" and "Using Ada for model verification."
Space Tech Expo Europe is the continent's major dedicated supply-chain and engineering event for manufacturing, design, test and engineering services for spacecraft, subsystems and space-qualified components. The exhibition and conference draw attendance from thousands of industry leaders, decision makers, engineers, specifiers and buyers to meet manufacturers across the supply chain for commercial, government and military space.
The automation offered by modern program proof tools goes hand in hand with the capability to interact with the tool when the verification fails. The SPARK proof tool tries to help the user by providing the right information, so that the user can help the tool complete the proof. In this article, we present these mechanisms and how they work concretely on a simple running example.
FOSDEM is a free, two-day event organized for software developers to meet, share ideas and collaborate. The goal is to promote the widespread use of free and open source software. AdaCore engineers gave two talks this year. One on "Adding contracts to the GCC GNAT Ada standard libraries to strengthen analysis provided by formal verification tools," and one on "Proving heap-manipulating programs with SPARK."
The International Conference on Formal Engineering Methods (ICFEM) is an international leading conference series in formal methods and software engineering. Researchers and practitioners from industry, academia, and government, are encouraged to attend, present their research, and help advance state-of-the-art. AdaCore engineers presented a paper/talk on "Verification of Programs with Pointers in SPARK."
The High Confidence Software and Systems Conference is a forum for the development of scientific foundations and innovative and enabling software and hardware technologies for the assured engineering of complex computing systems. AdaCore's Yannick Moy gave a talk on "How to Improve the Robustness of Auto-active Program Proof Through Redundancy".
AdaCore's Yannick Moy will be presenting a paper/talk on "How the Analyzer can Help the User Help the Analyzer" at this 6th Workshop on Formal Integrated Development Environment, which is affiliated with NASA Formal Methods 2021.
AdaCore's Yannick Moy was invited by Xavier Leroy, Software Sciences Chair of the prestigious Collège de France, to give a talk on "Preuve auto-active de programmes en SPARK" (in French).
When it comes to providing software assurance, SPARK, a formally provable subset of Ada, is the best weapon in the arsenal to ensure the absence of data-flow and runtime errors. Furthermore, SPARK offers mechanisms to prove key integrity properties and even complete functional proof of requirements. Regardless of the apparent benefits of using SPARK in safety-critical applications, there is still some reservation in adopting the technology over traditional languages like C and C++, which offer minimum software assurance. Instead, developers in many cases rely on heavy testing approaches with the hope that all the possible bugs will be captured before application deployment. Arguments in favour of such problematic approaches include a perceived steep-learning curve for adopting SPARK, and thus, an increase in production cost, and the assumption that SPARK will significantly negatively impact the execution time of an application. These are all perceptions mainly formed due to a lack of understanding the technology. This paper takes a quantitative approach, where SPARK is put under test, and relevant metrics, such as performance and development time, are recorded to demystify the impact of adopting SPARK and expose any areas that the technology can be further improved. To achieve this a relevant to the industry embedded benchmark suite written in C, the EMBENCH, is converted to Ada and SPARK, to prove the absence of runtime errors, which are well-known sources of security vulnerabilities. Furthermore, we share our valuable experiences on best practices for hardening software libraries using SPARK.
Written by Kyriakos Georgiou, Paul Butcher and Yannick Moy
At the Aviation Forum Hamburg, more than 750 decision-makersand experts from the aviation industry will meet to shape the new age of the aviation industry. Under the motto “Aviation Reloaded” new strategies, technologies and partnerships will be discussed to meet the new demands on aviation. After facing the biggest crisis the aviation industry has ever experienced, the industry needs to reposition itself and rethink old structures to prepare thoughtfully for a fresh start.
We invite you to explore the Mi-V RISC-V® ecosystem during the first Mi-V Virtual Summit Conference. This event is a technology showcase that will bring together an esteemed group of innovators, academics, clients and collaborators.
The Mi-V Virtual Summit Conference will deliver valuable information about solutions, hardware, tools and Intellectual Property (IP) that are available for the PolarFire® SoC FPGA family. As the industry continues to shift towards digital-only events, the Mi-V Virtual Summit Conference will deliver engaging and high-quality content from our Mi-V ecosystem partners.
As a result of a 15-year partnership, AdaCore is organizing for the first time a private event solely dedicated to technical staff at the Airbus Group.
Ada and its subset SPARK, a language inspired by Pascal, embedding capabilities to describe specification, implementation and verification in one platform
Artificial Intelligence extended the limits considerably of what is technically feasible. In avionics, stakeholders are also pushing AI. However, research results are usually confronted with restrictions in avionics: Safety and certification are often assumed as showstoppers. This is not quite precise, since stakeholders are approaching each other. We collect the demand for AI applications in avionics and develop a classification scheme for these. For each identified AI class the status quo is compiled. We conclude with an assessment of AI readiness and the identification of necessary research effort for AI in avionics.
In this webcast, Shinya Yoneki from JTEKT introduces the use of Formal Verification Tool Suite, SPARK Pro for JTEKT's electric power steering system, along with concrete examples.
The size of the software used in automobiles is continuously increasing as autonomous driving technology is being introduced and there is a need to ensure higher safety and reliability. Therefore, it is important to achieve higher quality while adhering to the development schedule. Formal verification can be used as a development method to detect defects early in the software development process and reduce the man-hours required for testing and rework.
The conference will focus on cyber safety for embedded systems (ie. the confluence of safety and security), and how innovations in testing and the application of formal methods can help to achieve those objectives. Talks will address themes including the state of the art in software testing, using fuzz testing in a civil avionics security certification context (DO-326A), and applying innovative techniques such as formal methods to achieve cybersecurity.
This year, the conference will feature a keynote talk about the work of the National Cybersecurity Centre in the domain of embedded and critical systems.
The UK Space Conference is well established as the most important and influential event for space in the UK. For the sixth time, this biennial event will bring together the UK and international space community from across government, industry and academia to exchange ideas, share plans, develop relationships and seek inspiration to thrive in the new space age.
The Transmission Control Protocol (TCP) at the heart of TCP/IP protocol stacks is a critical part of our current digital infrastructure. In this article, we show how an existing professional-grade open source embedded TCP/IP library can benefit from a formally verified TCP reimplementation. Our approach is to apply formal verification to the TCP layer only, relying on validated models of the lower layers on which it depends. We translated the TCP user functions into SPARK and modeled asynchronous events with ghost code. This enabled the detection of two bugs in the original C implementation related to memory management and concurrency. The translated code has been proven to be free of run-time errors and to respect the transitions of the TCP state machine, specified in RFC 793. For the lower layers, we used symbolic execution with KLEE to formally verify the contracts used in SPARK to model the corresponding behavior. This work is a step towards a more secure implementation for TCP.
This paper is copyrighted by IEEE, and reproduced here with their permission.
AdaCore will be exhibiting in Aerospace Techweek 2021 and Eric Perlade will present "Making FACE™ Units of Conformance Fully Portable: Coding Guidelines for Ada” on November 3rd.
This report offers further guidelines and considerations to the security refutation objectives described within the following two technically identical documents:
ED-203A “Airworthiness Security Methods and Considerations”, European Organisation for Civil Aviation Equipment (EUROCAE)
DO-356A “Airworthiness Security Methods and Considerations”, Radio Technical Commission for Aeronautics (RTCA)
Refutation is described within ED-203A / DO-356A as follows:
“Refutation acts as an independent set of assurance activities beyond analysis and requirements. As an alternative to exhaustive testing, refutation can be used to provide evidence that an unwanted behavior has been precluded to an acceptable level of confidence. NOTE: Refutation is also known as Security Evaluation in some contexts.” [ taken from ED-203A / DO-356A].
The main part of the report summarizes how refutation activities fit into the associated Airworthiness Security Process. In addition, a series of guidelines and considerations for including a Refutation Test Plan within a Plan for Security Aspects of Certification (PSecAC) is presented. Annexes are then provided to cover additional guidelines for specific refutation activities. This version of the report includes Annex A, which covers “Fuzz Testing”.
SPARK is a software development technology (programming language and verification toolset) specifically designed for engineering ultra-low-defect-level applications, for example where safety and/or security are key requirements. SPARK Pro is the commercial-grade offering of the SPARK technology developed by AdaCore, Altran and Inria.
SPARK has an extensive industrial track record. Since its inception in the late 1980s it has been used worldwide in a range of industrial applications such as civil and military avionics, air traffic management/control, railway signaling, cryptographic software, cross-domain solutions, medical devices and automotive.
The SPARK language is a large subset of Ada 2012. SPARK includes as much of Ada as is possible/practical to analyze formally, while eliminating sources of undefined and implementation- dependent behavior. SPARK includes Ada’s program-structure support (packages, generics, child libraries), most data types, safe pointers, contract-based programming (subprogram pre- and postconditions, scalar ranges, type/subtype predicates), Object-Oriented Programming, and the Ravenscar subset of tasking features.
Software is a critical element in almost any military application and can be a differentiator that provides strategic and tactical advantages on the battlefield. However, it also has to meet set challenges – it has to be long-lived, reliable, and easily maintainable to match the longevity of the military platform on which it is deployed. That means it has to account for both innovation and longevity from the start, and be able to work consistently and effectively over decades without the risk of failure.
Yet, in long-lived military projects, software is often being rewritten from scratch, pushing up costs and delaying overall completion. For example, the U.S. Government Accountability Office (GAO) highlighted software delays as a key factor in the F-35 fighter jet modernization program failing to meet deadlines to move to full-rate production. This is no outlier – 10 of the Department of Defense’s (DoD’s) 15 major IT projects are behind schedule.
It’s therefore time for a new approach – one that applies lessons learned from previous military software development and focuses on military grade, open source, standards-based solutions that reuse and rejuvenate existing assets. This method will deliver the innovative software capabilities that military projects require – on time and on budget.
At AdaCore we pledge to timely analyze vulnerabilities in our products and disclose them in a way that balances the interests of our customers & community.
Source code portability of airborne software is the keystone of the Future Airborne Capability Environment (FACETM) approach and is realized through well-defined application program interfaces (APIs) and widely used industry standards such as IDL, POSIX, and ARINC-653. However, full portability of a Unit of Conformance (UoC) requires more than usage of common APIs and standards. It entails adhering to programming language-specific restrictions to ensure that the UoC has an equivalent effect when ported to a new platform. This paper, geared to UoC developers and project managers, offers guidance for Ada and its formally analyzable SPARK subset. It shows how to deal with vendor-specific or optional language features, how to avoid implementation dependencies, and how to manage target platform dependencies. By adopting the recommended stylistic conventions (most of which can be enforced by static analysis tools) developers of airborne software can use Ada or SPARK to achieve full portability for their FACE UoCs while also realizing the assurance benefits (extensive static checks that catch errors early) that these languages provide.
Software development presents daunting challenges when the resulting system needs to operate reliably, safely, and securely while meeting hard real-time deadlines on a memory-limited target platform. Correct program execution can literally be a matter of life and death, but such is the reality facing developers of space software systems.
This book explains how the Ada and SPARK programming languages, together with AdaCore’s products, can reduce system life cycle costs and facilitate conformance with applicable software certification / qualification standards.
In an increasingly digital age, safety-critical software is becoming an ever more vital component of military and aerospace projects. Given its importance, any issues with writing and certifying this software can negatively impact overall project success, increasing risk and causing potential delays.
As the role of safety-critical software grows, so does its complexity and the time required to create and test code. That’s why many projects now use a model-based design approach to programming. Essentially, this allows teams to create digital models of the software to be built, which can be run, checked, and refined through simulations – all before any code is written.
One of the key benefits here is that modeling languages allow domain experts, rather than software engineers, to write software specifications. As domain specialists understand more deeply what they want the safety-critical system to achieve, this ensures a closer fit to real-world requirements.
However, while this helps with the early stages of a project, often these models are then handed over to programmers to manually create code that matches the behavior of the original model. This adds time to the process and introduces the potential for programming errors that then need to be spotted and fixed later in the project, leading to potential delays.
We have investigated the Java log4j logging facility documented as CVE-2021-4428 and also known as log4shell. We can confirm that AdaCore is not affected.
Formal verification of floating-point computations remains
a challenge for the software engineer. Automated, specialized tools can
handle floating-point computations well, but struggle with other types
of data or memory reasoning. In this article, we show how generic deductive verification tools based
on general-purpose SMT solvers can be used to verify different kinds of
properties on floating point computations up to bounds on rounding er-
rors. The demonstration is done on a computation of a weighted average
using floating-point numbers, using an approach which is heavily based
on auto-active verification. We use the general-purpose tool SPARK for
formal verification of Ada programs based on the SMT solvers Alt-Ergo,
CVC4, and Z3 but it can in principle be carried out in other similar
languages and tools such as Frama-C or KeY.
AdaCore is a regular sponsor of this annual workshop on spacecraft flight software. This year, we also gave a technical presentation "System-to-Software Integrity: from SysML to Simulink to Code” and a sponsor presentation on "Dynamic Memory Management with Ownership in Rust and SPARK"
AdaCore was an exhibitor at this year's SIGCSE Technical Symposium on Computer Science Education promoting our GNAT Academic Program (www.adacore.com/academia) to a global audience of educators and researchers.
AdaCore attended this year's Tri-Service Open Architecture Interoperability Demonstration - a single-day Technical Interchange Meeting and Expo focusing on Modular Open Systems Approach (MOSA) principles and innovations.
AdaCore will be attending the AAAA - Army Aviation Mission Solutions Summit, an annual event where the entire Army aviation community gathers to focus solely on Army aviation issues.
AdaCore will be exhibiting at this one-day event hosted by the U.S. Air Force. Technology Interchange Meetings (TIM) allow DoD, Industry, and Academia to collaborate on Research and Engineering technology challenges.
AdaCore will be exhibiting at Aerospace Tech Week's inaugural event in the Americas. Thisconference and exhibition will offer an exclusive focus on the Americas developments for the commercial, defense, and bizjet aerospace tech sectors.
AdaCore is a sponsor and will be actively participating in this year's HILT Workshop. Held every two years and sponsored by SIGAda, the workshop focuses on the use of High Integrity Language Technology to address challenging issues in the engineering of highly complex critical software systems. This year's event will be held in Ann Arbor, Michigan, in conjunction with the 2022 Automated Software Engineering conference (ASE'22).
This workshop is exclusively for GNAT Academic Program (GAP). Members will share information regarding successful teaching methods and research projects, even student projects. AdaCore engineers will also provide updates on Ada, SPARK, related resources, and our community efforts.
CYBERUK is the UK Government’s flagship cyber security event which AdaCore will be attending to demonstrate expertise in military-grade cyber-secure system design at exhibition booth A68.
Join AdaCore at the 11th edition of ERTS, which will take place at Diagora Congress in Toulouse.
AdaCore will be exhibiting and presenting “Dynamic Memory Management in Critical Embedded Software”, hosted by Claire Dross, Cyrille Comar, Yannick Moy and Florian Giltcher from Ferrous Systems.
As part of the Tempest future combat air system program, BAE Systems will be using the VxWorks 653 platform, a part of Wind River Studio, and associated DO-178C DAL B safety certification evidence packages, and AdaCore's GNAT Pro Assurance as part of ongoing technology demonstration project work.
The 26th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2022) will take place in Ghent, Belgium in dual mode, with a solid core of in-presence activities accompanied by digital support for remote participation. The conference schedule comprises a journal track, an industrial track, a work-in-progress track, a vendor exhibition, parallel tutorials, and satellite workshops.
Memory management has always been a delicate issue in critical embedded software because memory is often a scarce resource and many of the typical software errors jeopardizing the integrity of the execution of the software are related to memory mismanagement. Furthermore, critical software has had a tendency to grow in size and complexity in recent years, because it is using more and more complex algorithms in the critical parts of a system. The push towards autonomous mobility is a good example of the drivers for complexity reaching the most critical parts of software controlling such systems. This added complexity requires added flexibility in memory management that is not compatible with the traditional memory management techniques used for critical embedded software. In this paper we will first go over the traditional memory management limitations and the reasons behind them, we will then explore possibilities for going beyond them while being able to provide a high level of guarantees of correctness with regard to memory usage.
Since Ada targets safety-critical programs, many features of the language introduce safety nets in the form of language-mandated checks. Even if compile-time verification is preferred to runtime verification whenever possible, many of these checks are still done dynamically, an exception being raised in case of violation.
The addition of contracts in Ada 2012 follows a similar trend, as a violation causes an exception to be raised when the code is compiled with assertions enabled. The SPARK tool aims at statically verifying that language-mandated checks and the user-written contracts can never fail at runtime.
In this article, we give insights on how the tool works in practice and what are the most important challenges as of today.
When Masten Space Systems was awarded a NASA contract to land scientific payloads on the Moon, the company chose to work with AdaCore’s mission-critical flight control software development and verification tools for its XL-1 Lunar Lander spacecraft. Masten Space Systems will use AdaCore’s the Ada and SPARK programming languages and AdaCore’s GNAT Pro integrated development environment and SPARK Pro static analysis verification tools in the exciting exploration project.
To learn how AdaCore can help build your space systems, please contact info@adacore.com.
When IPESOFT was looking to develop its core real-time D2000 industrial automation platform, it knew that choosing the right development language and software tools would be crucial to the success of the platform and the company’s overall business growth. The solution needed to be reliable, secure, high performance, and easy and efficient to maintain over the long-term. Ultimately, IPESOFT chose AdaCore’s GNAT Pro and the Ada language to develop its D2000 platform. As a result, the company has successfully completed D2000 implementations in over 2,000 successful projects and has expanded into six countries.
Semiconductor manufacturing has some of the most exacting needs when it comes to performance and reliability, requiring millisecond-level precision and the ability to cost-effectively produce billions of smaller and smaller devices every year. That’s why ITEC, one of the major semiconductor manufacturing equipment and automation providers, chose Ada as its programming language to develop its critical control software.
Semiconductor manufacturing has some of the most exacting needs when it comes to performance and reliability, requiring millisecond-level precision and the ability to cost-effectively produce billions of smaller and smaller devices every year. That’s why ITEC, one of the major semiconductor manufacturing equipment and automation providers, chose Ada as its programming language to develop its critical control software.
How Ada is helping the Laboratory for Atmospheric and Space Physics minimize risk, reduce cost, and assure reliable control of software used for spacecraft and instrument operations.
How Ada is helping the Laboratory for Atmospheric and Space Physics minimize risk, reduce cost, and assure reliable control of software used for spacecraft and instrument operations.
This is the user documentation for GNAT DAS (Dynamic Analysis Suite), a package comprising GNATcoverage, a DO178-capable structural coverage analysis toolset; GNATtest, a unit test harness generator; and GNATfuzz, a tool for automating dynamic testing on Ada code, performing test case generation and discovery of software vulnerabilities through fuzzing.
The challenges faced by companies like your own in confronting increasingly hostile cybersecurity environments and how NVIDIA is tackling this to overcome a scarcity in expert software security resources
Learn why NVIDIA made the “heretical” decision to abandon C/C++ and adopt SPARK as its coding language of choice for security-critical software and firmware components and the impact this had
The advantages of using the SPARK for security- and safety-critical coding applications
How NVIDIA's tried and tested approach to ramping up their use of SPARK for critical component development can help your business
The benefits NVIDIA has gained through their adoption of SPARK
Why many of NVIDIA’s early SPARK skeptics have now become SPARK evangelists
NVIDIA’s recommendations for would-be SPARK adopters
See first-hand how you can adopt SPARK to establish and demonstrate assurance against cyberattacks and critical system failures
As one of the world's most trusted names in high-performance computing, security is essential to NVIDIA’s brand. With cybersecurity risks rising across the board, the company took an ambitious path to examine its software development methodology and find a more measurable solution. Ultimately, it chose to abandon C/C++ and adopt SPARK as its coding language of choice for verifying its most security-critical software and firmware components.
AdaCore is exhibiting at Embedded World 2023 from March 14th to 16th in Nuremberg, Germany in partnership with Ferrous Systems. Visit us in Hall 4 at Booth 4-148 to discuss your high integrity software needs.
AdaCore will be exhibiting at SIGCSE, one of the largest academic shows dedicated to teaching resources related to software and hardware. Visit us at Booth 417 to learn about AdaCore's GNAT Academic Program and the benefits of using Ada and SPARK within an academic setting.
AdaCore is a sponsor/exhibitor of this annual workshop on spacecraft flight software. We are also sponsoring a presentation by LASP at the University of Colorado on Adamant - A New Mission-Critical Flight Software Framework Written in Ada. Stop by our on-site kiosk to learn about AdaCore's long history of providing tools and expertise to the space industry.
AdaCore, a trusted provider of software development and verification tools, today announced the launch of its new RecordFlux technology, designed to ease the development and security of binary communication protocols. The technology comprises a Domain Specific Language (DSL) to precisely describe complex binary data formats and communication protocols, and a toolset to verify specifications and generate provable SPARK code that can be executed on a target CPU.
One of the basic requirements for enterprise platform security is device attestation: trustworthy evidence of a device’s identity and security properties. The industry standard Security Protocol and Data Model (SPDM) addresses this need, defining message formats and session behaviors that device suppliers can implement for attestation.
This paper explains how AdaCore partnered with NVIDIA to capture and implement a subset of the SPDM 1.1.0 specification, using AdaCore’s RecordFlux product in conjunction with the SPARK/Ada programming language and the SPARK Pro toolsuite. The project successfully demonstrated that these technologies can address the vulnerabilities that communication protocols and complex data formats can bring, and the SPDM library that the project produced will be integrated into the firmware of microcontrollers and microprocessors that NVIDIA designs
The User Request Evaluation Tool developed by a team that included Lockheed Martin and AdaCore is conflict-detection technology that is said to save time, fuel, and money while also helping to ensure safe aircraft separation.
BAE Systems are using the GNAT Pro development environment for host Ada compilation in the development of software for the Eurofighter’s mission computers.
MacDonald Dettwiler (MDA) chose open-source GNAT Ada 95 from Ada Core Technologies to develop control software for the Mobile Servicing System (MSS), an essential com- ponent of the International Space Station (ISS).
AdaCore is a sponsor of this year's HCSS event and will be presenting a paper on Bridging the Gap Between Protocol Specification and Program Verification. HCSS focuses on new scientific and technological foundations for the assured engineering of complex computing systems.
AdaCore is a sponsor of this year's Showcase for Commerce event - a nationally renowned business and industry trade show and defense contracting exhibition.
Exclusively for GNAT Academic Program (GAP) members, our annual GAP Workshop provides a forum for members to share information regarding successful teaching methods and research projects, even student projects. AdaCore engineers also provide updates on Ada, SPARK, related resources, and community efforts.
AdaCore will be exhibiting at this two-day event hosted by the U.S. Army. Technology Interchange Meetings (TIMs) allow DoD, industry, and academia to collaborate on research and engineering technology challenges. This year's event will be held in conjunction with the MOSA Industry and Government Expo and Summit.
AdaCore, a trusted provider of software development and verification tools, today announced it has committed books, resources, and training in support of BAE Systems’ engineering apprenticeship programme, demonstrating its role as a dedicated partner and its commitment to the advancement of high integrity software.
AdaCore is co-organizing, sponsoring, and exhibiting at this year's High Integrity Software Conference.
The mission of HISC is to share challenges, best practice and experience between software engineering practitioners. The conference features talks from industrial and academic specialists which disseminate experience and knowledge of important techniques and methods that are applicable across industry sectors.
The Ada Europe conference schedule comprises a journal track, an industrial track, a work-in-progress track, a vendor exhibition, parallel tutorials, and satellite workshops.
AdaCore is sponsoring this event and will be giving two talks:
Patrick Rogers will present "An Update On the Tasking Profiles in Ada 2022"
Paul Butcher will present " ‘Security Hardening Ada Programs through Innovative Fuzz Testing"
AdaCore is sponsoring this years Ada Deutschland Workshop, the workshop will look at making processes and systems safe in artificial intelligence and machine learning. The opportunities and challenges of AI processes in real use will be discussed from the point of view of industrial practice and the user, as well as from the point of view of science and research.
Space applications are either safety critical or mission critical, and most have hard real-time constraints. Guiding a launcher or delivering positioning data requires precision and high reliability. This makes Ada not only suitable for space applications but a very good fit. See our interview with Technical Account Manager, Eric Perlade, on AdaCore and the Space Sector.
Electronic election systems need to be demonstrably secure in order to ensure the protection of votes, the privacy of voters, and the prevention of interference. That’s why Software Improvements selected the Ada 2012 programming language and AdaCore’s GNAT Pro Ada development environment to upgrade the Australia Capital Territory’s Electronic Voting & Counting System (eVACS®), a public-facing system that demands a high level of security.
Building a compiler for a programming language is a notoriously hard task, especially when starting from scratch. That’s why we developed Langkit, a meta-compiler which allows language designers to focus on the high-level aspects of their language. In particular, the specification of type systems is done in a declarative manner by writing equations in a high-level logic DSL. Those equations are then resolved by a custom solver embedded in the generated compiler front-end whenever a code fragment of the target language needs to be analyzed. This framework is successfully used at AdaCore to implement name and type resolution of Ada, powering navigation in IDEs and enabling development of deep static analysis tools. We discuss the implementation of our solver, and how a recent switch to using a DPLL(T) solver backend with a custom theory allowed us both to address long-standing combinatorial explosion problems we had with our previous approach, but also to gain new insights in how to emit human-readable diagnostics for type errors.
AdaCore will be sponsoring the GNU Tools Cauldron this year.
The purpose of this workshop is to gather all GNU tools developers, discuss current/future work, coordinate efforts, exchange reports on ongoing efforts, discuss development plans for the next 12 months, developer tutorials and any other related discussions.
The Digital Security by Design (DSbD) programme from UK Research and Innovation (UKRI) is transforming digital technology and creating a more resilient, and secure foundation for a safer future. Across the current DSbD ecosystem, industry and academia are discovering the benefits of porting and refactoring their code to the Morello prototype platform. AdaCore are involved in the initiative via the GE Aerospace primed Edge Avionics project
This is the main documentation for GNAT SAS, a static error detection tool that automatically identifies possible programming errors and verifies logical correctness, without relying on labor-intensive run time testing.
This document provides a guide through the major capabilities of GNAT SAS inside GNAT Studio by working on a code example: sdc, a simple desktop calculator.
Discover Enhanced Software Security with SPARK Pro! Dive into our exclusive webinar featuring Yannick Moy, and learn about the cutting-edge features of SPARK Pro with live demonstrations on pointer ownership, function contracts, and secure type casting.
In the competitive New Space industry, ingenuity, reliability, and cost-effectiveness are paramount factors. When Latitude embarked on creating their cutting-edge small satellite launcher, Zephyr, they recognized the importance of selecting the right programming language and development tools to support their efforts. After evaluating a number of candidates, Latitude settled on Ada and its formally verifiable SPARK subset. Ada and SPARK were judged to have the best support for sound software engineering practice, thus reducing life cycle costs, while meeting real-time embedded systems performance and predictability requirements. Based on their successful experience, Latitude plans to expand its use of Ada and SPARK on future projects and sees these technologies as key enablers.
Documentation for the GNAT Metrics tool, which can be used to compute various program metrics. It takes an Ada source file as input and generates a file containing the desired metrics data as output.
AdaCore is attending Embedded World 2023 from April 9th to 11th in Nuremberg, Germany. The embedded world Exhibition & Conference provides a global platform and a place to meet for the entire embedded community. It offers unprecedented insight into the world of embedded systems, from components and modules to operating systems, hardware and software design, M2M communication, services, and various issues related to complex system design.
Join AdaCore at the Army Aviation Mission Solutions Summit, an annual event where the entire Army aviation community gathers to focus solely on Army aviation issues.
AdaCore will be exhibiting and presenting at the 12th edition of the Embedded Real-Time Systems European Congress (ERTS), which will take place at Diagora Congress in Toulouse.
AdaCore will exhibit at this year's SIGCSE Technical Symposium on Computer Science Education promoting our GNAT Academic Program (www.adacore.com/academia) to a global audience of educators and researchers.
In the context of the evolving telecommunications industry, characterized by the emergence of 5G and a surge of connected devices in IoT, LatenceTech, founded in Montreal, Canada, by former Ericsson senior executive Benoit Gendron, identified a specific need for specialized network tools focusing on precise latency measurement. “This precision is essential for the functionality of applications such as autonomous vehicles and connected robotics. Current technologies, including Ping, ICMP, and even advanced protocols like TWAMP (co-developed by Cisco), still do not meet this requirement entirely.” To address this, Gendron’s team deployed monitoring agents into client networks, explicitly focusing on measuring and managing network latency. This approach extends traditional methods to a strategy that balances data analysis and performance optimization. The objective is to redefine performance metrics by emphasizing the quality of network experience rather than relying solely on conventional, quantitative data metrics.
We’re excited to announce that the Communications of the ACM has published a paper on SPARK: “Co-Developing Programs and Their Proof of Correctness”. The paper provides a comprehensive and up-to-date presentation of SPARK, including: an overview of the programming language and its design goals; an explanation of what it means to co-develop a program and its proof of correctness; and approaches to practical, incremental adoption that allow at-scale application to industrial, high-integrity systems.
Battery Ventures, a global, technology-focused investment firm, today announced a significant investment in AdaCore, a leader in providing software development tools for safety- and security-critical systems. This strategic partnership will catalyze AdaCore's expansion, positioning the company as the go-to source for high-integrity, software-development tooling.
The Ada Developers Workshop is co-located with the 28th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2024). The Workshop aims to create an informal yet dynamic platform for developers in the Ada community to meet, share insights, and present their latest projects or project updates, using the Ada programming language and Ada-related technology such as SPARK. Topics will range from community advocacy all the way to technical presentations.
AdaCore is co-organizing, sponsoring and exhibiting at this year’s High Integrity Software Conference.
The mission of HISC is to share challenges, best practice and experience between software engineering practitioners. The conference features talks from industrial and academic specialists which disseminate experience and knowledge of important techniques and methods that are applicable across industry sectors.
GNAT Pro for CHERI enhances memory safety in modern systems and eradicates many memory-related vulnerabilities. It also provides a complete Ada toolchain to build secure applications executing on Arm Morello, a Capability Hardware Enhanced RISC Instructions (CHERI) CPU. Enhancements to the GNAT Pro GCC and LLVM bare-metal Ada runtimes bring automated CHERI pure-capability memory allocators and other novel security features to the developer, permitting new security-by-design paradigms to systems development.
AdaCore, a leader in high-assurance, safe, and secure software toolchains, is set to stand out at CYBERUK by showcasing its unique approach to Secure Avionics by Design (SAbD).
AdaCore will be attending the Farnborough International Airshow 2024, which will host leading innovators from the aerospace, aviation and defence industries and beyond.
In an age of increasing security breaches and cyberattacks, the need for robust and comprehensive security mechanisms within embedded real-time systems is paramount.
AdaCore is thrilled to be part of the Safety-Critical Rust Consortium alongside The Rust Foundation, Arm, Ferrous Systems, OxidOS, HighTec EDV-Systeme GmbH, TrustInSoft, Veecle, and Woven by Toyota. The primary objective of this group will be to support the responsible use of the Rust programming language in safety-critical software — systems whose failure can impact human life or cause severe environmental or property harm.
This year, the High Integrity Software Conference (HISC) will move to a new, larger venue, the International Convention Centre (ICC) Wales.
The mission of HISC is to share challenges, best practices, and experience between software engineering practitioners. The conference features talks from industrial and academic specialists who disseminate their experience and knowledge of essential techniques and methods applicable across industry sectors.
For 30 years, AdaCore has provided the essential tools for building reliable, safe, and secure software. Throughout these decades, the Ada programming language and freely licensed open-source software have been integral to AdaCore's mission.
AdaCore is excited to announce its participation in the SCHEME research project. Rolls-Royce has assembled a world-class consortium of UK industry and academia to deliver the next generation of high-integrity processing platforms for use in aerospace and other harsh environments.
This guide describes how to install GNAT Pro for Rust, as well as how to build, run, and debug native, cross-compiled, and mixed-language applications.
The Copilot for Ada programming language project aimed to research and develop a proof-of-concept code completion tool and evaluate its performance on the Ada code generation task. Its idea is to boost Ada software developers’ productivity by providing intelligent code completions and suggestions, improving the pace of task automation, and saving significant amounts of time on repetitive and boilerplate code.
Rapita Systems will demonstrate the integration of their RapiCover Zero and RapiTime Zero tools with AdaCore’s GNAT Pro for Rust next week at the High Integrity Software Conference (HISC). The integration will show how structural coverage and execution time metrics, including worst-case execution time, can be collected during on-target tests of safety-critical code written in Rust.
Explore the advantages of Ada, SPARK, and Rust over C/C++ for high-integrity software. This paper highlights the safety, security, and efficiency of each language, covering ecosystems, community support, and adoption costs. Discover the best fit for your projects to reduce errors and boost software integrity. Download now for strategic insights.
Do you need to meet ISO 26262 qualification requirements? AdaCore’s development tools provide solutions for guaranteeing the safety of automotive software.
AdaCore will be exhibiting at Embedded World Europe in Nuremberg, Germany on 11 - 13 March 2025. Meet us at Booth 4-148 to discover demonstrations and talk to our experts about high-integrity technologies including Ada, SPARK, C/C++, Rust and more.
Explore how Ada, SPARK, and Rust address critical memory safety challenges in our latest whitepaper. Memory safety issues account for over 70% of security vulnerabilities in major tech systems, making robust solutions essential. This paper discusses common bugs like out-of-bounds writes and null pointer dereferences, and demonstrates how the unique features of these programming languages significantly reduce risks and enhance system reliability. Discover how adopting these memory-safe languages can fortify your software against pervasive security threats, enabling you to develop complex systems with greater confidence and security. Download now to learn more.
In an age where security breaches and cyberattacks have become increasingly prevalent,
the need for robust and comprehensive security mechanisms within embedded real-
time systems is paramount. In this paper, we propose a novel solution to enforce fault-detection
and increase security assurance: “Security by Default”, specifically combining Capability
Hardware Enhanced RISC Instructions (CHERI) ISA microprocessor extensions with a CHERI
pure-capability compliant Ada runtime. We present case studies showing how combining
memory-safe hardware with memory-safe software results in a mutualistic layered
approach to security and increases assurance of embedded real-time systems. We argue
that this satisfies regulatory security verification objectives outlined in standards like the
“Airworthiness Security Process Specification” (DO-326A/ED-202A[1] [2]).
The Rust Foundation is an independent non-profit organization dedicated to stewarding the Rust programming language, nurturing the Rust ecosystem, and supporting the set of maintainers governing and developing the project.
AdaCore, a leader in high-integrity software development tools, is excited to announce its participation in Embedded World 2025, which will take place from March 11th to 13th in Nuremberg, Germany. This year, AdaCore will showcase its cutting-edge solutions for safety and security-critical embedded systems, with a special focus on SPARK and Rust technologies.
Meet AdaCore at Booth 3015 at the Army Aviation Mission Solutions Summit, an annual event where the entire Army aviation community gathers to focus solely on Army aviation issues. Speak to your Account Manager to set up a meeting with our team.
AdaCore are co-sponsors, co-organizers and exhibitors at the High Integrity Software Conference.
HISC features high-quality content from experts in industry and academia who disseminate their knowledge of important and innovative techniques and methods that software engineers can apply in practice across industry sectors.
HISC will return on 13 November 2025. Registration opens on 31 March.
AdaCore is well-known for its support of high-integrity embedded development. When a new language, Rust, emerged and started making claims about memory safety and minimal footprint, it was only a matter of time before it found its way into the AdaCore family.
Pointer errors have plagued software developers for decades. Rust’s innovative and expressive approach helps make pointers safe and efficient. Pointers have been a staple of programming languages since the earliest days of computing, serving two purposes:
• Indirection: a means to share (rather than copy) data values within a program. This can be implicit, for example by passing a variable as a “by reference” parameter, or explicit through syntax for reference creating / dereferencing (such as “&x” and “*p” in C).
• Dynamic allocation: a means to construct and manipulate data structures (linked lists, trees, graphs, …) that can grow and shrink during program execution. However, with power comes danger, and pointers can compromise both safety and performance. This paper investigates the challenges that pointers bring and explains how Rust meets these challenges.
Rust’s approach requires programmers to think about pointers in a new way, but the effect is memory safety / early detection of pointer errors and efficient performance, with the expressiveness of a general-purpose data structuring facility.
The user guide for Ada & SPARK extension for Visual Studio Code. This extension provides support for the Ada and SPARK programming languages in VS Code.
AdaCore is sponsoring the 29th edition of the Ada-Europe International Conference on Reliable Software Technologies (AEiC 2025), held in Paris. On Thursday 12th June at 14:00, AdaCore’s Claire Dross, Joffrey Huguet and Johannes Kanig will give a presentation on "Reasoning about Subprogram Termination in SPARK" at AEiC 2025. Get in touch at info@adacore.com to meet our team at the conference.
Discover how to Prove Security and Safety for Embedded and Systems Software. Learn about what SPARK is, how SPARK works, and see how SPARK can be applied to a M.A.R.S. Rover to prove safety during this webinar hosted by AdaCore’s Head of Product and Innovation, Tony Aiello.
AdaCore will exhibit from Booth 417 at the American Society for Engineering Education (ASEE) conference in Montreal, Canada. We will showcase this year’s Capstone projects from AdaCore’s GNAT Academic Program (also known as GAP). Get in touch at info@adacore.com to meet our team at the conference or express interest in joining GAP.
Join high-integrity software engineers from across North America for AdaCore Tech Day in Denver. Attend technical briefings, watch live demos and engage in conversations with other software engineers. Get answers to all your questions about today's software development landscape from our experts and learn where the future of critical software is headed.
Join high-integrity software engineers from across Europe for AdaCore Tech Day in Munich. Attend technical briefings, watch live demos and engage in conversations with other software engineers. Get answers to all your questions about today's software development landscape from our experts and learn where the future of critical software is headed.
High-integrity software tooling experts, AdaCore, are delighted to announce the introduction of the Ada and SPARK programming languages into the automotive market. Together with their partner NVIDIA, they are set to publish an off-the-shelf reference process, allowing others to follow their lead.
