Fri 24 October 2014

[Adacore] Better error locations for flow analysis

Flow analysis used to point at the export (Something) when it issued messages like
  warning: incorrect dependency "Something => State"
We now point at the incorrect dependency (State) instead.

Thu 23 October 2014

[Adacore] High Integrity Software

Oct 23, 2014 – Bristol, UK

AdaCore is a major sponsor of this event and will be exhibiting.

[Adacore] AdaCore’s CodePeer Static Analysis Tool Earns Qualification for Software Verification in Avionics, R

Automatic code review and validation tool meets rigorous industry software verification standards; provides trusted reliability for Ada developers in safety-critical applications

NEW 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.”

Avionics Qualification
CodePeer has been qualified as a verification tool for DO-178B, the software safety standard for commercial airborne systems. Certification authorities such as the FAA in the U.S. and EASA in Europe apply DO-178B to provide confidence that the software will meet its requirements.

Vulnerabilities detected by CodePeer analysis for avionics include following:

  • Overflow on integer and floating point types
  • Range violations on integer and floating point types
  • Index violations on array operations
  • Division by zero on integer and floating point types
  • Uninitialized variables
  • Underflow on floating point types

Where no potential error is reported, CodePeer guarantees that the code is exempt from these vulnerabilities.

Railway Qualification
For railway applications, CodePeer has been used to verify code certified in accordance with CENELEC EN 50128:2011 SIL 4 --the highest safety integrity level.

In this context, CodePeer has been used for the following activities:

  • Boundary value analysis: it detects attempts to dereference a pointer that could be null, to read values outside the bounds of an Ada type or subtype, and also detects buffer overflows, numeric overflow or wraparound, and division by zero.
  • Control flow analysis: it detects suspicious and potentially incorrect control flows, such as unreachable code, redundant conditionals, loops that either run forever or fail to terminate normally, and subprograms that never return.
  • Data flow analysis: it detects suspicious and potentially incorrect data flows, such as variables read before they are written (uninitialized variables), variables written more than once without being read (redundant assignments), variables that are written but never read, and parameters with an incorrect mode (unread parameter, unassigned parameter).

CodePeer can be used in conjunction with AdaCore’s GNAT Pro development environment where it is tightly integrated into AdaCore’s GPS (GNAT Programming Studio) and GNATbench IDEs, or as a standalone product. It 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), a semantic analyzer and a document generator.

A demo highlighting the new features introduced in the latest version of CodePeer can be viewed at the following url: http://www.adacore.com/codepeer-2-3-demo/

About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore's flagship product is the open source GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see www.adacore.com/customers/ for further information.

Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including space-based systems, commercial aircraft avionics, military systems, air traffic management/control, railroad systems, and medical devices, and in security-sensitive domains, such as financial services. The SPARK Pro toolset, available from AdaCore, is especially useful in such contexts.

AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com

Press Contacts

Jamie Ayre

AdaCore

press@adacore.com

http://twitter.com/AdaCoreCompany

Jenna Beaucage
Rainier Communications
jbeaucage@rainierco.com
508.475.0025, ext. 124

[Adacore] AdaCore Development Environment Selected for New Spanish Satellite Project

NEW YORK, PARIS and BRISTOL, October 23, 2014, High Integrity Software Conference, Bristol, UKAdaCore 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.

The software component of the project is being led by UPM’s Real-Time Systems and Telematic Services Engineering Research Group (Grupo de Sistemas de Tiempo Real e Ingeniería de Servicios Telemáticos / STRAST), with coding and testing scheduled to be completed by the end of 2014. The development environment is GNAT Pro for 32-bit Linux, targeted to the LEON3 processor.

UPM STRAST selected Ada for its combination of high reliability, speed of development, and ease of verification and validation. The team has extensive experience using Ada on previous high-integrity embedded system projects, and has collaborated with AdaCore on a number of these.

The STRAST team is using the GNAT technology  to program the control software of the satellite’s on-board LEON3 processor, which is expected to reach 20,000 lines of code. UPM STRAST is using its own Open Ravenscar Real-Time Kernel (ORK), along with the Ada code generator from the TASTE toolset (The ASSERT Set of Tools for Engineering). AdaCore verification and validation tools will be used to ensure code integrity, using an approach based on the ECCS-ST-E40 standard.

"Controlling a satellite’s operation requires software that meets the highest levels of reliability and integrity,” said Professor Juan Antonio de la Puente, Universidad Politécnica de Madrid. “Ada was the obvious choice, and the combination of GNAT Pro and model-based code generation has proved to be a very fast way of developing reliable software for this project. UPMSat-2 provides the perfect platform for our students to develop their skills, and for STRAST to demonstrate its capabilities in real-time embedded systems to potential commercial partners.”

The UPMSat-2 hardware platform’s on-board computer is an ACTEL FPGA board developed by TECNOBIT, with UPM responsible for synthesizing the System On Chip (SOC) from the Gaisler GRLIB IP Library for LEON3 processors.

“We have collaborated with the team at UPM STRAST for 20 years across a number of projects,” said Cyrille Comar, AdaCore Managing Director. “This ambitious satellite project demonstrates all the advantages of Ada as a language, requiring reliable, real-time software that will need to operate in the toughest conditions. We look forward to the successful completion of the satellite and its launch in 2015.”

About AdaCore

Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore's flagship product is the open source GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see www.adacore.com/customers/ for further information.

Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including space-based systems, commercial aircraft avionics, military systems, air traffic management/control, rail systems, and medical devices, and in security-sensitive domains, such as financial services. The SPARK Pro toolset, available from AdaCore, is especially useful in such contexts.

AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com

About UPM
Universidad Politécnica de Madrid (UPM) is the oldest and largest of the Spanish Technical Universities. UPM currently has more than 3000 faculty members, around 38,000 undergraduate students, and around 6,000 postgraduate students. UPM’s schools cover most engineering disciplines, including aeronautical, agronomical, chemical, civil, electrical, electronic, forestry, industrial, mechanical, mining, nuclear, and naval engineering, as well as architecture, computer science, and geodesy & cartography.

The Real-Time Systems and Telematic Services Engineering Research Group (STRAST) is focused on research and teaching in the area of real-time and high-integrity systems, as well as new generation telematics services on mobile devices.

###

All brand or product names are registered trademarks or trademarks of their respective holders.

Press Contact

Jamie Ayre

AdaCore

press@adacore.com

http://twitter.com/AdaCoreCompany

[Adacore] GPS:—version and—help no longer require GUI

The switches are parsed before GPS attempts to connect to the GUI environment. As a result, it is possible to get the help or the version even when the environment is not setup for GUI.

[Adacore] Support for overriding keyword in Ada 95 mode

For compatibility with some Ada 95 compilers which support only the overriding keyword of Ada 2005, the -gnatd.D debug switch can now be used along with -gnat95 to achieve a similar effect with GNAT.

Tue 21 October 2014

[Adacore] ACM SIGAda’s HILT 2014

Oct 21-24, 2014 – Portland, OR, USA

AdaCore is a Platinum sponsor/exhibitor, and Tucker Taft is Program Chair.

[Adacore] Use of floating-point in fixed-point operations

In the presence of restriction No_Floating_Point, a multiplication of two fixed point quantities of the same fixed point type in an integer context does not generate conversions to floating-point for run-time evaluation.

Mon 20 October 2014

[Adacore] New implementation of Ghost entities

The SPARK toolset now implements the new semantic and legality rules of Ghost entities. This feature now encompases states, objects, subprograms, packages and types. As a result, convention Ghost has been replaced with aspect Ghost.

[Adacore] Raise, no-return and statically-false assertions

Flow analysis now ignores all statements that inevitably lead to a raise statement, a statically-false assertion or a non-returning procedure. Additionally, all statements that follow a raise statement, a statically-false assertion or a non-returning procedure that are not otherwise reachable from the start of the subprogram are also ignored.

Fri 17 October 2014

[Adacore] Support for Runtime & Target attributes in projects

These two new attributes are now supported by GPS and should replace the use of the IDE'Gnatlist attribute to specify the same information.

Wed 15 October 2014

[Adacore] GPRslave control of simultaneous responses

A new option has been added to GPRslave to control the number of simultaneous responses (sending back object code and ALI files) supported. This was hard coded to 2, it is now possible to set this value between 1 and the maximum number of simultaneous compilations.