Software Components

The software for the buoy is written in SPARK, a strict subset of the Ada programming language. This was chosen because of its high integrity and reliability. Once the buoy is deployed, there will be no opportunity to correct software bugs or errors, so a solid program is essential.

Unfortunately, the microcontroller we chose (Texas Instruments MSP430) has no Ada compiler available. In order to combat this, a software toolchain has been created, which can be seen at right.

In detail, the SPARK code written by the developers is run through Altran's SPARK examiner to ensure that the annotations match the code. The code is then run through SofCheck's AdaMagic compiler, which compiles the Ada code into C code. That C code is then combined with microcontroller device drivers written in C and called from Ada, and it is compiled for the MSP430 platform using Rowley Associates' CrossWorks.