Getting Rid of Rust with Ada

There are a lot of DIY CNC projects out there (router, laser, 3D printer, egg drawing, etc.), but I never saw a DIY CNC sandblaster. So I decided to make my own.

#STM32    #Embedded    #ARM    #Makers   

SPARKZumo Part 1: Ada and SPARK on Any Platform

So you want to use SPARK for your next microcontroller project? Great choice! All you need is an Ada 2012 ready compiler and the SPARK tools. But what happens when an Ada 2012 compiler isn’t available for your architecture?

#CCG    #SPARK    #Arduino    #RISC V    #Embedded   

Ada on the micro:bit

Updated July 2018

#Embedded    #Ada    #nRF51    #ARM   

Tokeneer Fully Verified with SPARK 2014

Tokeneer is a software for controlling physical access to a secure enclave by means of a fingerprint sensor. This software was created by Altran (Praxis at the time) in 2003 using the previous generation of SPARK language and tools, as part of a project commissioned by the NSA to investigate the rigorous development of critical software using formal methods. The project artefacts, including the source code, were released as open source in 2008. Tokeneer was widely recognized as a milestone in industrial formal verification. We recently transitioned this software to SPARK 2014, and it allowed us to go beyond what was possible with the previous SPARK technology. We have also shown how security vulnerabilities introduced in the code can be detected by formal verification.

#SPARK    #Formal Methods   

The Road to a Thick OpenGL Binding for Ada: Part 2

This blog post is part two of a tutorial based on the OpenGLAda project and will cover implementation details such as a type system for interfacing with C, error handling, memory management, and loading functions.

#OpenGL    #Binding   

For All Properties, There Exists a Proof

With the recent addition of a Manual Proof capability in SPARK 18, it is worth looking at an example which cannot be proved by automatic provers, to see the options that are available for proving it with SPARK. We present three ways to complete a proof beyond what automatic provers can do: using an alternative automatic prover, proving interactively inside our GPS IDE, and using an alternative interactive prover.

#SPARK    #Formal Methods   

Bitcoin blockchain in Ada: Lady Ada meets Satoshi Nakamoto

Bitcoin is getting a lot of press recently, but let's be honest, that's mostly because a single bitcoin worth 800 USD in January 2017 was worth almost 20,000 USD in December 2017. However, bitcoin and its underlying blockchain are beautiful technologies that are worth a closer look. Let’s take that look with our Ada hat on!

#Bitcoin    #Blockchain    #Ada   

The Road to a Thick OpenGL Binding for Ada: Part 1

This blog post is part one of a tutorial based on the OpenGLAda project and will cover some the background of the OpenGL API and the basic steps involved in importing platform-dependent C functions.

#OpenGL    #Binding   

Leveraging Ada Run-Time Checks with Fuzz Testing in AFL

Fuzzing is a very popular bug finding method. The concept, very simple, is to continuously inject random (garbage) data as input of a software component, and wait for it to crash. If, like me, you find writing robustness test tedious and not very efficient in finding bugs, you might want to try fuzzing your Ada code.Here's a recipe to fuzz-test your Ada code, using American Fuzzy Lop and all the runtime checks your favorite Ada compiler can provide.Let's see (quickly) how AFL works, then jump right into fuzzing 3 open-source Ada libraries: ZipAda, AdaYaml, and GNATCOLL.JSON.

#Testing    #Ada    #VerificationTools   

Cross-referencing Ada with Libadalang

Libadalang has come a long way since the last time we blogged about it. In the past 6 months, we have been working tirelessly on name resolution, a pretty complicated topic in Ada, and it is finally ready enough that we feel ready to blog about it, and encourage people to try it out.

#Libadalang    #Ada   

Make with Ada 2017- Ada Based IoT Framework

SummaryThe Ada IoT Stack consists of an lwIp (“lightweight IP”) stack implementation written in Ada, with an associated high-level protocol to support embedded device connectivity nodes for today’s IoT world. The project was developed for the Make With Ada 2017 competition based on existing libraries and ported to embedded STM32 devices.

#Embedded    #Ada    #IoT   

There's a mini-RTOS in my language

The first thing that struck me when I started to learn about the Ada programing language was the tasking support. In Ada, creating tasks, synchronizing them, sharing access to resources, are part of the language

#Ada    #Ravenscar    #Embedded    #STM32   

Physical Units Pass the Generic Test

The support for physical units in programming languages is a long-standing issue, which very few languages have even attempted to solve. This issue has been mostly solved for Ada in 2012 by our colleagues Ed Schonberg and Vincent Pucci who introduced special aspects for specifying physical dimensions on types. This dimension system did not attempt to deal with generics though. As was noted by others, handling generics in a dimensional analysis that is, like in GNAT, a compile-time analysis with no impact on the executable size or running time, is the source of the problem of dimension handling. Together with our partners from Technical Universitat München, we have finally solved this remaining difficulty.

#GNAT     #typing   

Make with Ada 2017: Brushless DC Motor Controller

This project involves the design of a software platform that provides a good basis when developing motor controllers for brushless DC motors (BLDC/PMSM). It consist of a basic but clean and readable implementation of a sensored field oriented control algorithm. Included is a logging feature that will simplify development and allows users to visualize what is happening. The project shows that Ada successfully can be used for a bare-metal project that requires fast execution.

#Makers    #MakewithAda    #STM32    #Embedded   

#SPARK   

#Formal Verification    #SPARK   

Highlighting Ada with Libadalang

While we are working very hard on semantic analysis in Libadalang, it is already possible to leverage its lexical and syntactic analyzers. A useful example for this is a syntax highlighter.

#Libadalang    #Ada   

#gdb