AdaCore Blog

26 entries tagged with #Floating Point

by Jon Andrew

CuBit: A General-Purpose Operating System in SPARK/Ada

Last year, I started evaluating programming languages for a formally-verified operating system. I've been developing software for a while, but only recently began work in high integrity software development and formal methods. There are several operating system projects, like the SeL4 microkernel and the Muen separation kernel, that make use of formal verification. But I was interested in using a formally-verified language to write a general-purpose OS - an environment for abstracting the underlying hardware while acting as an arbiter for running the normal applications we're used to.

by Pat Rogers

From Ada to Platinum SPARK: A Case Study for Reusable Bounded Stacks

This blog entry describes the transformation of an Ada stack ADT into a completely proven SPARK implementation that relies on static verification instead of run-time enforcement of the abstraction’s semantics. We will prove that there are no reads of unassigned variables, no array indexing errors, no range errors, no numeric overflow errors, no attempts to push onto a full stack, no attempts to pop from an empty stack, that subprogram bodies implement their functional requirements, and so on. As a result, we get a maximally robust implementation of a reusable stack abstraction providing all the facilities required for production use.

#SPARK    #Ada    #Transitioning to SPARK   

by Pat Rogers

Making an RC Car with Ada and SPARK

As a demonstration for the use of Ada and SPARK in very small embedded targets, I created a remote-controlled (RC) car using Lego NXT Mindstorms motors and sensors but without using the Lego computer or Lego software. I used an ARM Cortex System-on-Chip board for the computer, and all the code -- the control program, the device drivers, everything -- is written in Ada. Over time, I’ve upgraded some of the code to be in SPARK. This blog post describes the hardware, the software, the SPARK upgrades, and the repositories that are used and created for this purpose.

#Ada    #SPARK    #Robotics   

by Allan Ascanius , Per Dalgas Jakobsen

Winning DTU RoboCup with Ada and SPARK

The Danish Technical University has a yearly RoboCup where autonomous vehicles solve a number of challenges. We participated with RoadRunner, a 3D printed robot with wheel suspension, based on the BeagleBone Blue ARM-based board and the Pixy 1 camera with custom firmware enabling real-time line detection. Code is written in Ada and formally proved correct with SPARK at Silver level.

#Robotics    #Ada    #SPARK   

by Yannick Moy

Two Days Dedicated to Sound Static Analysis for Security

​AdaCore has been working with CEA, Inria and NIST to organize a two-days event dedicated to sound static analysis techniques and tools, and how they are used to increase the security of software-based systems. The program gathers top-notch experts in the field, from industry, government agencies and research institutes, around the three themes of analysis of legacy code, use in new developments and accountable software quality. Here is why it is worth attending.

#SPARK    #Frama-C    #Security    #Formal Methods    #Static Analysis   

by Yannick Moy

Research Corner - FLOSS Glider Software in SPARK

Two years ago, we redeveloped the code of a small quadcopter called Crazyflie in SPARK, as a proof-of-concept to show it was possible to prove absence of run-time errors (no buffer overflows, not division by zero, etc.) on such code. The researchers Martin Becker and Emanuel Regnath have raised the bar by developing the code for the autopilot of a small glider in SPARK in three months only. Their paper and slides are available, and they have released their code as FLOSS for others to use/modify/enhance!

#Formal Verification    #Dev Projects    #SPARK   

by Yannick Moy

Research Corner - Floating-Point Computations in SPARK

It is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the values taken by entities in the program. Thanks to the recent changes in SPARK 17, users can now benefit from much better provability for these programs, by combining the capabilities of different provers. For the harder cases, this requires using ghost code to state intermediate assertions proved by one of the provers, to be used by others. This work is described in an article which was accepted at VSTTE 2017 conference.

#Formal Verification    #SPARK   

by Jorge Real

Writing on Air

While searching for motivating projects for students of the Real-Time Systems course here at Universitat Politècnica de València, we found a curious device that produces a fascinating effect. It holds a 12 cm bar from its bottom and makes it swing, like an upside-down pendulum, at a frequency of nearly 9 Hz. The free end of the bar holds a row of eight LEDs. With careful and timely switching of those LEDs, and due to visual persistence, it creates the illusion of text... floating in the air!

#STM32    #Ravenscar    #Ada    #Makers    #Embedded Development   

by Fabien Chouteau , Arnaud Charlet , Yannick Moy

SPARK Tetris on the Arduboy

One of us got hooked on the promise of a credit-card-size programmable pocket game under the name of Arduboy and participated in its kickstarter in 2015. The kickstarter was successful (but late) and delivered  the expected working board in mid 2016. Of course, the idea from the start was to program it in Ada , but this is an 8-bits AVR microcontroller (the ATmega32u4 by Atmel) not supported anymore by GNAT Pro. One solution would have been to rebuild our own GNAT compiler for 8-bit AVR from the GNAT FSF repository and use the AVR-Ada project. Another solution, which we explore in this blog post, is to use the SPARK-to-C compiler that we developed at AdaCore to turn our Ada code into C and then use the Arduino toolchain to compile for the Arduboy board.

by Yannick Moy

GNATprove Tips and Tricks: What’s Provable for Real Now?

One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK). Since then, we have integrated static analysis in SPARK, and modified completely the way floating-point numbers are seen by SMT provers. Both of these features lead to dramatic changes in provability for code doing fixed-point and floating-point computations.

#Formal Verification    #SPARK   

by Yannick Moy

The Most Obscure Arithmetic Run-Time Error Contest

Something that many developers do not realize is the number of run-time checks that occur in innocent looking arithmetic expressions. Of course, everyone knows about overflow checks and range checks (although many people confuse them) and division by zero. After all, these are typical errors that do show up in programs, so programmers are aware that they should keep an eye on these. Or do they?

#Formal Verification    #SPARK   

by Yannick Moy

GNATprove Tips and Tricks: What’s Provable for Real?

SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known fixed-point reals, called this way because their precision is fixed (contrary to floating-points whose precision varies with the magnitude of the encoded number). This support is limited in some ways when it comes to proving properties of computations on real numbers, and these limitations depend strongly in the encoding chosen. In this post, I show the results of applying GNATprove on simple programs using either floating-point or fixed-point reals, to explain these differences.

#Formal Verification    #SPARK   

by Anthony Leonardo Gracio

How to prevent drone crashes using SPARK

The Crazyflie is a very small quadcopter sold as an open source development platform: both electronic schematics and source code are directly available on their GitHub and its architecture is very flexible. Even if the Crazyflie flies out of the box, it has not been developed with safety in mind: in case of crash, its size, its weight and its plastic propellers won’t hurt anyone! But what if the propellers were made of carbon fiber, and shaped like razor blades to increase the drone’s performance? In theses circumstances, a bug in the flight control system could lead to dramatic events. In this post, I present the work I did to rewrite the stabilization system of the Crazyflie in SPARK 2014, and to prove that it is free of runtime errors. SPARK also helped me to discover little bugs in the original firmware, one of which directly related with overflows. Besides the Crazyflie, this work could be an inspiration for others to do the same work on larger and more safety-critical drones.

#UAVs    #crazyflie    #SPARK    #Drones   

by Yannick Moy

How Our Compiler Learnt From Our Analyzers

Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction. We recently discovered such an inconsistency in how our compiler and analyzers dealt with floating-point exponentiation, which lead to a change in how GNAT now compile these operations.

#Compilation    #Formal Verification    #SPARK   

by Olivier Ramonat

AdaCore Releases GNAT Pro 7.3, QGen 1.0 and GNATdashboard 1.0

February saw the annual customer release of a number of important products. This is no mean task when you consider the fact that GNAT Pro is available on over 50 platforms and supports over 150 runtime profiles (ranging from Full Ada Support to the very restricted Zero Footprint Profile suitable for safety-critical development). All in all, from the branching of the preview version to the customer release it takes us nearly 4 months to package everything up! Quality is assured through the internally developed AdaCore Factory.

#GNAT Pro    #SPARK Pro    #GPS    #GNATbench    #GNATdashboard    #Ada    #AdaCore Factory    #CodePeer    #QGen   

by Yannick Moy

Using SPARK to Prove AoRTE in Robot Navigation Software

Correctness of robot software is a challenge. Just proving the absence of run-time errors (AoRTE) in robot software is a challenge big enough that even NASA has not solved it. Researchers have used SPARK to do precisely that for 3 well-known robot navigation algorithms. Their results will be presented at the major robotics conference IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2014) this coming September.

#Formal Verification    #SPARK    #Robotics