236 – Space Flight Software
| Rate/Vote |   (average: 4.39) Loading... |
Guest: Maria Hernek Host: Markus Voelter Shownoter: Markus Voelter
Last fall I visited ESTEC, ESA’s space research and technology center. In this first of three episodes, I talk with Maria Hernek, who heads the Flight Software Systems section. We talk about the challenges of space flight software, the development processes used by ESA and its vendors, as well as means of ensuring the required quality attributes. This episode can be seen as a continuation of the conversation with Andreas Wortmann in the OHB episode.
Introduction Maria and Departments
00:02:40Maria Hernek | Flight Software Section | Telecom Satellites | Navigation Satellites | Deep Space Missions | Galileo | EGNOS | Work Share with Vendors | Systems Engineering vs. Software Engineering
Development Process and Standards
00:08:20Agile | Incremental Development | Scrum | Agile vs. Contracting | Assembly, Integration and Test | Assembly, Integration and Verification | Risk Management | ECSS Standard | Coding Guidelines | ECSS E40 | ECSS Q80 | Verification vs. Validation | Redundancy | Runtime Monitoring | Engineering Handbook | Java
Systems Engineering and High-Level Structure
00:19:40Data Handling | AOCS System | GPS | Star Tracker | Central Data Management Unit | Rosetta Mission | Leon Processor | EOC 32 Processor | Sparc Instruction Set | Radiation Hardening | System-on-a-Chip | VHDL | ASIC | Redundancy | Hot/Cold Redundancy | CRC Checking | Reconfiguration Module | Watchdog | Single point of failure | Cross coupling | Design Drivers
Software Architecture, Communication and Operating System
00:33:27Simulink | AOCS Mode | Telemetry | C | Instrument Software | Data Compression | Geostationary | On-Board Software | CAN Bus | Mil Std 1553 Bus | Deterministic Bus | System Integration | Bandwidth | Spacewire | TTCAN | Task | Deadline | Realtime Software | Multitasking | Non-Determinism | Cyclic Scheduler | Preemptive Scheduler | ARTEMS | Task Scheduling | Process Isolation | Inter Process Communication | VxWorks | QNX | Ada
Timing and other Analyses
00:53:46Worst-case execution time | Interrupt Routine | Hierarchical Analysis | Prototyping | Bus Load Analysis | Runtime Monitoring | Utilization | Graceful Degradation | Safe Mode | Fail Safe | Fail Operational | Kopernikus Satellite
Testing and Verification
01:06:24Unit Testing | Integration Testing | Test Coverage | Hardware in the loop testing | Non-Functional Properties | Formal Verification | mbeddr Project | Design-by-Contract | CBMC | DeepSpec project | Benjamin Pierce | Hypervisor
Tools, Languages, Qualification and Interfaces
01:16:52Simulink | UML | Grady Booch | Layers Pattern | Driver | Ada | C | gcc | Scade | Tool Qualification | Interface Control Documents | Telecommand | MISRA-C | ASIL Levels | ATV
This website uses cookies to improve your experience. We'll assume you're ok with this.
Diese Webseite verwendet Cookies. Wir gehen davon aus, dass das für Sie/Dich in Ordnung ist.
This was an interesting episode with some questions remaining. First, the argument against C++ (“there is no compiler”) seems to be implausible. GCC for a long time has been the Gnu Compiler Collection and includes a C++ compiler on all platforms I am aware of. There are plenty of reasons against C++, of course, with good taste usually being sufficient. ;-).
Secondly, when using formal methods for verification, a certified compiler/toolchain is important. Testing can be done on the final binary, but I’m not aware of any serious approach to prove a binary correct – all tools I know work on the source code level. There is a certified C compiler around, namely the CompCert C compiler, which supports nearly all of ANSI C, and fully supports MISRA-C. The compiler has been verified in Coq, and the project is at http://compcert.inria.fr/.
Re C++: there might not be a compiler for their special space-qualified, rad hardened processors.
Re Verification: You can “proof” a binary correct by running a generated, high-coverage test suite. Regarding proofing and CompCert, you might be interested to hear that an episode on exactly this topic, with Benjamin Pierce as a guest, is coming up. Currently being shownoted :-)
Well, Maria told us that they are using GCC, and I don’t think there is a platform that has GCC where GCC does not support both C and C++ – especially since C++ is now being used in GCC itself, and it has been self-hosting for a long long long time.
As for proving correctness by testing: Yes, you can do that. But for it to be a proof, you need to consider all input/output pairs (or, in the case of continuously running software, all possible sequences of input and matching behaviour). That requires very patient customers ;-).
I’m looking forward to the CompCert episode!
Re C++: I take your point. On the other hand, I do hear in any places that C++ is not used, for various reasons. There must be something to it.
Re Verification: The episode is not specifically about CompCert. And the problem with a certified tool chain is that of course it does not solve the problems of errors in the sources/functionality. So you still have to test, or verify that part, right?
Well, if you can trust your compiler, a proof that the source code implements the specification carries over to the binary. But yes, you still must do the original proof. And, of course, you cannot always exclude bugs in the specification, to begin with. So I definitely think testing is valuable, and indeed necessary. To quote Knuth: “Beware of bugs in the above code; I have only proved it correct, not tried it.” ;-)
But formal methods can very well handle corner cases, or ensure general properties (not NULL dereference, guaranteed termination, …). And they force people to be explicit about their requirements, which often is the most useful part.
I agree with all you say, but both rely on the user writing formal specifications of their programs. The kinds of users I deal with simply will not do this. In mbeddr, we had integrated pre- and postconditions on interfaces, plus checking at runtime or statically using CBMC. Even competent developers didn’t use it. So the notion of “forcing” developers to make their requirements explicit is a wish, not a reality.
Great episode! With a lot of verve Maria explained the technical process aspects of space software development. I enjoyed her competent architecture insights, her process expertise and the aspects of more modern technologies and process aspects (e.g. agile). 5 stars.
On the use of Ada compared to C: “Is it (Ada) very good for low level hardware programming? Probably No.”
Admittedly, I haven’t done low level hardware stuff in C, so I can’t compare. But if this statement would be true, Ada would have missed one of its major language design goals! In my experience, it works very well.
I guess a more differentiated statement would be: Ada is good at realtime embedded applications. But C is better at low level memory stuff, because it performs fewer (no) checks.