26 entries tagged with #Events
by Pat Rogers
Task Suspension with a Timeout in Ravenscar/JorvikThis blog entry shows how to define an abstract data type that allows tasks to block on objects of the type, waiting for resumption signals from other components, for at most a specified amount of time per object. This "timeout" capability has been available in Ada from the beginning, via select statements containing timed entry calls. But what about developers working within the Ravenscar and Jorvik tasking subsets? Select statements and timed calls are not included within either profile. This new abstraction will provide some of the functionality of timed entry calls, with an implementation consistent with the Ravenscar and Jorvik subsets.
by Pat Rogers
On the Benefits of Families ... (Entry Families)
Ada has a concurrency construct known as “entry families” that, in some cases, is just what we need to express a concise, clear solution.
Make with Ada 2020: CHIP-8 InterpreterLaurent Zhu's and Damien Grisonnet's project was accomplished for the EPITA Ada courses and won a finalist prize in the Make with Ada 2019/20 competition.
by Emma Adby
Make with Ada 2020: The SmartBase - IoT Adjustable BedJohn Singleton's The SmartBase makes your existing adjustable bed safer and easier to use by adding voice control and safe (and fun!) LED underbed lighting! Additionally, this project won first place prize in the 2019/20 Make with Ada competition.
by Jon Andrew
CuBit: A General-Purpose Operating System in SPARK/AdaLast 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.
Using GNAT-LLVM to target Ada to WebAssembly
The GNAT-LLVM project provides an opportunity to port Ada to new platforms, one of which is WebAssembly. We conducted an experiment to evaluate the porting of Ada and the development of bindings to use Web API provided by the browser directly from Ada applications.
RecordFlux: From Message Specifications to SPARK CodeHandling binary data is hard. Errors in parsers routinely lead to critical security vulnerabilities. In this post we show how the RecordFlux toolset eases the creation of formally verified binary parsers in SPARK.
by Boran Car
Bringing Ada To MultiZoneC is the dominant language of the embedded world, almost to the point of exclusivity. Due to its age, and its goal of being a “portable assembler”, it deliberately lacks type-safety, opening up exploit vectors. Proposed solutions are partitioning the application into smaller intercommunicating blocks, designed with the principle of least privilege in mind; and rewriting the application in a type-safe language. We believe that both approaches are complementary and want to show you how to combine separation and isolation provided by MultiZone together with iteratively rewriting parts in Ada. We will take the MultiZone SDK demo and rewrite one of the zones in Ada.
A Modern Syntax for AdaOne 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.
by Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 2This 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.
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!
Leveraging Ada Run-Time Checks with Fuzz Testing in AFLFuzzing 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.
by Yannick Moy
(Many) More Low Hanging BugsWe reported in a previous post our initial experiments to create lightweight checkers for Ada source code, based on the new Libadalang technology. The two checkers we described discovered 12 issues in the codebase of the tools we develop at AdaCore. In this post, we are reporting on 6 more lightweight checkers, which have discovered 114 new issues in our codebase. This is definitely showing that these kind of checkers are worth integrating in static analysis tools, and we look forward to integrating these and more in our static analyzer CodePeer for Ada programs.
New strings package in GNATCOLLThis post describes the new GNATCOLL.Strings package, and the various optimizations it performs to provide improved performance.
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!
AdaCore attends FOSDEMEarlier this month AdaCore attended FOSDEM in Brussels, an event focused on the use of free and open source software. Two members of our technical team presented.
Unity & AdaUsing Ada technologies to develop video games doesn’t sound like an an obvious choice - although it seems like there could be an argument to be made. The reverse, however, opens some more straightforward perspectives.
C library bindings: GCC plugins to the rescue
I recently started working on an Ada binding for the excellent libuv C library. This library provides a convenient API to perform asynchronous I/O under an event loop, which is a popular way to develop server stacks. A central part of this API is its enumeration type for error codes: most functions use it. Hence, one of the first things I had to do was to bind the enumeration type for error codes. Believe it or not: this is harder than it first seems!
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!
by Yannick Moy , Jamie Ayre , Emma Adby
Ada Lovelace Bicentennial
The three of us attended the Ada Lovelace Symposium in Oxford (UK). The two days were one fantastic discovery after another about the life, achievements and legacy of Ada Lovelace, the programming pioneer who lent her name to the Ada language.
AdaCore Tech Days 2015
by Jack Mellor
2015: A Space Ada‑sseyAdaCore has a long history of providing tools and support to develop mission critical applications for Space. Check out this video we made and showed at the conference to see which ones!
Make with Ada: All that is useless is essentialA 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 .
How to prevent drone crashes using SPARKThe 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.
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!