AdaCore Blog

46 entries tagged with #embedded

by Emma Adby

It's time to Make with Ada!

The challenge Are you ready to develop a project to the highest levels of safety, security and reliability? If so, Make with Ada is the challenge for you! We’re calling on embedded developers across the globe to build cool embedded applications using the Ada and SPARK programming languages and are offering over $8000 in total prizes. In addition, eligible students will compete for a reward of an Analog Discovery 2 Pro Bundle worth $299.99!

by Pamela Trevino

Public Ada Training Paris, France Dec 3 - 7, 2018

This course is geared to software professionals looking for a practical introduction to the Ada language with a focus on embedded systems, including real-time features as well as critical features introduced in Ada 2012. By attending this course you will understand and know how to use Ada for both sequential and concurrent applications, through a combination of live lectures from AdaCore's expert instructors and hands-on workshops using AdaCore's latest GNAT technology. AdaCore will provide an Ada 2012 tool-chain and ARM-based target boards for embedded workshops. No previous experience with Ada is required.

by Julia Teissl

Train control using Ada on a Raspberry Pi

I was looking for a topic for my master thesis in embedded systems engineering when one of my advisor proposed the idea of programming a control system for autonomous trains in Ada. Since I am fascinated by the idea of autonomous vehicles I agreed immediately without knowing Ada. 

by Fabien Chouteau

Ada on FPGAs with PicoRV32

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.

#embedded    #RISC-V    #Ada   

by Pamela Trevino

AdaCore major sponsor at HIS 2018

We are happy to announce that, AdaCore, alongside Altran and Jaguar Land Rover will be major sponsors of the fifth edition of the renowned High Integrity Software Conference on the 6th November in Bristol!

by Fabien Chouteau, Emma Adby, Yannick Moy

Learn.adacore.com is here

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.

#Teaching    #Ada    #SPARK   

by Emma Adby, Fabien Chouteau

GNAT Community 2018 is here!

Calling all members of the Ada and SPARK community, we are pleased to announce that GNAT Community 2018 is here! adacore.com/download

by Johannes Kanig

Taking on a Challenge in SPARK

Last week, the programmer Hillel posted a challenge (the link points to a partial postmortem of the provided solutions) on Twitter for someone to prove a correct implementation of three small programming problems: Leftpad, Unique, and Fulcrum.

#Formal Verification    #Formal Methods    #SPARK   

by Rob Tice

SPARKZumo Part 2: Integrating the Arduino Build Environment Into GPS

This is part #2 of the SPARKZumo series of blog posts. This post covers the build system that was used to build the SPARKZumo project and how to automate the process in GPS.

#GPS    #Python    #Libadalang    #Arduino    #CCG   

by Fabien Chouteau

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   

by Rob Tice

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   

by Fabien Chouteau

Ada on the micro:bit

Updated July 2018

#embedded    #Ada    #nRF51    #ARM   

by Pierre-Marie de Rodat, Yannick Moy, Fabien Chouteau, Raphaël Amiard

AdaCore at FOSDEM 2018

Every year, free and open source enthusiasts gather at Brussels (Belgium) for two days of FLOSS-related conferences. FOSDEM organizers setup several “developer rooms”, which are venues that host talks on specific topics. This year, the event will happen on the 3rd and 4th of February (Saturday and Sunday) and there is a room dedicated to the Ada programming language.

by Manuel Iglesias Abbatermarco

Make with Ada 2017- Ada Based IoT Framework

Summary The 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   

by Fabien Chouteau

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   

by J. German Rivera

Make with Ada 2017- A "Swiss Army Knife" Watch

Summary  The Hexiwear is an IoT wearable development board that has two NXP Kinetis microcontrollers. One is a K64F (Cortex-M4 core) for running the main embedded application software. The other one is a KW40 (Cortex M0+ core) for running a wireless connectivity stack (e.g., Bluetooth BLE or Thread). The Hexiwear board also has a rich set of peripherals, including OLED display, accelerometer, magnetometer, gryroscope, pressure sensor, temperature sensor and heart-rate sensor. This blog article describes the development of a "Swiss Army Knife" watch on the Hexiwear platform. It is a bare-metal embedded application developed 100% in Ada 2012, from the lowest level device drivers all the way up to the application-specific code, for the Hexiwear's K64F microcontroller. I developed Ada drivers for Hexiwear-specific peripherals from scratch, as they were not supported by AdaCore's Ada drivers library. Also, since I wanted to use the GNAT GPL 2017 Ada compiler but the GNAT GPL distribution did not include a port of the Ada Runtime for the Hexiwear board, I also had to port the GNAT GPL 2017 Ada runtime to the Hexiwear. All this application-independent code can be leveraged by anyone interested in developing Ada applications for the Hexiwear wearable device.

by Jonas Attertun

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   

by Rob Tice

The Adaroombot Project

The Adaroombot project consists of an iRobot CreateⓇ 2 and Ada running on a Raspberry Pi with a Linux OS. This is a great Intro-to-Ada project as it focuses on a control algorithm and a simple serial communications protocol. The iRobot CreateⓇ 2 platform was originally design for STEM education and has great documentation and support - making it very easy to create a control application using Ada. This blog looks at the creation of the project and some cool features of Ada that were learned along the way.

#Raspberry Pi    #ARM    #Linux    #Ada    #Roomba   

by Fabien Chouteau

Ada on the first RISC-V microcontroller

Updated July 2018

#Embedded Development    #Ada    #RISC-V   

by Fabien Chouteau

DIY Coffee Alarm Clock

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 :)

#Embedded Development    #STM32    #Makers    #Ada    #ARM   

by Anthony Leonardo Gracio

GPS for bare-metal developers

In my previous blog article, I exposed some techniques that helped me rewrite the Crazyflie’s firmware from C into Ada and SPARK 2014, in order to improve its safety.

#GPS    #Embedded Development    #Makers   

by Pierre-Marie de Rodat

GNATcoverage moves to GitHub

Following the current trend, the GNATcoverage project moves to GitHub! Our new address is: https://github.com/AdaCore/gnatcoverage

#GitHub    #GNATcoverage   

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 Pat Rogers

Getting started with the Ada Drivers Library device drivers

The Ada Drivers Library (ADL) is a collection of Ada device drivers and examples for ARM-based embedded targets. The library is maintained by AdaCore, with development originally (and predominantly) by AdaCore personnel but also by the Ada community at large.  It is available on GitHub and is licensed for both proprietary and non-proprietary use.

#Ada    #Devices    #drivers    #STM32    #embedded   

by Fabien Chouteau

Make with Ada: DIY instant camera

There are moments in life where you find yourself with an AdaFruit thermal printer in one hand, and an OpenMV camera in the other.

#Makers    #Ada    #STM32    #ARM    #Embedded Development   

by AdaCore Admin

Make With Ada Winners Announced!

Judging for the first annual Make with Ada competition has come to an end and we can now reveal the results.

by Pat Rogers

Driving a 3D Lunar Lander Model with ARM and Ada

One of the interesting aspects of developing software for a bare-board target is that displaying complex application-created information typically requires more than the target board can handle. Although some boards do have amazing graphics capabilities, in some cases you need to have the application on the target interact with applications on the host. This can be due to the existence of special applications that run only (or already) on the host, in particular.

#Bareboard    #Embedded Development    #STM32    #Ada   

by Emmanuel Briot

GNAT Programming Studio (GPS) on GitHub

The GPS source repository has been published on GitHub. This post briefly describes how you can access it, and hopefully contribute.

#GPS    #GitHub   

by AdaCore Admin

Introducing the Make With Ada competition!

If you’ve been looking for a way to start your next embedded project in Ada or SPARK. Then, look no further than the Make with Ada competition!

#MakewithAda    #embedded    #SPARK     #Ada   

by Fabien Chouteau

Make with Ada: ARM Cortex-M CNC controller

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.

#Makers    #Ada    #STM32    #ARM    #Embedded Development   

by AdaCore Admin

Provably safe programming at Embedded World

AdaCore continues to build reliable and secure software for embedded software development tools. Last month, we attended Embedded World 2016, one of the largest conferences of its kind in Europe, to present our embedded solutions and our expertise for safety, and mission critical applications in a variety of domains.

#ARM    #emb2016    #embedded    #Embedded World   

by AdaCore Admin

Embedded Product Line Updates

Embedded products are not stand alone, this allows them to have safety, mission critical and real-time requirements that they wouldn’t necessarily have otherwise. The embedded product line provides analyzable, verifiable, and certifiable software for both static and dynamic analysis tools.

#AdaCoreTechDay    #GNAT     #Embedded Development    #embedded   

by AdaCore Admin

QGen 2.1 Release!

Embedded World will see the latest release of QGen, the qualifiable and customisable code generator for Simulink® and Stateflow® models!

#QGen    #QGen2.1    #AdaCoreTechDay    #Embedded World    #emb2016   

by AdaCore Admin

ERTS and Embedded World conferences 2016

We are pleased to announce that we will be a major sponsor and exhibitor at ERTS, Toulouse and will be exhibiting at Embedded World, Nuremberg in the coming months!

#ERTS2016    #Embedded World    #emb2016    #Embedded Development    #Safety Critical Development   

by AdaCore Admin

ARM TechCon and NBAA Conference 2015

We are continuing to develop tools for use within projects that require reliable and secure embedded software for ARM. Our engineering team have been busy creating demos running on ARM technology, such as Tetris in SPARK on ARM Cortex M4.

#ARM    #SPARK    #Drones    #NBAA2015    #ARMTechCon   

by Raphaël Amiard

Make with Ada : From bits to music

I started out as an electronic musician, so one of my original motivations when I learnt programming was so that I could eventually *program* the sounds I wanted rather than just use already existing software to do it.

#Makers    #Ada    #Embedded Development   

by Fabien Chouteau

Make with Ada: All that is useless is essential

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 .

#Makers    #Ada    #Embedded Development    #Devices    #STM32   

by Yannick Moy

A Building Code for Building Code

In a recent article in Communications of the ACM, Carl Landwehr, a renowned scientific expert on security, defends the view that the software engineering community is doing overall a poor job at securing our global information system and that this is mostly avoidable by putting what we know works to work, to the point that most vulnerabilities could be completely avoided by design if we cared enough. Shocking! Or so it should appear.

#Ada    #SPARK    #Static Analysis    #Security   

by Jamie Ayre

QGen on Embedded News TV

Embedded News TV caught up with our own Matteo Bordin to talk about QGen. Matteo provides a nice overview of QGen and it's position in the industry as the need for safe and secure software becomes increasingly important.

#QGen    #Safety Critical Development   

by AdaCore Admin

A Busy Schedule Ahead!

If you have a passion for Ada, need more information on our technology or would just like to have a chat, there are a couple of upcoming events where we'd love to meet up. What's more, we'll be launching our brand new product QGen at Embedded World!

#Ada    #Embedded World    #Certification Together    #QGen   

by Florian Schanda

SPARK 2014 Rationale: Data Dependencies

Programs often use a few global variables. Global variables make passing common information between different parts of a program easier. By reading the specification of a subprogram we are able to see all of the parameters that the subprogram uses and, in Ada, we also get to know whether they are read, written or both. However, no information regarding the use of global variables is revealed by reading the specifications. In order to monitor and enforce which global variables a subprogram is allowed to use, SPARK 2014 has introduced the Global aspect, which I describe in this post.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

Case Study for System to Software Integrity Includes SPARK 2014

My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study showing how formal verification with SPARK can be included in a larger process to show preservation of properties from the system level down to the software level. The case study is based on the Nose Gear challenge from the Workshop on Theorem Proving in Certification.

#Formal Verification    #Certification    #SPARK   

by Yannick Moy

Rail, Space, Security: Three Case Studies for SPARK 2014

We will present three case studies using SPARK 2014 at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February 2014, in three different domains: rail, space and security. The lessons learned in those three case studies are particularly interesting. Here is the companion paper that we wrote.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Mixing SPARK and Ada Code

The first step before any formal verification work with SPARK is to delimitate the part of the code that will be subject to formal verification within the overall Ada application. This post presents the solution we've come up with for SPARK 2014.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Loop Variants

Loop variants are the little-known cousins of the loop invariants, used for proving termination of subprograms. Although they may not look very useful at first, they can prove effective as I show with a simple binary search example. And we came up with both an elegant syntax and a slick refinement for loop variants in SPARK 2014, compared to similar constructs in other languages.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

Project Hi-Lite Wrap-up

After three years of hard work, we have reached last week the end of project Hi-Lite, whose goal was to simplify the use of formal methods. We're proud to publicize the results obtained, in particular the new version of SPARK and the associated tool GNATprove. Here's a summary of the wrap-up meeting.

#Formal Verification    #SPARK