ExoMars - Schiaparelli landing Options

[Phil Stooke]

Starting a new topic here - hopefully that's OK! Clearly there will be a lot of action around this in the next weeks and months with descent images and HiRISE views of the hardware.

I thought I had posted this map earlier but apparently not. This shows the various landing ellipses in this area. The original plan was for an ellipse oriented NW-SE, but it changed with the different launch date and is now nearly E-W. Note that the ellipse shown in the recent ESA release is the envelope of all ellipses over a given launch period, but the actual landing ellipse for the given launch date is smaller. Opportunity's final landing ellipse is shown for comparison.

http://exploration.esa.int/mars/57445-exom...6-landing-site/

http://exploration.esa.int/mars/57446-exom...6-landing-site/

Phil

[Gerald]

Those event-triggered multi-threading systems are very hard to test and debug.
There may have been set a timer, which triggers the thruster shut-down if some event hasn't occurred within this time. If, for example the velocitiy variable is initialized with zero, and adjusted by the radar after an assumed time, a delayed setting of the variable may return standstill, although the variable simply hasn't been set. This could be resolved to some degree by adding an invalid flag. But how should the system behave in case of an invalid variable? Default would still be thrusters off, since waiting too long near ground with thrusters on would prevent a landing, and thrusters on during flight would be wrong, too.
There are certainly thousands of possible errors of this kind you don't see in a fixed set of simulations. With the actual data, they can now set-up a new series of unit tests to get closer to real conditions near Mars. And once the error is nailed down, some will certainly say, that this could have been known before. But before the real-world test, finding a needle in a haystack is much easier.
I'm wondering now, whether another test with a low-cost lander should be performed, or if the expensive payload should be risked without a prior fully accomplished landing test.

[mcaplinger]

Those event-triggered multi-threading systems are very hard to test and debug.

A sensible designer would never use such a structure for a flight control application. There have been well-understood flight control algorithms in use for almost 50 years that can be tested. Note that Viking landed on Mars with a very simple computer the very first time. http://history.nasa.gov/computers/Ch5-6.html

[JRehling]

Just to clarify on the question of proving computer program correctness…

In the study of formal program verification, one seeks a mathematical-style proof that a program will correctly meet the formal requirements that are defined. This is, as was noted, quite hard to do for complex systems. Moreover, a program that is proven correct may be part of a failing system because the formal requirements are not an accurate statement of the real world application. For example, an airplane autopilot program that assumed that winds are always under 10km/hour might be proven logically correct, but lead to immediate failure because the real world has winds higher than that.

I doubt if any spacecraft failures take place because an algorithm could have been proven correct in the above sense, but the effort to prove it was not made or was not tractable in a computational sense. It's far more likely that ignorance, oversight, or negligence would arise in defining the formal requirements or – more likely still – the notion of proving an algorithm correct in the formal sense was never part of the development process in the first place, for the very good reason that it's usually not tractable for complex systems.

Formal program verification, as the literature defines it, is not a part of any software development process that I've been around. I'd liken it to a doctor trying to use the periodic table of elements to diagnose a patient's illness. Technically, an illness pertains to how your atoms are arranged, but that's not a useful level of description for a sick person, in most cases.

For example, the two problems that afflicted the Cassini-Huygens relay: (1) The Doppler shift in radio frequency because of the relative velocity of Cassini and Huygens during the mission was not put into the formal requirements. Moreover, empirical testing that would have revealed this would have been unthinkable. The algorithm was absolutely correct – assuming that Cassini and Huygens were not moving very fast. The fact of their high relative velocity during the mission was simply excluded from the design phase, but fortunately this oversight was caught before arrival at Saturn. (2) The software that was supposed to turn on radio receivers listening to two partially-redundant radio channels did not turn on one of the two receivers, which meant that Cassini transmitted it in vain, and half of the images that it took were never received, and lost forever. Here, I'm not sure that enough information was released to the public for us to say exactly what went wrong. It becomes a bit arbitrary as to whether the algorithm was correct, but the specifications written incorrectly, or if the specifications were written correctly but the algorithm was not proven correct. My sense is that the paradigm of logical program verification is probably not a good description of their development process, but that may not be public information.

[mcaplinger]

Formal program verification, as the literature defines it, is not a part of any software development process that I've been around.

I have a PhD in computer science and I develop flight software for a living (among other things) and I use whatever tools I can, including formal correctness. But I guess I'd agree that it's not common.

The software that was supposed to turn on radio receivers listening to two partially-redundant radio channels did not turn on one of the two receivers...

My understanding is that this was user error (miscommanding) rather than a software failure per se.

Software can be complex, and the simpler it is, the more likely it is to be right. Landing on Mars should not be that hard from a software perspective.