Fabien joined AdaCore in 2010 after his engineering degree at the EPITA (Paris). He is involved in real-time, embedded and hardware simulation technology. Maker/DIYer in his spare time, his projects include electronics, music and woodworking.
55 entries written by Fabien Chouteau
In a previous post we presented the RecordFlux specification language and toolset, illustrating how to design and generate formally proven binary protocol parsers and serializers. In this follow-up we will look at the protocol session part of RecordFlux.
This week we announced a new tool called RecordFlux. The goal of RecordFlux is to address one of the most critical parts of the software stack in terms of security, binary protocol parsers/serializers.From a protocol specification written in the RecordFlux Domain Specific Language (DSL), the tool can generate provable SPARK code. This means memory safety (no buffer overruns), absence of integer overflow errors, and even proof of functional properties. In this blog post I will try to explain how this is a game changer for cybersecurity.
AdaCore has partnered closely with Lynx to deliver Ada language support alongside its LYNX MOSA.ic software framework that comprises a real-time operating system (LynxOS-178), Linux and hypervisor (LynxSecure) technology.
Last year we announced our strategic partnership with Ferrous Systems, a technology company specializing in the Rust programming language. Today we are announcing a new step in our involvement with the Rust ecosystem and community
This year marks the return of the FOSDEM conference as an "in-person" event. As always, AdaCore will participate in this major gathering of the free and open source community.We encourage you to stop by the Ada-Europe booth (Building K, level 2) to have a chat or get answers to any questions regarding Ada, SPARK, or other topics, such as those covered in our blog.
In June of 2022 we launched the second edition of the Ada/SPARK Crate Of The Year Awards. We believe the Alire source package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem. Today we are pleased to announce the results. But first, we want to congratulate all the participants, and the Alire community at large, for reaching 320 crates in the ecosystem in January of this year. We truly believe in a bright future for the Ada/SPARK open-source ecosystem with Alire at the forefront. Reaching this milestone is a great sign,both inside and outside the Ada/SPARK community, of the evolution and the energy of the ecosystem.
At the end of November we called the Ada and SPARK programmers community to take on a challenge for a good cause. We are now in January and it is time for the results!
From time to time we see, here and there, discussions in the Ada community about the design and adoption of a common logo to represent the language. Today we want to bring our contribution to this discussion by offering a logo to the Ada community.
A few months ago I was reading this article about coroutines in game development and how they are great tools for writing scripts (as in movie scripts) in the same language as the game engine. Until then I heard about coroutines but never really gave them a thought, this piqued my curiosity.
Every year since 2015, a team of dedicated individuals led by Eric Wastl organizes an online programming challenge called: Advent of Code. The concept is simple yet brilliant: from December 1st to 25th, every day a new small programming exercise is published on the adventofcode.com website. This year we want to join the fun, and bring a little bit of extra motivation for a good cause.
Today I want to share a great story about why many NVIDIA products are now running formally verified SPARK code. This blog post is in part a teaser for the case study that NVIDIA and AdaCore published today. Our journey begins with the NVIDIA Security Team. Like many other security oriented teams in our industry today, they were looking for a measurable answer to the increasingly hostile cybersecurity environment and started questioning their software development and verification strategies.
For years in this blog my colleagues and I have published examples, demos, and how-to’s on Ada/SPARK embedded (as in bare-metal) development. Most of the time, if not always, we focused on one way of doing things: to start from scratch and write everything in Ada/SPARK, from the low level drivers to the application. While this way of doing Ada/SPARK embedded will yield the best results in terms of software quality, it might not be the most efficient in all cases. In this blog post I want to present an alternative method to introduce Ada/SPARK into your embedded development projects.
We're happy to announce our the second edition of our programming competition, the Ada/SPARK Crate Of The Year Award! We believe the Alire package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem.
Today we have two exciting announcements for the future of the Ada/SPARK ecosystem.
A few weeks ago a piece of code went viral in the online dev community. The “Quite OK Image Format” (QOI) is a fast, lossless image compression designed to have a very simple implementation (about 300 lines of C). Shortly, a few alternative implementations popped up here and there, and in this kind of situation we are eager to show what Ada/SPARK can bring to the table.
In this second post of the Ada GameDev series we will see how to create game maps and export them to a format that is compatible with the GESTE library.
In this first entry of the series, I want to present my GEneric Sprite and Tile Engine (GESTE) project. The goal of GESTE is to bring the rendering and anesthetic of 8bit era game consoles to modern microcontrollers.
Like previous years, AdaCore will participate in FOSDEM. Once again the event will be online only, but this won’t prevent us from celebrating Open Source software and it is an opportunity for even more people to participate around the world.
In June of 2021 we announced the launch of a new programming competition called Ada/SPARK Crate Of The Year Awards. We believe the Alire source package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem. Today we are pleased to announce the results. But first, we want to congratulate all the participants, and the Alire community at large, for reaching 200 crates in the ecosystem in January of this year. We truly believe in a bright future for the Ada/SPARK open-source ecosystem with Alire at the forefront. Reaching this milestone is a great sign, inside and outside the Ada/SPARK community, of the evolution and the energy of the ecosystem.
A couple years ago I started to tackle what was probably my most daunting project at the time, an embedded USB Device stack written 100% in Ada.
A few days ago, someone asked on the Ada Drivers Library repository how to add support for the SAMD21 micro-controller. Nowadays, I would rather recommend people to contribute this kind of micro-controller support project to the Alire ecosystem. I started to write a few instructions on how to get started, but it quickly became a blog-worthy piece of text.
When I do Object Oriented Programming with Ada, I tend to follow a design pattern that makes it easier for me and hopefully also for people reading my code.
We're happy to announce our new programming competition, the Ada/SPARK Crate Of The Year Award! We believe the Alire package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem.
We are happy to announce that the GNAT Community 2021 release is now available via https://www.adacore.com/download. Here are some release highlights:
I am following the evolution of the embedded Rust community and in particular the work of James Munns from Ferrous-Systems. One of the projects that caught my attention is bbqueue, a single producer, single consumer, lockless, thread safe queue, based on BipBuffers.
Like previous years, AdaCore will participate in FOSDEM. This time the event will be online only, but this won’t prevent us from celebrating Open Source software. AdaCore engineers will give two talks in the Safety and Open Source devroom, a topic at the heart of AdaCore since its inception.
Beyond the great look, the Mini SAM M4 provide a powerful 120 Mhz Microchip SAMD51 Cortex-M microcontroller, a couple of LEDs and a user button. Let's program it with Ada.
In this blog post I want to present a new tool that allows one to very quickly and easily start Ada programming on any ARM Cortex-M or RISC-V microcontroller.
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
A few years ago we realized that having a package manager for the Ada/SPARK community would be a game changer. Since then, AdaCore has been sponsoring and contributing to the Alire project created by Alejandro Mosteo from the Centro Universitario de la Defensa de Zaragoza. With this blog post I want to introduce Alire and explain why this project is important for the `Ada`/`SPARK` community.
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
Starting today, AdaCore has put in place a Code of Conduct (CoC) to ensure a positive environment for everyone willing and wanting to interact with us. With the development of this blog, our twitter accounts, and our GitHub corporate account, there is more and more communication between AdaCore and a number of communities. In this Code of Conduct we want to explain how we are going to moderate the AdaCore-maintained community spaces with the goal of maintaining a welcoming, friendly environment.
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
Like last year and the year before, AdaCore will participate to the celebration of Open Source software at FOSDEM. It is always a key event for the Ada/SPARK community and we are looking forward to meet Ada enthusiasts. You can check the program of the Ada/SPARK devroom here.
I was quite happy to see AdaFruit release their first Feather format board including a micro-controller with plenty of Ada support, the STM32F4. I bought a board right away and implemented some support code for it.
When I bought the TinyFPGA-BX board, I thought it would be an opportunity to play a little bit with FPGA, learn some Verilog or VHDL. But when I discovered that it was possible to have a RISC-V CPU on it, I knew I had to run Ada code on it.
We are very proud to announce the availability of our new Ada and SPARK learning platform learn.adacore.com, which will replace AdaCoreU(niversity) e-learning platform. Learn all about it in this blog post.
One of the most criticized aspect of the Ada language throughout the years has been its outdated syntax. Fortunately, AdaCore decided to tackle this issue by implementing a new, modern, syntax for 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.
Updated July 2018
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
Updated July 2018
A few weeks ago one of my colleagues shared this kickstarter project : The Barisieur. It’s an alarm clock coffee maker, promising to wake you up with a freshly brewed cup of coffee every morning. I jokingly said “just give me an espresso machine and I can do the same”. Soon after, the coffee machine is in my office. Now it is time to deliver :)
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.
There are moments in life where you find yourself with an AdaFruit thermal printer in one hand, and an OpenMV camera in the other.
I started this project more than a year ago. It was supposed to be the first Make with Ada project but it became the most challenging from both, the hardware and software side.
A few months ago, my colleague Rebecca installed a candy dispenser in our kitchen here at AdaCore. I don’t remember how exactly, but I was challenged to make it more… fun.
When the Pebble Time kickstarter went through the roof, I looked at the specification and noticed the watch was running on an STM32F4, an ARM cortex-M4 CPU which is supported by GNAT. So I backed the campaign, first to be part of the cool kids and also to try some Ada hacking on the device.
July 20, 1969, 8:18 p.m. UTC, while a bunch of guys were about to turn blue on Earth, commander Neil A. Armstrong confirms the landing of his Lunar Module (LM), code name Eagle, on the moon. Will you be able to manually land Eagle on the Sea of Tranquillity?
A few weeks ago I discovered the wonderful world of solenoid engines. The idea is simple: take a piston engine and replace explosion with electromagnetic field. In this article I will experiment a solenoid engine using a hacked hard drive and a software controller on a STM32F4 .