AdaCore
150 W. 30th Street, 16th floor
New York, NY 10001 [email protected]
+1 212 620 7300
https://www.adacore.com/
New York, NY 10001 [email protected]
+1 212 620 7300
https://www.adacore.com/
Articles related to AdaCore
Cyber
Building trust in a model-based automatic code generator - Story
August 16, 2016
How do you go about building trust in an automatic code generator used for safety-critical systems? For example, given a code generator that takes a real-time model for a flight control system represented in Simulink and Stateflow and turns it into MISRA C or the SPARK subset of Ada, what process could ensure that the [...]
Comms
Ada Watch: Bringing Ada onto the battlefield - Blog
July 28, 2014
The growth in smartphones and tablets is radically changing the face of military technology. As in civilian life, the power of commercial off-the-shelf (COTS) handheld devices is enabling fast, frontline access to systems that previously required larger, bulkier computers. For example, ruggedized phones and tablets now have the processing power to access mission-critical command and control and communication systems, while being portable enough to fit into a pocket. In these systems the original operating system (OS) and consumer-oriented applications are replaced by customized versions that include domain-specific software using proprietary and/or confidential algorithms.
Avionics
AdaCore launches free online programming university - News
October 31, 2013
NEW YORK. AdaCore recently launched a free online resource center called AdaCore University, created for anyone interested in learning about the Ada programming language. The website offers learn-at-your-own-pace pre-recorded courses, with access to AdaCore’s GNAT Ada toolset for writing and running example programs.
Avionics
Ada Watch: Choosing the right Ada subset for strong static guarantees - Blog
August 13, 2013
While Ada offers many features that act as safety guards at run time, by raising exceptions when a violation is detected, some of these features may be too complex to guarantee a safe execution before the program is run. This is the case for example of pointers, which may be used to create arbitrarily complex shared data structures in memory. SPARK is a subset of Ada that forbids these features, most notably pointers, in order to be able to provide strong guarantees at compile time. A preview of the next revision of SPARK called SPARK 2014 is already available, as well as the associated verification tools.
Avionics
Completion of Project Hi-Lite to improve verification for high integrity systems - News
May 30, 2013
PARIS and NEW YORK. AdaCore has announced the completion of Project Hi-Lite, a joint research project focused on enhancing formal verification for multi-language, open-source software projects that require safety certification. Leveraging Airbus verification methods and industry tools, Project Hi-Lite combined formal proofs with testing and static analysis to improve the development of high integrity software. In the process, the Hi-Lite project also produced the first tools capable of integrating testing and formal verification for Ada and C programs.
Avionics
GNAT Pro 7.1 release includes Ada 2012 support, other enhancements - News
April 25, 2013
SAN JOSE, CA. A new release of the GNAT Pro multi-language development environment has been released by AdaCore. GNAT Pro 7.1 is a Freely Licensed Open Source Software (FLOSS) that includes enhancements in Ada language features, new tools, and run-time improvements over previous versions.
Avionics
DO-332, the Liskov Substitution Principle, and local type consistency ramp up DO-178 certification - Story
March 12, 2013
DO-332, the DO-178C standard's supplement on Object-Oriented Technology (OOT) and related techniques, analyzes the issues raised by object orientation in safety-critical software and supplies new guidance to deal with OOT's vulnerabilities. An important new objective of DO-332 is "Local Type Consistency Verification," which exploits a type theory result known as "the Liskov Substitution Principle" and helps address some of the key certification challenges raised by OOT's dynamic flexibility.
