18 entries tagged with #Safety Critical Development
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.by Quentin Ochem
NVIDIA is joining the Ada and SPARK adopter wave
Over the past several years, a great number of public announcements have been made about companies that are either studying or adopting the Ada and SPARK programming languages. Noteworthy examples include Dolby, Denso, LASP and Real Heart, as well as the French Security Agency.
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.by Yannick Moy
Verified, Trustworthy Code with SPARK and Frama-C
Last week, a few of us at AdaCore have attended a one-day workshop organized at Thales Research and Technologies, around the topic of "Verified, trustworthy code - formal verification of software". Attendees from many different branches of Thales (avionics, railway, security, networks) were given an overview of the state-of-practice in formal verification of software, focused on two technologies: the SPARK technology that we develop at AdaCore for programs in Ada, and the Frama-C technology developed at CEA research labs for programs in C. The most interesting part of the day was the feedback given by three operational teams who have experimented during a few months with either SPARK (two teams) or Frama-C (one team). The lessons learned by first-time adopters of such technologies are quite valuable.by Quentin Ochem
Unity & Ada
Using 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.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.
by AdaCore Admin
Formal Verification Made Easy!
We are pleased to announce our latest release of SPARK Pro! A product that has been jointly developed alongside our partner Altran and following the global AdaCore Tech Days, you can now see the SPARK 2014 talk, Formal Verification Made Easy by AdaCore’s Hristian Kirtchev, on YouTube.
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!
by AdaCore Admin
Dissimilar tools: Use cases and impact on tool qualification level
Frederick Pothon of ACG Solutions has recently published a document entitled - Dissimilar tools: Use cases and impact on tool qualification level on the open-DO blog.
by Jack Mellor
2015: A Space Ada‑ssey
AdaCore 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!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.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.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.
by Jamie Ayre
20 years on...
20 Years of AdaCore: Company as Committed as Ever on Safety-Critical Software Solutions
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.
by Tristan Gingold, Yannick Moy
Tetris in SPARK on ARM Cortex M4
Tetris is a well-known game from the 80's, which has been ported in many versions to all game platforms since then. There are even versions of Tetris written in Ada. But there was no version of Tetris written in SPARK, so we've repaired that injustice. Also, there was no version of Tetris for the Atmel SAM4S ARM processor, another injustice we've repaired.