News Article | May 8, 2017
ANNAPOLIS, Md.--(BUSINESS WIRE)--AdaCore today announced the publication of a free booklet, Implementation Guidance for the Adoption of SPARK, which explains how best to introduce and make use of the SPARK/Ada formal verification technology based on a project’s assurance goals. Co-authored by AdaCore and Thales, a global technology leader in critical domains, the booklet describes the various levels of software assurance at which the SPARK language and toolset can be used. It explains the associated benefits and costs at each level, and details the processes that Thales is using to introduce formal verification in operational projects. The booklet will be a valuable resource for project leaders, technology experts, and software developers responsible for producing high-assurance software for critical systems. After briefly introducing the Ada language and its SPARK subset, the booklet describes four levels of software assurance: A fifth level, Platinum, entails a full functional proof that the software meets its formally specified requirements. This level is outside the scope of the booklet. “From our years of providing SPARK solutions to critical industries, we know that it can take time and effort to introduce disruptive technologies into an established workflow, even when the benefits are clear,” said Yannick Moy, SPARK Product Manager at AdaCore. “That’s why I’m pleased that we had the opportunity to work with Thales on this booklet. Now any organization developing and verifying high-assurance software will find practical guidance on how to adopt and best exploit SPARK technology.” “Introducing formal verification in a project requires an informed scoping of the targeted software functions, as well as a clear definition of the verification objectives,” said Véronique Normand, Research & Technology Manager at Thales. “This booklet is intended to help teams characterize their verification objectives, and to provide practical implementation guidance in applying SPARK. Developed together with several Thales software architects, it is now used to support further SPARK initiatives in the Thales Group.” Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. Four flagship products highlight the company’s offerings: Over the years, customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as railway systems, space systems, commercial avionics, military systems, air traffic management/control, medical devices and financial services. AdaCore has an extensive and growing worldwide customer base; see www.adacore.com/customers/ for further information. AdaCore products are open source and come with expert online support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com Thales is a global technology leader for the Aerospace, Transport, Defense and Security markets. With 64,000 employees in 56 countries, Thales reported sales of €14.9 billion ($16 billion) in 2016. With over 25,000 engineers and researchers, Thales has a unique capability to design and deploy equipment, systems and services to meet the most complex security requirements. Its exceptional international footprint allows it to work closely with its customers all over the world. The booklet is available for free, both on-line and as a paper copy; please visit http://www.adacore.com/knowledge/technical-papers/implementation-guidance-spark/ or contact firstname.lastname@example.org.
News Article | May 15, 2017
NEW YORK & PARIS--(BUSINESS WIRE)--AdaCore today announced the launch of its 2nd annual “Make with Ada” programming competition, a contest that aims to help the embedded software community improve the quality of their code by encouraging the use of the Ada and SPARK programming languages. The competition runs from May 15 to September 15, 2017, and offers over €8000 in total prizes. Participants can register for the competition at www.makewithada.org. The competition is open to individuals and to teams with up to four members. The goal is to design and implement an embedded software project where Ada and/or SPARK are the principal language technologies. Entrants will need to demonstrate that their system meets its requirements and has been developed using sound software engineering practices. The submission deadline is September 15, 2017, and the award winners will be announced in October 2017. Cash prizes will be awarded to the projects that best meet the overall criteria of software dependability, openness, collaborativeness and inventiveness. A Student-only Prize will also be awarded to the best-ranking Student Finalist: one Printrbot Portable 3D Printer. Entrants must provide a student ID when registering to qualify for this prize, as defined in the competition terms and conditions at http://makewithada.org/terms. A project submitted by a student is eligible for both the Student-Only Prize and the cash prizes. The panel of judges comprises embedded systems experts Jack Ganssle, Principal Consultant at The Ganssle Group; William Wong, Technical Editor at Penton Media; Richard Nass, Embedded and IoT Franchises Brand Director at OpenSystemsMedia; Cyrille Comar, AdaCore President; and Stephane Carrez, Software Engineer at Bouygues Telecom and Make with Ada 2016 competition winner. “Judging last year’s Make with Ada competition showed me how developers new to Ada and SPARK could quickly come up to speed with these languages and produce some ingenious embedded applications,” said competition judge William Wong. “I look forward to seeing the range of projects that are submitted this year; I’m sure that the combination of software engineering talent, safe / secure languages and top-notch development tools will produce some impressive results.” “This is an exciting opportunity for developers to try the Ada or SPARK technologies and demonstrate their imagination and programming skills,” said Fabien Chouteau, AdaCore software engineer and author of the Make with Ada blog post series. “Ada and SPARK are most known for their track record in large-scale long-lived systems, but you can use these languages and AdaCore’s tools for software that has to run in the most resource-limited embedded environments including bare metal targets.” The “Make with Ada” competition is part of an overall AdaCore initiative to foster the growth of Ada and SPARK for developing embedded systems and more generally for developing “software that matters”. Other elements of this initiative are the free on-line training available at AdaCore U (u.adacore.com), and the various resources for free software developers and students/hobbyists at the GitHub repository (github.com/AdaCore) and the libre site (libre.adacore.com). Further information about Ada and SPARK, along with links to free resource pages and instructions on how to get started by downloading the GNAT GPL edition for Bare Board ARM, are available at http://makewithada.org/getting-started. Ada is a modern, internationally standardized programming language with a long and successful track record in the development of high-reliability embedded systems. Its strong typing and compile-time checking help catch errors early, when they are easiest and least expensive to correct. The most recent version of the Ada standard, Ada 2012, supports contract-based programming (pre- and postconditions for subprograms), which in effect embeds the software’s low-level requirements as checkable assertions in the source code. In critical systems where testing alone might not provide sufficient confidence, the SPARK subset of Ada supports mathematics-based assurance that relevant program properties are met (for example, the absence of run-time errors such as buffer overflow). SPARK can be introduced incrementally into a project, and contracts can be verified either statically (by the SPARK proof engine) or dynamically (with run-time checks). Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical, and security-critical systems. Four flagship products highlight the company’s offerings: Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as railway systems, space systems, commercial avionics, military systems, air traffic management/control, medical devices, and financial services. AdaCore has an extensive and growing world-wide customer base; see www.adacore.com/customers/ for further information. AdaCore products are open source and come with expert on-line support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com
News Article | May 24, 2017
YOKOHAMA, Japan--(BUSINESS WIRE)--Automotive Engineering Exposition--AdaCore today announced that MHI Aerospace Systems Corporation (MASC), a member of the Mitsubishi Heavy Industries Group, has selected the QGen toolset to develop the software for the Throttle Quadrant Assembly (TQA) system. This avionics research project is being conducted to meet the Level C objectives in the DO-178C safety standard for airborne software and its DO-331 supplement on Model-Based Development and Verification. The use of a qualified code generator can help save significant effort in developing and verifying the software, and the future availability of qualification material from AdaCore factored strongly in MASC’s decision to choose QGen. The QGen code generator can be qualified at the highest Tool Qualification Level, TQL-1 (equivalent to a development tool in DO-178B). “The QGen product is specifically targeted to model-based development in safety-critical control systems,” said Juan-Carlos Bernedo, QGen Product Manager at AdaCore. “However, model-based development raises some important questions: how to verify the model’s safety properties, such as freedom from run-time errors, and how to know that the properties are preserved in the generated code. QGen and its supporting TQL-1 qualification material help to answer these questions, and we’re pleased that MASC’s Throttle Quadrant Assembly project will be taking advantage of these benefits.” “We chose QGen as our Auto Code Generator because we believe TQL-1 qualification will reduce the effort of our verification activities that comply with DO-331,” said Hiroyuki Kakamu, General Manager of MASC. “As part of the TQA project, we discussed DO-331 compliance with AdaCore’s engineers. Based on these discussions, we developed a Model-Based Design process that complies with DO-331 based on the use of QGen.” QGen’s qualifiable and customizable code generator processes a safe subset of Simulink® and Stateflow® models and generates optimized source code in the safety-oriented programming languages SPARK (a formally analyzable Ada subset) and MISRA C. QGen incorporates static model verification, processor-in-the-loop (PIL) testing on a real target or through emulation on the host robust, and powerful model-level debugging support for back-to-back testing between simulation and target execution. TQA is a product of Tamagawa Seiki Co., Ltd., for light airplanes. Tamagawa Seiki Co., Ltd., is a Japanese manufacturer that develops a variety of products for the airplane and automotive markets. In 2014 they and MASC developed the TQA product controlled by software that was written manually, not using MBD. In 2016 they initiated a research project to redevelop the TQA using MBD technologies, and they verified that it had good enough functionality and performance as compared with the original TQA. Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. Four flagship products highlight the company’s offerings: Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as commercial avionics, automotive, railway, space, military systems, air traffic management/control, medical devices and financial services. AdaCore has an extensive and growing worldwide customer base; see www.adacore.com/customers/ for further information. AdaCore products are open source and come with expert online support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com Founded in 1986, MHI Aerospace Systems Corp. is a member of the MHI Group dedicated to custom computer programming services for the aerospace industry. It is located in Nagoya, Japan. Lately MASC has been conducting various activities related to DO-178C certification such as researching the standards, discussing with DERs, consulting to Japan’s equipment manufacturers, etc. Now MASC is a leading company for DO-178C technologies in Japan.
News Article | May 23, 2017
NEW YORK & PARIS--(BUSINESS WIRE)--AdaCore today announced the continuing growth of its Future Airborne Capability Environment (FACE™) support, through both the current availability of its GNAT Pro 17.1 Ada Development Environment for the Wind River® FACE Certified VxWorks® 653 Platform, and initiation of the FACE verification/certification process for GNAT Pro 17.1. VxWorks 653 is the first Commercial-Off-The-Shelf (COTS) product to be certified as conformant to the FACE Technical Standard’s Operating System Segment (OSS) Safety Base Profile. By using GNAT Pro on this platform, developers of embedded software can realize the benefits of Ada’s high reliability together with the safety-critical support and ease of rapid component integration that come from VxWorks 653 and its FACE conformance. GNAT Pro for VxWorks 653 includes a configurable run-time library facility that is targeted toward high-assurance applications. The “cert” run-time profile for VxWorks 653, which includes support for threading, exceptions, and (limited) dynamic allocation, has been used in airborne systems that have been certified to DO-178B Design Assurance Level (DAL) A. “Wind River and AdaCore have a long history in providing software solutions to modern avionics projects,” said Jamie Ayre, Commercial Director at AdaCore. “With the VxWorks 653 platform certified as FACE conformant, we look forward to continuing to offer the best-in-class software development tools for avionics applications taking advantage of the efficiencies of the FACE Technical Standard." ”Extending Wind River’s certified FACE conformant COTS platform with a robust Ada runtime that is proven in multiple high-criticality environments is another proof point of our ongoing successful collaboration with AdaCore,” stated Chip Downing, Senior Director of Aerospace and Defense at Wind River. “Both companies look forward to our continued efforts helping customers build highly configurable, standards-based, safety-critical solutions for global military platforms.” AdaCore has been actively participating in the FACE Consortium for the past five years, with the objective of ensuring that Ada’s software engineering benefits are appropriately reflected in the Ada language profiles. With all internal testing and analysis showing that GNAT Pro supports the FACE OSS Ada language requirements, AdaCore has started working with an approved FACE Verification Authority (VA) to verify that GNAT Pro Ada meets the applicable FACE Technical Standard requirements for the Ada Language Runtime Safety and Security Profiles. Availability GNAT Pro for VxWorks 653 is available immediately. About AdaCore Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. Four flagship products highlight the company’s offerings: Over the years, customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as space systems, commercial avionics, military systems, air traffic management/control, rail systems, medical devices and financial services. AdaCore has an extensive and growing worldwide customer base; see www.adacore.com/customers for further information. About Wind River VxWorks 653 Platform Wind River VxWorks 653 Platform offers a complete ARINC 653 product that safely and reliably delivers an ARINC 653 platform to the Integrated Modular Avionics (IMA) marketplace. VxWorks 653 Platform provides robust partitioning to enable the asynchronous insertion of applications from multiple suppliers without forcing a re-test of the entire platform. The avionics consolidation platform enables reduction of space, weight and power requirements, as well as reduction of the bill of materials, on the industry’s most advanced aircraft. VxWorks 653 Platform supports open standards by allowing customers to choose from a variety of APIs when developing their software. Applications can be written to ARINC 653, VxWorks, and/or POSIX APIs. Wind River’s commitment to open standards and portability is strengthened by supporting the FACE Technical Standard managed by The Open Group. VxWorks 653 is the first RTOS to be certified conformant to the FACE Technical Standard Operating System Segment (OSS) Safety Base Profile, supporting all ARINC 653 and POSIX capabilities required by the FACE Conformance Test Suite. About The Open Group FACE™ Consortium The FACE Consortium was formed in June 2010 as a government and industry partnership to define an open avionics environment for all military airborne platform types. Today, it is an aviation-focused professional group made up of industry suppliers, customers and users. It provides a vendor-neutral forum for industry and government to work together to develop and consolidate the open standards, best practices, guidance documents and business models necessary to result in:
Dross C.,AdaCore |
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2017
Formal program verification can guarantee that a program is free from broad classes of errors (like reads of uninitialized data and run-time errors) and that it complies with its specification. Tools such as SPARK make it cost effective to target the former in an industrial context, but the latter is much less common in industry, owing to the cost of specifying the behavior of programs and even more the cost of achieving proof of such specifications. We have chosen in SPARK to rely on the techniques of auto-active verification for providing cost effective formal verification of functional properties. These techniques consist in providing annotations in the source code that will be used by automatic provers to complete the proof. To demonstrate the potential of this approach, we have chosen to formally specify a library of red-black trees in SPARK, and to prove its functionality using auto-active verification. To the best of our knowledge, this is the most complex use of auto-active verification so far. © Springer International Publishing AG 2017.
Proceedings of the ACM SIGAda Annual International Conference; SIGAda | Year: 2012
We give a hands-on introduction to the tools GNATtest and GNATprove, both developed at AdaCore in the Hi-Lite research project. They allow to do verification of Ada 2012 contracts through testing and formal verification, and also allow a combination of the results of both tools. The tutorial will contain a very short introduction to Ada 2012, and attendees will write a small example on which they can play with GNATtest to develop test cases, and GNATprove to do some formal verification. © 2012 Author.
CrossTalk | Year: 2010
Static analysis tools are gaining popularity for safeguarding against the most common causes of errors in software. The main focus of these tools is on automatic bug-finding-the first stage in a two-phase process where the tool finds bugs and the human then corrects them. This article explains that such a goal is too narrow for critical software assurance (SwA). Instead, static analysis tools should adopt a broader perspective: computing properties of software.
Ada User Journal | Year: 2015
This paper continues the publication of the "SPARK 2014 Rationale", which started in the December 2013 issue of the Ada User Journal. In this instalment, we present three contributions regarding ghost code, Object Oriented programming and functional update in SPARK.
News Article | November 28, 2016
NEW YORK, PARIS, & SINDELFINGEN, Germany--(BUSINESS WIRE)--#ARM--AdaCore announces winners of the first annual Make with Ada competition, an initiative designed to foster the growth of Ada and SPARK for developing embedded systems.
News Article | December 6, 2016
NEW YORK & PARIS & SAN JOSE, Calif.--(BUSINESS WIRE)--Embedded Systems Conference - AdaCore today announced that its CodePeer advanced static analysis tool for Ada has been formally designated as “CWE-Compatible” by the MITRE Corporation’s Common Weakness Enumeration (CWE) Compatibility and Effectiveness Program. This program is a web-based initiative that consolidates and organizes information about cyber-security products and services. “It’s a great achievement to have CodePeer officially recognized as CWE compatible, which confirms that the tool can detect the most frequent types of software vulnerability,” said Arnaud Charlet, AdaCore Technical Director and CodePeer Product Manager. “CodePeer’s deep analysis of Ada code supports a wide range of uses including coding standard checking, automated code review, and exhaustive detection of certain CWE weaknesses as well as other kinds of error.” CodePeer was recognized as CWE-Compatible based on its ability to detect the following code weaknesses, which are among the CWE’s Top 25 Most Dangerous Software Errors: A number of other CWE weaknesses are also detected by CodePeer: CodePeer is an Ada source code analyzer that detects run-time and logic errors. It assesses potential bugs before program execution, serving as an automated peer reviewer, helping to find errors efficiently and early in the development life-cycle. It can also be used to perform impact analysis when introducing changes to the existing code, as well as helping vulnerability analysis for legacy systems. Using control-flow, data-flow, and other advanced static analysis techniques, CodePeer detects errors that would otherwise only be found through labor-intensive debugging. The tool’s deep analysis can directly support formal certification against industry-specific safety standards. For avionics applications CodePeer has been qualified as a Software Verification Tool under DO-178B, automating a number of verification activities defined in paragraph 6.3.4f (“Accuracy and consistency”). These activities include detecting errors such as values outside the bounds of an Ada type or subtype, buffer overflows, integer overflow or wraparound, division by zero, use of uninitialized variables, and floating point underflow. CodePeer has also been qualified for EN 50128, the highest international standard for safety integrity concerning software for railway control and protection, including communications, signaling and processing systems. The EN 50128 qualification material addresses the following: Qualification materials for DO-178B and EN 50128 are available as an option with CodePeer. CodePeer is fully integrated into AdaCore’s GNAT Pro development environment and comes with a number of complementary static analysis tools common to the technology – a coding standard verification tool (GNATcheck), a source code metric generator (GNATmetric) and a document generator. Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. Four flagship products highlight the company’s offerings: Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as space systems, commercial avionics, military systems, air traffic management/control, railway systems, medical devices and financial services. AdaCore has an extensive and growing worldwide customer base; see www.adacore.com/customers/ for further information. AdaCore products are open source and come with expert online support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com CodePeer is available now. Please contact AdaCore (email@example.com) for information on product pricing and supported configurations.