SBTB 2023: Ivan Perez, Open Source in Space.
Recording: SBTB 2023: Ivan Perez, Open Source in Space.
Thanks everyone. Thank you for being here. Uh thank you for the introduction and thank you to the organizers for inviting me. Uh my name is Ivan Perez. I'm a contractor working for NASA Ames. Um and today I want to talk about open source for space. I want to talk about the work that I do, specifically developing and using open source and how we engage with the community and hopefully get some of you to contribute to the work that we do and to use it. Before I begin, let me make it very clear
I don't speak on behalf of the government, NASA, anybody else but myself. What you're about to see is my opinion and my opinion alone. If something is wrong, it's my fault and no one else's. Now, NASA is a big player when it comes to open source and it uses open source kind of everywhere. Uh very famously, the Mars helicopter, which is a helicopter that is flying in Mars, uh uses open source. It's a it's a Linux device. And it's used in the James Webb telescope and it's used in many many many many missions. And there's a repository of open source software that you can go to and you can find a lot of what we do
It's not everything. You can also go to places like GitHub and there's a NASA organization. You can find I think some something like 400 projects over there. So, there's a lot that is open and there's a lot more that you will find in different organizations because not everything is in the same place. Now, today I'm going to talk about my job. My job, plain and simple, is to develop the next generation of systems to make sure that things don't fall out of the sky. And what I do is I try to assure, mainly the software that we develop. Now, when it comes to assuring, specifically software, but in general, just any kind of system, there are three ways that you can go about it, right? One of them is that you can prove mathematically that it works
You can come up with a mathematical model of the system, an abstraction, and then prove properties about that abstraction. And hopefully, those properties will translate into the thing in the real world. So, if you prove that the system is safe in theory, then in practice it will be safe. Or if you prove that there is a problem, then in practice there will be that problem, you can find it, right? The problem is that coming up with those mathematical models, formalizing all of that, is really hard. And it's some of the methods that we use in formal in formal methods are computationally very expensive. So, those techniques only scale for Well, they don't really scale. They They only work for relatively small-sized problems. And when I say relatively, you have to consider the scope of a mission, the complexity of a space mission, right? Now, the second option you have, let's say that you cannot formally prove that the system always works
Okay, well, you can still test it, the way they've been doing for hundreds of years, right? The problem with testing, there there are really two problems with it. One of them is that just because you test something once and it works, doesn't mean that if you do the same thing again, it's going to work without further assurances and methods to to provide that determinism, there's no guarantee that just because you do something once it's going to behave the exact same way next time. And that's true for software and for hardware. The other problem with testing is that testing is only as good as how exhaustively you traverse the input space or the state space of the program. And that means if there's infinitely many possible tests, then no matter how hard you try, you will always get a fraction that is negligible compared to everything that could happen, right? So, the third option is, okay, well, if I cannot prove that it always works and I can test a meaningful meaningful amount of samples or I don't want to just rely on the tests. What I can do is I can monitor it. I can just install something that goes along the device at runtime and make sure that everything behaves as expected. And it could it could be monitoring the environment where it runs so that if there's a deviation from your expectations, you know, and it could also be monitoring the device itself to make sure that it behaves as it should
And that is known as runtime verification or runtime monitoring and these two terms are large largely interch- interchangeable. And the idea is that you just monitor a system at runtime and if something deviates from uh the nominal condition, then depending on the mission and the situation, you switch to maybe a backup unit, degrade performance, uh engage some sort of fault handling mechanism, uh there's an operator that comes and connects to the system and something else. Runtime verification doesn't concern itself with what you do when there is a problem. It's only about detecting the problem. And it's very important that we get it right. I always say that runtime verification is the last line of defense. Runtime verification is there to catch the things that you couldn't prove and you couldn't test for. Which means it's your last opportunity to catch whatever it may be wrong
If you stop a mission that was working fine because you implemented the monitors wrong, then it could be a lot of money or opportunities down the line just because you stopped something with a false negative. If you do the opposite and you say, you know, everything's okay when it isn't, then it could crash. So, you really want to get it right. And I work on two applications at for NASA that are used for runtime monitoring and they're Copilot and Ogma and I'm going to talk about those. And I'm going to tell you not just some technicalities of the language, but also how we um carry out software engineering activities and we do this in a very open way and hopefully some ideas that I want to pass on to other projects in the community. And just to give you a hint of what the talk is about, these projects are implemented in Haskell. Um, they go through a qualification process at NASA, which I'll talk a little bit about. And as I said, they're open source
So, Co-pilot. Co-pilot is a runtime verification language. And what it does is it allows you to specify the properties that you want to monitor. And when you compile a specification, out comes hard real-time C code or an FPA. And what I mean when I say hard real-time is that that code executes with predictable memory, constant memory, and constant time. There's no mallocs, there's no for loops, there's no recursion. We know exactly how long it'll take. And for the kinds of work that for the kind of work that we do, that's critical
And as I said, it's open source. It goes through a process known as NPR 7150 and you can find documentation online about the software engineering requirements that we follow and I'll show a couple of them later. And it's released every 2 months. And for me, that's actually paramount that we release every 2 months. And I don't mean almost every 2 months, I mean exactly every 2 months to the day. We've never been late. And you can find the project over there. And the And the idea that we've never been late is important for me because I want to send the right message to the community that this is open source that is reliable
And even though I cannot put a personal guarantee on it, I want people to get the message that this is we are a reliable team from the get-go. This is what a Co-pilot specification looks like. And there's been talks on streaming today, so this is another kind of streaming. The idea is that the information that you get from the vehicle or from the rover or from the from the robot. It's also used for robotics. And comes as a stream of data. An an infinite sequence of data. And it could be the the battery temperature, it could be the air speed of a of an aircraft, it could be the altitude or the GPS position
And it is just coming as a sequence of samples. And you take some of those streams, put them together, manipulate them in some way, and ultimately what you want to create is a stream of booleans. Where true means there's a violation and false means that everything's okay. And at the very top of that specification, you'll see that it says trigger heat off temp increasing fast and then some argument. And what that means is if the stream temp increasing fast becomes true at some point, then the heat off function will be executed. And that heat off function is responsible for dealing with that violation. And you see that, you know, you can subtract streams. You see the temp delta there is is the the subtraction of two streams
You can multiply them by numbers and that means just multiply every sample by that number. You can delay streams, putting samples before with that zero plus plus in past temp. That just means prepend the sample to a stream. And you can also get streams from the outside world. And that's the last one at the bottom that says external temperature. And that just means that's a given for us. We don't have to define it. It's going to be given by the the outside world by some other part of the system that where this is embedded
Now, when you compile that specification, out comes C code. And I'm not going to give you the C code. I'm just going to give you the header file. Now, the top two lines are the expectations. The things that you as the user of this module need to provide. The first one is the current value of the temperature. Every time that you need to check the status of the monitors, give me the temperature. The second one is the heat of function
It's how you will deal with the violation. You have to implement that function. In return, if you give us that, we'll give you the step function, which is the one that checks the monitors for you. And even though for that specification that you saw, the monitors are relatively simple, in real life monitors can be complicated and you don't want to get them wrong. Now, why do we use Haskell? And the the decision to use Haskell actually predates my arrival at NASA. I've been there for 6 years. But um I can tell you some of the advantages that I see in in using Haskell in these projects. The first one is that our code is declarative
Now, our language is a DSL, a domain-specific language embedded in Haskell. That means we don't need to write our own parser, type checker, type inference system. We just rely on Haskell's. So, what you see is valid copilot code, but it's also valid Haskell code. And we can leverage all the power of the language. And it allows us to write things in a declarative way. And what I mean by that is that the specifications tell us what they intend to do, not how they intend to do it. You won't see there anything This is implemented using a ring buffer
You have to keep at the position of the index to to know where you are in the ring buffer and so on. You won't see any of that here. In that specification, all you see is I'm going to have a stream of data and I subtract another stream of data and that's it. The code tells you exactly what it intends to do. Now, Haskell I How many people, out of curiosity, have used Haskell? I see 1 2 3 4 5. Okay, 6. So, Haskell is a functional language and it is statically typed. And if I had to pick one of those two features, I'd prefer that it be statically typed and strongly typed rather than functional, even though functional is is great
And that's because of the assurance that it gives us. So, um if we write we don't have to write the types of everything in our specifications, but if we write the types, then the the compiler is going to have an easier time helping us and we are going to declare what we mean by things in the types. And if we get a type wrong, the compiler at compile time is going to tell us you got the type wrong. That means we don't have to run the C code that comes out to realize that something was wrong. At compile time we already know that there's a whole class of errors that cannot happen in our specs. And that means in our monitors, and that means a whole class of errors that cannot happen in missions. And I I I always tell it this way, especially when you work with with um like if you don't have types in your functions, right? Then you have to test your functions for many possible outputs, how they handle if you pass the wrong thing and whatnot. So, every type you write is potentially an infinite number of tests that you don't have to
So, that's why it's important that we write the types. But Haskell has a very advanced type system. And what's cool about it is that it has dependent types, a limited version of dependent types. And what that means is that not only can you can you use types at the type level in the annotations, you can use literals at the type level. And you can extend your types with literals. For example, streams can carry arrays, can carry multiple values together in one sample. And the arrays have known length. And this is crucial for us because we want to generate C code with known memory bounds
So, we need to know how big the arrays are. And we can do this easily because the arrays, if you see that example at the bottom, it says array of two floats. Now, if have a variable with two floats and we try to assign it a value with three floats, the compiler is going to tell you that does not work because the length doesn't match. And the same is true if we try to access out of bounds. So, if we say we want to access the the fifth element of that stream of every element of that stream, the compiler is going to tell us at compile time that's not going to work. So, there's again a whole class of errors that we just eliminate by just using the language with types. And a few more things. Haskell is deterministic
In Haskell, if something has side effects, you have to say it. And if you don't say it, then it doesn't. And for us, that means in terms of testing that we can leverage really powerful techniques for uh randomized property-based testing. So, essentially, we have a huge battery of tests that we need to build to to qualify for the category where we are in terms of criticality for these projects. And what we say in the tests is not run this function with this particular input and check if the output is like this. We just say, "Well, this property should always be true. And here's a way to build random specifications. And here's a way to build random streams." And the testing system will start generating random specs and streams, putting them together, and running them, and comparing the specification that it generated with the expectation based on the denotational semantics of the language, which are given in the same test
And it tells us, "Is the language behaving according to the formal definition or not?" And it just tries hundreds, thousands of tests every single time. And we run this in every pull request. Now, there are challenges also to using Haskell. And if you've ever used it or if you used it especially recently, you'll know this. Um Haskell, even though it's been around for 30 years, I think 30 plus at this point, um, it's a changing ecosystem. It's constantly changing. Uh, even basic things like the installation tools change. And that has caused struggles in our team where somebody in the team that was in a geographically, uh, far location, remote location, couldn't get stuff installed on their machine and nobody was there to help them
And it took a few calls and a few weeks of coordinating, uh, with them to get things installed. Which is something that in a language that is stable, you wouldn't you wouldn't really expect that these things happened very often. Um, it's also a changing language. Somehow one thing that has happened with the language is that there used to be a standard and in the last few years the language is whatever the compiler supports. And in our case, for example, there's a public definition in the API that we now need to remove because there's a new keyword in the language being introduced, but it's not a new version of the language. It's a new version of the compiler. Right? And also there's a public perception. We've heard, uh, people say in aerospace companies, like, "I can't deal I can't teach my engineers Haskell
We don't want them to learn Haskell. We want them to learn Co-pilot, which is a much smaller language. But there's a public perception that Haskell is a language that is difficult, mathematical, and so on. So to combat that, we came up with this other tool and it's Augma. And Augma is just a translator. So what Augma does is Augma is like Co-pilot on steroids. Just makes it easier to use. So Augma takes a high-level spec, which could be in Co-pilot, but it could be many other languages that we support, and it gives you the monitoring application
So instead of having to define the temperature and the handler, and then, uh, call the step function, it kind of tries to make it easier for you to integrate all of this into your actual target platform. And we support a bunch. Um there's apart from the standalone C module at the top, we can also give you code that is ready to run on NASA's Core Flight System. And NASA NASA's Core Flight System is um a software framework that is open source as well. And uh is used in many many applications. And there's a version of CFS that is certified to fly I think in the highest category of criticality at NASA. Don't quote me on that, but I think that's is somewhere along that. Um we also generate uh monitoring applications ready to run in the Robot Operating System
So, if you're doing robotics, then you can get the monitoring problem out of the way with a simple Haskell spec. And we also generate code for F' Prime. And F' Prime is the software framework used in the Mars helicopter. We we didn't participate in that mission, but it's the same software framework. And um it it's all from the same spec. It's all from the same source. We try to automate the whole process. And again, this is a Haskell application and it's a compiler really
And that's why Haskell is such a great choice. And like the other one, it's open source, it goes through a certification process, and is released every 2 months, and is available on NASA's GitHub. Now, the the reason why we can do this easily is because these uh software platforms that we are targeting are um component-based platforms where people just implement a bunch of modular components that deal maybe with the camera or with the vision or with the planning or with scheduling, and then connect them in some way either through a software bus or through ports. In the case of F' Prime, they just have ports like cute, and you just connect the ports. And in the case of CFS and ROS, you have a software bus, and then you publish to the software bus, and subscribe. This publish subscribe. And what Ogma does is it generates one more unit at the same level as everything else. And that unit knows how to get the data for you, and how to publish the results of the violations
And it gets the data based on the name. So, if you say temperature, there's a database that knows, "Ah, the temperature is coming in this particular part of the software bus with this message, and it has this type, so I know how to get it." So, you just have to write the requirement, the property with temperature in the name, and it knows how to how to deal with it, and how to get it for you every single time there's a new message with a new temperature, a new air speed, it will take the value, put it in the global variable, re-evaluate the monitors, and if there's a violation, publish it back in the software bus. So, it just eliminates the whole problem for you. And even though the software that we are checking at this point is C++ and Python, which is what CFS Well, CFS is nor- is is mostly done in C, I believe. Um C++ and Python normally used in ROS, and I think F' is also C++. Um even though we're checking languages that are not They don't have the same guarantees as Haskell, uh we can leverage the same ideas, and we we give you, for example, an interactive testing system that will feed random inputs to your flight application or robotics application. And if there's a violation, publish the results so that you can replicate it. And I don't know if you can see Is the video playing? Yeah
So, this is kind of what it looks like for a particular simulation. This is neither ROS nor CFS, but we just pick a simple property, hit a button, and out comes code that monitors the property, which in this case was that the air speed of the of the plane shouldn't drop for too long. And if the air speed drops, then you see the little red um icon next to the mouse, and that indicates a violation. Thank you. Thank you. And that that process is kind of automated, right? The The going from the property that you write in Copilot to something you can fully integrate is automated. Now, these tools go through a qualification process and I'm not going to give you all of the details, but I want to give you a hint because you are doing things related to this probably. NASA has a guide of software engineering requirements
It's called the NPR 7150. Projects are classified based on criticality. We are a a class D. Uh classes go E to A with A being the highest criticality. And it's a long extensive list. And this is one example of a of a requirement. Requirements are high-level. They don't tell you specifically the tools you have to use or specifically how to do it
It's kind of a bit up to you. You just have to convince some some evaluator that you're doing it right. But this is one that you're probably doing, which is the project manager shall track and evaluate changes to software products. I'm going to show you how you how we do it and then it it will probably be similar to some of the things you see in the wild. What we do, if you go to a repository, is that every single commit references the issue it's trying to address. And we never ever ever commit without referencing the issue and we never mix things. So, if you go to if if as part of an issue you have to fix a bug and you realize that somewhere in the module there's a typo in a comment, that's not the same thing. So, you open a separate issue and you deal with it separately
And um we never cross branches. We never uh we we never deal with the same with different issues in the same branch. We just deal with one issue and close it. And the way that it looks like if you go to repo is that we have a an official template for the change request that just describes what the problem is and ideally how to replicate it. And then it goes through a series of steps from initiated, which just means it's been formally filed, through scheduled, which means we're going to do something about it and we have a person assigned to it and we know the release it's coming out, and to close, which means the work is done and it's fully integrated. And we just leverage what is available on GitHub to do this. So, even though GitHub is not an open source project, we leverage the same technology that everybody's using for their open source work, which in this case it's just GitHub and Travis and so on. And um we start changing the labels to indicate how the the issue progresses all the way to termination
And at the end, uh with the pull request, there's an evaluation and a couple of things that again, not open source, but is a kind of technology that we've been we've embraced in the open source community. We have a pointer to a Travis log that shows that everything built correctly, including the tests that I was talking about before, and also a Docker image that shows that the the bug was present before the merge and absent after. And it's just a little bit of extra work that allows you to deliver the kind of reliability that we're looking for. Again, this is our method, Copilot and Nogma is not for everybody. Now, this is just a glimpse of what we use Haskell and the tools that we use, but there's a lot more that we are leveraging and I'm hoping there's also a lot more that we can share and hopefully that the community can use even if it's not at the depth and and with the rigorousity that NASA will will use it in a in a lighter way. So, our documentation is built in markdown. And this is the documentation that we have to file to auditors to get the thumbs up for software to be released at the criticality that we want. And markdown uh we use Pandoc, which is a again a Haskell coincidentally is a Haskell tool, but there's there's that's just the way that it was
It's a tool that will transform the markdown into a PDF and it produces a beautiful result. It gives us everything exactly the way that we have to file it internally. We have to adapt the template, of course, but it gives us everything we need. And that means we don't have to to work with binary files anymore. We can again use all the techniques and all the tools that we use in the open source community to keep track of things. For example, we we manage the files internally using GitLab and again we can keep track of all the changes and sure that there are no accidental modifications to the binary files and so on. Now, I'm not expecting you guys to go through something like that for your own projects. It's a lot of work and for many open source projects is not really justified
But what we're trying to do is we're trying to make it easier not just for other open source projects, but not not just for other NASA projects, but also in general for open source projects to adopt some of these techniques. And the thinking here is if we make it so easy to do the right thing, you're probably just pick it up because it's just so cheap to adopt. Thank you. So, we're doing this in two ways. The first one is we're producing bash scripts that you can use in your pull requests as part of the CI jobs that check whether you can merge those changes or not or whether they pass the test. We're using we're developing bash scripts that will check for compliance with basic rules like for example, that you always reference the change that you're working on. And ideally this should be easily adoptable. Currently, I'm doing this working with the Space ROS project, which I'm a part of, which is a version of the Robot Operating System that is geared towards space applications
And the idea is that they will implement some lightweight version of our process that is easier for the open source community to accept, but at the same time goes a long way at given as the reliability that we want to see in these kinds of applications. And by making it so easy to adopt, it's just a bash script, you put it in the in the CI job and then configure it, then hopefully a lot more people will will embrace better software engineering techniques in their work. And the other thing that we're doing is we're building a tool that analyzes your repo and tells you whether you're compliant with your process and also a little bit of information about the risk that you're taking. So you probably have seen a lot of abandoned work in your life, software projects that kind of die because, you know, the the the developer has something else, something happens in their life, they get a job and they have to to quit the project. And what these tools tell us is, for example, that there are certain people that are responsible for some modules and no one else knows how they work. Or that there's a lot of people there's a couple of people taking on most of the issues and no one else is doing as much. And that's a risk for you. Like, that's me
What that graph tells you is that I was working on all of the blue issues and there was a colleague working on the other blue at the bottom and every every other black dot in that area of the graph was a developer that was working maybe on one or two or three issues, which means if I leave, that project is at risk. But what that means now for us is that we can enforce rotation in the project. We can say, "No, actually, you're going to start working on that module, which you don't know, so that you do know it." And that way, if I leave, you know how to work with it. So, having these tools that analyze all our data from the Git repo and from GitHub, they just read the comments, they read the events, allow us to make better science-based decisions about how we manage these projects, and hopefully make sure that they don't become abandonware. And a couple more things about how we embrace open source. The first one is that we're trying to make all of these tools available on standard distributions. And that actually takes a bit of effort because NASA uses historically has used the NOSA license, and Ogma uses the NOSA license, and that license is not considered free I think by the Free Software Foundation, which means Ogma cannot get into Debian. So, now we need to talk with the lawyers to change the license so that it can get into Debian
But, CoPilot is already in Debian and Ubuntu, and we're trying to get it in Fedora. So, that people can install these tools without having to deal with all the installation issues that I talked about before. And we're looking for contributors. And what I mean by that is not just people that will commit to the project or send pull requests or bug fixes, but also people who will use it. We've seen people use CoPilot to build um ventilator machines. And we've seen people use CoPilot to build um connections with Arduino and Zephyr. Like, it's a language for stream processing, really. So, you can use it for a lot of things
And I would love to see you guys do stuff with CoPilot on your own. It doesn't have to be related to aerospace. It can be related to anything else. So, anything that you really related to this, it could be a paper, it could be an extension, it could be a project is more than welcome, and I would love to hear about it. And if you want to know more about the projects, again, those are the URLs, and you can jump in. And you can witness first-hand the software engineering process that we are I was talking about earlier. So, uh the main takeaways are, of course, that we developed these tools for runtime monitoring. Um that Haskell is an extremely useful asset that gives us advantages that no other language can give us
And that um is not just about doing the right thing. It's about showing easily that we are doing the right thing. So, we're building these tools to make software engineering not just a must, but an easy to audit task. And final but foremost is that open source and openness about this process is paramount to what we do. It's It's uh it's crucially important, especially for me. So, I want to be very open about how we develop this project so that perhaps the community can have a conversation that is long overdue about not just getting the software to do the right thing, but also getting the projects to be managed what right. Right. And with that, thank you all for your attention and I think we're a little bit over time, so probably I'll have to go upstairs if you have any questions
Thanks, everyone.