Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College have written a truly essential book for getting up to speed with formal verification using SPARK.
...
I see this book as a glorified User's Guide to SPARK, and I recommend it to anybody who either wants to have a first look at SPARK, or actually starts using it for real.
...
For those in academia who would like to teach SPARK, the book is ideally structured with a summary and exercises closing each chapter.
...
You may also get a free copy of the book from Cambridge University Press to evaluate it for your course (see the publisher's webpage).
The AdaCore Blog
Make with Ada: Formal proof on my wrist
by Fabien Chouteau
Nov 10, 2015 http://blog.adacore.com/make-with-ada-formal-proof-on-my-wrist
When the Pebble Time kickstarter went through the roof, I ... https://www.pebble.com/pebble-time-smartwatch-features
...
Binding the C API to Ada
...
To use this binding I decided to port the formally proven Tetris written in SPARK by Yannick and Tristan.
...
The formal proof is focused on things that are impossible to test, in our case, the game system.
Can you think of a way to test that the code will reject invalid moves on any piece, in any orientation, at any position and for every board state possible (that's trillions or quadrillions of combinations)?
...
This application was released on the Pebble app store under the name of PATRIS, and as of today more than 660 users downloaded it.
...
Persistent storage
...
Sources
...
(YouTube video)
...
The latest version of the AdaCore cross-development environment for Raspberry Pi 2 micro-PC allows students and other DIY developers to do software development in Ada, C, C++ or any combination of these.
...
"understanding just a single language promotes solutions that only approach a problem from a single perspective.
Knowing multiple languages allows the problem to be looked at from a variety of perspectives so that multiple solutions can be compared and the most natural solution for the problem can be selected."
- Greg Gicca, currently director of marketing at Verocel, previously director of safety and security product marketing at AdaCore
Although part of the initial run-time for the STM32F429-Disco is delivered with GNAT, it is not necessarily well optimized (some missing interrupts and a non-optimal clock speed in particular).
So I included the sfp and full ravenscar run-times for it as well in the final source packages.
...
To go further in customized run-time, you can refer to the following documentation: ...
... hands-on lab sessions using the latest AdaCore tools and the STM32F4 Discovery Board, introduces software developers to the principal features of the Ada language with a special focus on embedded systems.
"I am using it on more than two dozen different ARM boards and love having tasking without a separate RTOS and not having to spend near as much time with a debugger." - Jerry Petrey
Partially; AdaCore has some packages that improve file system speed and abstract the file system for portability between operating systems (virtual files).
I have not used those but instead the usual method via Ada Text_IO (Ada -> complete Ada run-time -> RTOS or OS).
Pretty much eliminates the need for an operating system.
Dependent on the Ada run-time as described in its Footprint Profile.
For most embedded systems that don't have the Ada run-time on an RTOS there's either no file system (Zero Footprint Profile or ZFP) or a minimal one.
For ZFP, some ways around are :
RTOS - the Ada procedure and its ZFP run-time in a process, thread, or task within an RTOS; to and from the file I/O via the RTOS messaging or mailbox functions and Ada's C interface package.
C library - via Ada's C interface if the C library is per the pre-conditions for ZFP.
Otherwise, a typical GCC-based Ada has the Ada run-time on POSIX.
Therefore, a reasonably complete file system is available via an OS or some RTOS; an example is the port to Raspberry Pi 2.
This release supports the ARM ELF bare metal target, hosted on Windows and Linux, as well as the following native platforms:
Mac OS (64 bits)
Linux (64 bits)
Windows (32 bits)
The GNATemulator technology has been added to the bare metal target, making it easier to develop and test on those platforms.
The compiler toolchain is now based on GCC 6. The native runtime comes with a Zero Foot Print runtime, and the ARM ELF compiler comes with runtimes for a variety of boards, including support for the Raspberry Pi 2.
The latest version of the GPS IDE comes with many bug fixes and enhancements, notably in the areas of debugger integration and support for bare-metal development.
We decided to adopt the micro:bit as our reference platform for teaching embedded Ada and SPARK. We chose the micro:bit for its worldwide availability, great value for a low price and the included hardware debugger. You can get one at:
...
RISC-V support
...
Find SPARK included in the package by default
...
Windows 64bit is finally here
...
Arm-elf hosted on Mac
...
P.S.
Another US source for BBC micro:bit is SparkFun via Mouser.
As an added bonus to this year’s GNAT Community 2018 release, we are very happy to announce the launch of learn.adacore.com, an interactive learning platform designed to teach the Ada and SPARK programming languages!
This new website is designed for individuals who want to get up and running with Ada/SPARK, and also for teams or teachers looking for training or tutorial material. Read more about it here.
Feeling inspired and want to start Making with Ada today? Get started early for this year’s Make With Ada Competition! https://www.makewithada.org/
A guess is a relative yes as AdaCore recently added several levels to their GNAT Pro product including a reduced price developer version (arm, RISC-V); 'relative' as PowerPC was primary (avionics, vehtronics, mechatronics)
AdaCore recently revamped and partitioned the product line into four editions: GNAT Pro Assurance, GNAT Pro Enterprise, GNAT Pro Developer, and the free, open-source GNAT Pro Community.
...
Developer and Community
The new Developer edition targets new Ada and SPARK developers.
...
Its pricing is on par with commercial C/C++ development suites. It provides direct support and access to the continuous patched releases. The community edition gets updated, but with a longer update cycle [1y].
...
All editions support bare-metal Arm platforms as well as embedded Linux. And all but the Community edition support QNX. This is significant, since QNX is used in high-reliability and safety application areas such as automotive.
...
Companies looking to develop safe, secure, bug-free code for their applications should consider the advantages of using Ada and SPARK. Getting started is now more economical.
If you like some heavy reading, then check out John Barne’s Programming in Ada 2012. This rather hefty book is in depth and a useful reference, but not a great idea for novice Ada programmers.
The Ada and SPARK courses are extensive but not exhaustive.
...
[AdaCore's CWE mitigations]
...
P.S.
Using programming languages like C and C++ to develop these types of applications [safe, secure, and reliable], so that developers can improve the quality of their code, usually means relying on additional software such as static-analysis tools.
lint and assert go a long way at zero price and low cost.
Static-analysis tools may implement software development process requirements for safety and/or security.
P.P.S.
Ada and it subset, SPARK, incorporate most features addressed by static-analysis tools.
Posted by gchapman: Tue. Jun 25, 2019 - 03:39 AM(Reply to #78)
1
2
3
4
5
Total votes: 0
Not available in GNAT Community Edition though CCG should be in GNAT Pro Developer as that can also build C.
Haven't inquired the price of GNAT Pro Developer though it was created to reduce the gap between GNAT Community Edition and GNAT Pro Enterprise (that's expensive)
(nearly complete fixed point math, last chance exception handling that's akin to how exceptions are done in C, no overflow checks so consider enabling assertions)
AVR - IIRC, there's a post in this forum stating a successful build of AVR GNAT from FSF GCC 8 or from GNAT Community Edition; AVR-Ada was recently updated.
CCG would be a fit for PIC, PIC24, and dsPIC; PIC32 - MIPS is in FSF GCC so simply build the Ada part of FSF GCC (runtime would be some effort though doable for some functionality besides Zero Footprint Profile [ZFP])
Based on the automotive-qualified SAMV71, the SAMV71Q21RT radiation-tolerantandSAMRH71 radiation-hardened MCUs implement the widely deployed Arm® Cortex®-M7 System on Chip (SoC), enabling more integration, cost reduction and higher performance in space systems.
Even if we’ve been able to report some successes over the years, we were falling short of the critical mass.
Or so it seemed.
The tide has turned.
...
The Established User Base
[avionics, defense]
...
Some applications are still maintained today on hardware dating as far back as Motorola 68K or Intel i386 series, while others are deployed on the latest ARM Cortex or RISC-V cores.
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopAda on an Atmel SAM3X8E :
The URL sequence to the above :
Other :
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopAda on a Texas Instruments ARM Cortex-R4F, the RM46L852 (dual ARM Cortex-R4F, ECC flash, ECC local SRAM, FPU, MPU, 16-bit EMIF) :
It's a Work-In-Progress though well along.
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Top"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Top"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Top"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Top"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopSTM32F469I-Discovery
STM32F746G-Discovery
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Top"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Top"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopFascinating. Has anyone seen an Ada file system? Pretty much eliminates the need for an operating system.
Imagecraft compiler user
- Log in or register to post comments
TopI have not used those but instead the usual method via Ada Text_IO (Ada -> complete Ada run-time -> RTOS or OS).
For most embedded systems that don't have the Ada run-time on an RTOS there's either no file system (Zero Footprint Profile or ZFP) or a minimal one.
For ZFP, some ways around are :
Otherwise, a typical GCC-based Ada has the Ada run-time on POSIX.
Therefore, a reasonably complete file system is available via an OS or some RTOS; an example is the port to Raspberry Pi 2.
http://libre.adacore.com/developers/documentation
http://libre.adacore.com/tools/gnat-component-collection/
http://www.adacore.com/press/adacore-introduces-gnat-gpl-2015-for-the-raspberry-pi-2/
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopNew board support :
https://github.com/AdaCore/Ada_Drivers_Library/tree/master/boards/OpenMV2
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Top"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopMore SAM :
https://github.com/AdaCore/embedded-runtimes/tree/master/ravenscar-sam4sxplainedpro
https://github.com/AdaCore/embedded-runtimes/tree/master/ravenscar-samg55xplainedpro
via
http://www.microchip.com/developmenttools/productdetails.aspx?partno=atsam4s-xpro
http://www.microchip.com/developmenttools/productdetails.aspx?partno=atsamg55-xpro
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Tophttp://libre.adacore.com/
http://docs.adacore.com/gnatemulator-docs/arm-elf-example.html
https://github.com/AdaCore/embedded-runtimes
http://libre.adacore.com/tools/gps/
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopLibre has been folded into AdaCore.
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopP.S.
Another US source for BBC micro:bit is SparkFun via Mouser.
https://www.mouser.com/new/sparkfun/sparkfun-bbc-microbit/
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Top"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopI guess this whole thread started before there was an ARM Cortex forum - but should it now be moved to the ARM Cortex forum ... ?
Top Tips:
- Log in or register to post comments
TopNo as AdaCore Community doesn't have much SAM (SAM 4S, SAM G55)
An advantage of a thread move would be to make it public by moving it out of the private Off Topic sub-forum.
https://github.com/AdaCore/bb-runtimes/tree/community-2018/arm/sam
via https://www.adacore.com/community
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Topin addition to GNAT Community 2018, today's e-mail has :
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopIs AdaCore seeing much Ada being used on ARM, including the smaller M parts?
- Log in or register to post comments
Toparm Cortex-M1 in FPGA :
https://github.com/AdaCore/bb-runtimes/tree/community-2018/arm/igloo
https://www.microsemi.com/product-directory/fpgas/1689-igloo#igloo-e
nRF51 (arm Cortex-M0) on BBC micro:bit :
https://github.com/AdaCore/bb-runtimes/tree/community-2018/arm/nordic
https://www.nordicsemi.com/eng/Products/Bluetooth-low-energy/nRF51822
Edit : 2nd URL
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopP.S.
lint and assert go a long way at zero price and low cost.
Static-analysis tools may implement software development process requirements for safety and/or security.
P.P.S.
One of the Ada static-analysis tools :
https://www.adacore.com/codepeer
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Top"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopDo you know if the CCG (Common Code Generator), that translates an Ada subset into C, is available in the community version?
- Log in or register to post comments
TopNot available in GNAT Community Edition though CCG should be in GNAT Pro Developer as that can also build C.
Haven't inquired the price of GNAT Pro Developer though it was created to reduce the gap between GNAT Community Edition and GNAT Pro Enterprise (that's expensive)
1. Getting Started — GNAT Pro Common Code Generator User's Guide Supplement 20.0w documentation
(nearly complete fixed point math, last chance exception handling that's akin to how exceptions are done in C, no overflow checks so consider enabling assertions)
GNAT Pro Comparison - Adacore
more :
https://www.avrfreaks.net/forum/jack-ganssles-reason-8-why-embedded-software-projects-run-trouble#comment-2594186
AVR - IIRC, there's a post in this forum stating a successful build of AVR GNAT from FSF GCC 8 or from GNAT Community Edition; AVR-Ada was recently updated.
CCG would be a fit for PIC, PIC24, and dsPIC; PIC32 - MIPS is in FSF GCC so simply build the Ada part of FSF GCC (runtime would be some effort though doable for some functionality besides Zero Footprint Profile [ZFP])
SAM - a few are already there; for others :
bb-runtimes/doc/porting_runtime_for_cortex_m at community-2018 · AdaCore/bb-runtimes · GitHub
RISC-V - that may take some thought (CPU configuration is very flexible)
MSP430TM - in FSF GCC (add the Ada part to the C part, likely will be ZFP)
https://sourceforge.net/p/avr-ada/mailman/avr-ada-devel/?viewmonth=201903
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Topadditional is
https://github.com/AdaCore/bb-runtimes/tree/master/arm/sam/samv71
Add Microsemi CoreCortexM1 BSP · AdaCore/bb-runtimes@1fd54d0 · GitHub
SAM V MCUs | Microchip Technology
FPGAs | Microsemi
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Top"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopAda for micro:bit Part 1: Getting Started - The AdaCore Blog
Ada for micro:bit Part 2: Push buttons - The AdaCore Blog
edit :
Ada for micro:bit Part 3: Pin Output | The AdaCore Blog
Ada for micro:bit Part 4: Pin Input | The AdaCore Blog
edit2 :
Ada for micro:bit Part 5: Analog Output | The AdaCore Blog
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
Topcan add another (SAM D51)
Mini SAM M4 Ada BSP | The AdaCore Blog
https://www.microchip.com/sitesearch/search/Product%20and%20Development%20Tools/ATSAMD51G
GitHub - bwshockley/Mini-SAM: Respository for Mini Sam PCB board using a SAMD51.
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopIn alpha state on SAM D51 and RP2040 :
An Embedded USB Device stack in Ada | The AdaCore Blog
SAM D | Microchip Technology
Raspberry Pi is now a microcontroller | AVR Freaks
"Dare to be naïve." - Buckminster Fuller
- Log in or register to post comments
TopPages