For the IceCube mission we intend to use SPARK 2014. This is a change from our BasicLEO mission where we used the older (and now obsolete) SPARK 2005. Unlike the previous version of SPARK, the new SPARK 2014 language and tools offer a much richer and more powerful environment for software development. In particular, SPARK 2014 supports a larger subset of the Ada language, and the tools include more modern and more powerful automatic theorem provers.
It was our original intention to use our CubeSat operating system CubedOS in the IceCube mission. However, experience with the latest SPARK tools supporting Ada's Ravenscar tasking profile has shown that CubedOS has a design flaw that makes analyzing it with SPARK difficult. We have thus decided to set aside the goal of using CubedOS for the IceCube software, and instead just borrow ideas from CubedOS to help with IceCube. Once this project is well in hand, we hope to copy what we learned back to CubedOS, generalizing the lessons in the process. We hope our experience with IceCube will allow us to offer a much more refined and practical version of CubedOS to other groups in the future.