Over on the Galois blog is a post about my current project, building a secure high-assurance autopilot called SMACCMPilot. SMACCMPilot is open-source; http://smaccmpilot.org/ is the project’s landing page that describes the technologies going into the project with links to the software repositories. Check it out!
Galois’ main approach to building SMACCMPilot is to use embedded domain-specific languages (EDSLs), embedded in Haskell that compile down to restricted versions of C. (If you’re not familiar with the “EDSL approach”, and particularly how it might improve the assurance of your systems, check out this paper we wrote about our experiences on a separate NASA-sponsored project.) The project is quickly approaching one of the larger EDSL projects I know about, and it’s still relatively early in its development. The EDSLs we’re developing for SMACCMPilot, Ivory (for embedded C code generation) and Tower (for OS task setup and communication), are suitable for other embedded systems projects as well.
Like many young and active open-source projects, the code is hot off the presses and under flux, and the documentation always lags the implementation, so let me know if you try using any of the artifacts and have problems. We’re happy to have new users and contributors!