Update 2020

Once again it has been a while since anyone has posted to this blog. Once again, that does not reflect a lack of activity in our projects, as much as a lack of committment to keeping this blog up to date. Here I will review some of the things that have happened since the last update.

1. We are no longer working on the IceCube project mentioned in the previous post. While I believe that project is still active, the software development for it has been moved to Goddard Space Flight Center, as far as I know.

2. We have started a project implementing the JT65 communications protocol in SPARK with the intention of providing a CubedOS module that supports it. JT65 allows a low bandwidth signal to be received with very low reception strength. It has the potential of enabling some level of deep space (i. e. interplantary) CubeSat communications using relatively modest radio equipment on both ends of connection.

3. We are looking into implementing some subset of the DTN protocols (again in SPARK) for use with CubedOS. Our goal here is to be interoperable with ION, and implementation of the DTN protocols created by NASA. Our work would have the benefit of being verified by the SPARK tools to be free of runtime error (or more). This work is in preparation of implementing some sort of distributed CubeSat demonstration, perhaps in collaboration with the University of Vermont.

4. We are thinking about creating a CubedOS/CFS bridge that would allow CubedOS to interoperate with NASA's CFS. Users of CFS could then incrementally use CubedOS, perhaps for mission critical functions (due to CubedOS's verification properties), while retaining their investment in CFS.

We are looking forward to making progress on these projects in the coming months. Hopefully we will be able to maintain this blog more regularly so that interested parties can follow the work.

General Update

This blog has been inactive for a while, but that's not because the Vermont Technical College CubeSat Laboratory has been inactive. In fact, we've been quite busy these past months ramping up on our next project. We are writing the flight software for Lunar IceCube, a collaboration between Morehead State University's Space Science Center, NASA Goddard Space Flight Center, NASA Jet Propulsion Laboratory, Busek Inc., and ourselves.

The mission is a 6U CubeSat (nominally 10cm x 20cm x 30cm) that will orbit the moon and make infrared observations looking for water in all of its phases (and other volatile compounds). We will piggyback on the maiden launch of SLS, along with several other CubeSat missions, and be deployed as SLS heads beyond the moon.

We intend to use CubedOS for the Lunar IceCube mission, making this the first time CubedOS will be deployed in space. This also gives us the opportunity to refine and enhance our ideas about CubedOS in the context of solving real problems for a real mission. We have been gathering software requirements, writing necessary infrastructure, and setting up both software and hardware test harnesses. Last May we attended the Lunar IceCube Preliminary Design Review (PDR) at Goddard Space Flight Center. Last October we spent a week at Morehead State University meeting with our collaborators there. Also last October we gave a paper at the High Integrity Language Technologies Workshop in Pittsburgh, PA that described Lunar IceCube and outlined the architecture of our SPARK flight software. Last December we attended the Flight Software Workshop in Pasadena, CA. We recently submitted a paper to Ada Europe 2017 which, if accepted, will be CubedOS's official debut.

It is our plan to resume regular posts on this blog so that those in the community who are interested in our work can stay apprised of our status. We'll be very busy in the coming months implementing the IceCube flight software, and we are sure there will be many issues that will arise during that effort that we can post about here.

CubedOS and CFDP

We have been building a general purpose infrastructure for CubeSat flight control software that we call CubedOS. Applications using CubedOS are organized as a collection of interacting "modules" with at least one thread of control, or task, per module. The CubedOS infrastructure provides an asynchronous messaging service as well as libraries of other useful space-mission oriented tools. Task management is handled by the underlying Ada runtime system under the restrictions imposed by the Ravenscar profile. It is our intention to eventually verify freedom from runtime errors using the SPARK tools although we don't yet have access to SPARK 2014 tools that can process Ada tasking constructs.

In part to demonstrate the usability of CubedOS, as well as to create a valuable software component in its own right, we are currently working on an implementation of the CCSDS File Delivery Protocol (CFDP) as a CubedOS module. This is a work in progress but so far it illustrates both what is good and bad about the CubedOS architecture.

CFDP requires that multiple, simultaneous file transfers be supported. Furthermore, a CFDP "entity" (the software implementing the protocol), must be able to simultaneously receive requests from a CFDP "user" (the software using the protocol) as well as protocol data units (PDUs) from a peer CFDP entity. These requirements are relatively straightforward to implement using CubedOS's message passing architecture.

Each CFDP entity executes a loop that first receives a message from its mailbox and then processes it. Roughly this loop looks like:

   loop
      Message_Manager.Mailboxes(MyID).Receive(Incoming_Message);
      -- Decode and process Incoming_Message
   end loop;

Messages coming from the CFDP user to initiate new file transfers and messages coming from the underlying communication module containing PDUs for active transfers can be mixed freely with no special handling. Provided the messages contain enough information to distinguish one transaction from another, it is also easy to see how to manage multiple transactions at once. The CFDP module maintains state information about all active transactions and uses information in the message to update the state of the appropriate transaction. Of course, processing an incoming message may require a reply message to be sent to either the CFDP user or to the underlying communication module. Again this presents no special problems and is quite straightforward to program.

The concurrency inherent in CubedOS allows CFDP protocol processing, communications, and high level application logic, to all execute simultaneously. Receiving a PDU in the communications module and processing some previously received PDU can be overlapped.

However, although the architecture of CubedOS is clearly well suited to this example there are problems with it as well:

• Messages can potentially pile up in a module's mailbox causing large and difficult to predict latencies in message handling. Even determining how large a mailbox is necessary can be problematic.
• There is runtime overhead associated with encoding and decoding CubedOS messages. We have yet to fully analyze the amount of overhead involved and its possible impact on performance.
• There is a loss of static type safety since invalid messages are detected and handled at runtime. Compare this to the static checking of procedure parameter types in normal Ada. This is a worrisome issue in light of our desire to ensure high levels of reliability in our software.
• The analyzability of CubedOS with SPARK remains to be seen. We await access to SPARK tools that can handle Ada's tasking constructs.

Yet despite the possible difficulties, we are encouraged so far by our experience with the CFDP implementation. The architecture of CubedOS is not without problems, but it clearly offers some nice advantages as well.

Programming an STM32F4DISCOVERY with Ada and GPS in Linux

Niels Huisman & Peter Chapin
VTC CubeSatLab

This tutorial was created using Linux Mint 17.1 Rebecca, and has been tested using Ubuntu 14.04. This information should also work with other Ubuntu-based distros, but that has not been tested.

Shorthand used:

<user> - Your username.
<filename> - Generic file name placeholder. Use whatever file name you wish.

 To make sure we have the required dependencies, get the following packages:

    $ sudo apt-get install autoconf
    $ sudo apt-get install automake
    $ sudo apt-get install pkg-config
    $ sudo apt-get install libusb-1.0
    $ sudo apt-get install git

This can also be done on one line:

    $ sudo apt-get install autoconf automake pkg-config libusb-1.0 git

Go to https://libre.adacore.com, click on the banner to download GNAT GPL select "Free Software for Academic Development", click on the button that says "Build Your Download Package", select "ARM ELF format (hosted on Linux)" from the drop-down menu, and download the GNAT GPL tarball for Linux.

Once downloaded, open a terminal (Ctrl+Alt+T), and navigate to the folder where it was downloaded (usually /home/<user>/Downloads). Once there, extract the file as follows:

    $ tar -xvf gnat-gpl-2015-arm-elf-linux-bin

This will create a folder of the same name.  Navigate to that folder using a command such as:

    $ cd gnat-gpl-2015-arm-elf-linux-bin

If you list all the files,  you will see a file called doinstall.  Execute that file using a command such as:

    $ sudo ./doinstall

You will need to enter your root password here. At some point during the install, you will be asked to specify the installation directory. If you already have GNAT installed for native development, you will need to somehow differentiate between the two. Here we use /opt/ARMgnat as the installation directory. If you have two separate GNAT installations, you will need to write a shell script to set the correct path when using GNAT for ARM. Open a text editor of your choice, write:

    export PATH=/opt/ARMgnat/bin:$PATH
    export ARMRUNTIME=/opt/ARMgnat/lib/gnat/arm-eabi/ravenscar-sfp-stm32f4

The first line makes the tools available at the shell prompt. The second line sets an environment variable used to locate the runtime system to be used in the programs. The idea is that Windows users could set ARMRUNTIME appropriately for their system and thus it is possible to share project files between Linux and Windows. For example in the GNAT project file for a project you might include:

    package Builder is
       for Default_Switches ("ada")
          use ("-g", "--RTS=" & external("ARMRUNTIME", ""));
    end Builder;

Save the shell script as <filename>.sh in /home/<user>/bin. Before using GNAT for ARM, you will need to run:

    $ source <filename>.sh

This will set the correct path for the ARM tool chain.

Now that we have GNAT and GPS installed, we need a way to communicate with the STM board, such as ST-Link. Fortunately, we can retrieve Texane STLink using Git using a command such as:

    $ git clone https://github.com/texane/stlink stlink

This will make a directory in /home/<user> called stlink. You can use any target directory name you like. Enter that director using a command such as:

    $ cd stlink


and run the following:

    $ ./autogen.sh
    $ ./configure
    $ make install

This will install st-flash, st-info, st-term, and st-util (the one we care about the most) in /usr/local/bin. To ensure that when st-util is run it behaves as though it was run as root, we need to modify it slightly. Change the owner (should be root already, but just to be sure), and the permissions as follows:

    $ sudo chown root /usr/local/bin/st-util
    $ sudo chmod 4755 /usr/local/bin/st-util

To check that everything took the way it's supposed to, run:

    $ ls -l /usr/local/bin

You should see an output similar to the following (the file size and, of course, date/time may be somewhat different):

    $ -rwsr-xr-x 1 root root 299527 May 14 12:11 st-util

Now that we have everything installed, connect your STM board using the USB mini B port, open a terminal, and run:

    $ /usr/local/bin/st-util

You should see a number of messages giving some information about your board and ending with "Listening at *:4242..." Open a separate terminal, navigate to the directory containing your project, run the script created earlier if necessary, and open GPS.

    $ source /home/<user>/bin/ARMgnatpath.sh
    $ gps

This will open up the GPS startup window where you can begin working.

VirtualBox Notes

If you are running Linux inside a VirtualBox virtual machine, you may wish to set up a USB filter so VirtualBox automatically recognizes the STM board. To do this, open up the virtual machine settings dialog box and select "USB." Click on the '+' symbol on the right to add a new USB filter. If you have the board plugged into your host, you should see it listed among the USB devices in the menu that appears. Selecting the board will set up a filter automatically.

Alternatively the filter can be set up manually using parameters such as the ones below. These values are appropriate for the STMF4DISCOVERY board. We suggest leaving the Serial Number field blank so the settings will work for any instance of the board (useful for sharing boards).

    Name: STMicroelectronics STM32 STLink [0100]
    Vendor ID: 0483
    Product ID: 3748
    Revision: 0100
    Manufacturer: STMicroelectronics
    Product: STM32 STLink
    Remote: No

After configuring a USB filter, boot the virtual machine with the board plugged into the host and VirtualBox should automatically make the board available to the VM.

CubedOS

To help support future missions we are currently working on a CubeSat "operating system" that we are calling CubedOS. Despite the name, CubedOS is really more of an application framework than a true operating system. It builds on the services provided by the underlying Ada runtime system, namely tasking support, which in turn are built (may be built) on top of some underlying host operating system.

Yet the intent of CubedOS is to serve an operating system-like role in the construction of CubeSat flight control software. It provides several common services needed by most, if not all, missions such as non-critical timing and background processing, a file system, a high level runtime library, and a driver model. CubedOS thus simplifies the construction of flight software by relieving the application developer of the burden of repeatedly providing these basic services.

At its core CubedOS provides a general purpose, asynchronous message passing facility that is used by CubedOS modules for inter-module communication. Because of the asynchronous messages, CubedOS applications can easily exhibit a high degree of concurrency. In addition, application developers do not need to separately design every communication path between interacting tasks; pre-built CubedOS messages should often be sufficient.

However, the message passing design of CubedOS also presents some challenges. The overhead of message passing may be unacceptable in some situations. We anticipate that some time critical interactions between tasks will still need to be hand designed. Furthermore the effect of the message passing architecture on the static analysis of CubedOS programs has yet to be fully explored. There is a potential loss of static type safety in the current architecture. Furthermore the ability for any module to asynchronously send a message to any other module (using potentially non-empty mailboxes) will likely complicate any real-time analysis required by the application. We intend to explore these issues further as we go forward. In the meantime our preliminary experiments with CubedOS do indicate that the architecture can simplify the construction of highly concurrent systems.

One might reasonably ask: why not just use the services of some suitable embedded operating system and be done with it? The main reason is our requirement to use SPARK and to insist on verifying freedom from runtime errors (at least). Most existing embedded operating systems are written in C and thus prone to errors that verified SPARK programs are not. That said, there do exist certified embedded operating systems that could potentially take over some of the functionality offered by CubedOS. Their use would allow us to replace certain packages in CubedOS with wrappers that simply enclose services provided by an underlying system while maintaining compatibility with CubedOS applications. We intend to explore this option in the future as well.

Introduction

Welcome to the Flying SPARKs blog!

This is the official blog of the CubeSat development team at Vermont Technical College (VTC). We are a group of students, faculty, and staff who are building spacecraft around the CubeSat standard. Classic "1U" (one unit) CubeSats are only 10 cm on each side and mass limited to 1.33 kg. Yet, thanks the miniaturization of modern electronics, these small spacecraft are still able to perform many useful functions.

There are numerous groups (academic, industrial, and governmental) who are building CubeSat spacecraft. What makes us different than the others is that we are using the SPARK programming language and tool set for our software development.

SPARK is a dialect of Ada that allows for the formal verification of programs. Using the SPARK tools it is possible to mathematically prove that one's software is free of many important classes of errors. Since CubeSat software is difficult or impossible to modify once it is deployed in space, increasing the robustness of that software is of great importance. The recent software problem with the Planetary Society's LightSail spacecraft is an example of the kind of error we hope to avoid by using SPARK.

Any member of the CubeSat development team at VTC can be an author on this blog. It is here where we share our musings about our work and post updates about our progress.

Enjoy!