Peter wrote:
Software whose complexity is above the “totally trivial” level cannot be formally proved to be bug-free.
Actually, using formal methods they can. With respect to some specific requirements specifications, of course.
One of the best known examples is the automated control system for the driverless Paris Metro line 14. It opened in 1996 and when I spoke to one of the developers in 2009, they were still running the original version of the software.
what_next wrote:
Get rid of the crew ASAP and accidents like this one will be history.
Yes, like that one. What about all the others?
One of the best known examples is the automated control system for the driverless Paris Metro line 14. It opened in 1996 and when I spoke to one of the developers in 2009, they were still running the original version of the software.
In the 1980s I wrote masses of software (about 10cm thickness of a paper listing) in Z80/Z180/Z280 assembler, and no customer ever found a bug in any of the products. Tens of thousands were sold.
But the most complex code size was about 50k bytes. In hand crafted assembler this is probably comparable in complexity to a GNS430.
Formal methods do not work for nontrivial projects. Absolutely not. No way. Well, they can be applied but they don’t result in zero bugs. Look at the B787 which will get a stoppage of both engines after several hundred days of on time. I bet formal methods were used there.
Peter wrote:
Look at the B787 which will get a stoppage of both engines after several hundred days of on time. I bet formal methods were used there.
This is an often quoted example which has zero relevance in real life. An overflow which occurs after 3 years of continuous operation of an engine whose fuel supply only lasts 14 hours is really not going to ever occur. I still wonder how they found out about that bug.
Martin wrote:
But smaller aircraft would have worse fuel economy. Also, you’d have more airframes and engines to maintain.
Yes, but at some point the logics of hubs makes no sense anymore. Travelling 2-3 times the needed distance, using 4-6 times the hours, is no recipe for good fuel economy and less maintenance costs. It’s certainly a waste of crew time, and cost.
Peter wrote:
Formal methods do not work for nontrivial projects. Absolutely not. No way.
Météor (Paris metro 14) was 86 kLOC. We can argue if that is “trivial” or not. And that was 20 years ago.
Well, they can be applied but they don’t result in zero bugs. Look at the B787 which will get a stoppage of both engines after several hundred days of on time. I bet formal methods were used there.
As I wrote, zero bugs with respect to a specific requirements specification…
This is an often quoted example which has zero relevance in real life. An overflow which occurs after 3 years of continuous operation of an engine whose fuel supply only lasts 14 hours is really not going to ever occur. I still wonder how they found out about that bug.
I don’t know but probably the issue is that the “ECU” doesn’t get powered down when the plane is at the gate.
what_next wrote:
This is an often quoted example which has zero relevance in real life. An overflow which occurs after 3 years of continuous operation of an engine whose fuel supply only lasts 14 hours is really not going to ever occur
I think the big issue was that the engine never gets truly powered down completely unless you physically open the thing up and disconnect the power supply by hand. Like so many devices, it might look off but there’s still a computer powered up in standby mode inside of it.
I’m not a software guru, but clearly we are not talking about traditional if-then-else software logic….we surely are taking about AI where the machine has the ability to assimilate masses of information and make the best decision based on (probabilistic) heuristics….ie like a human brain except many orders of magnitude faster and more thorough in assessment of the options…
LeSving wrote:
Google maps will find the fastest route in no time, and it will change it continuously in real-time based on traffic information received from other units.
That’s actually a great example how this does NOT work. I use Uber and Lyft (ride-sharing systems) all the time and the drivers tend to use either Google maps or Waze (the one that updates in real time). You know what? I can beat Waze any time navigating through L.A. and Google maps very often. Why? Because I know the place and know where shortcuts make sense and where they don’t. Waze in particular has a stupid tendency to send you down little side streets that are too narrow for two cars to pass (yes, there are plenty of those in L.A.!) and you end up losing huge amounts of time, not to mention a very unpleasant driving / riding experience. I image some wizz kid in Palo Alto thinks that’s all a great idea. Just that it isn’t. You want that kind of software to run airliners? Be my guest, I’ll watch you from the ground (or from my steam-driven Cessna, even better).
With ships, the problem is getting enough crew to stay for weeks isolated on a ship. This has lead to faster and larger (cargo) ships, when the most economical and most efficient would be smaller and slower ships, and more of them. Going from 16 to 11 knots will reduce fuel cost by 50% . I have no idea if this is transferable to aviation, but there seem to be a tendency of increased “hubbing” and less direct routes, which is very inefficient for travelers (you use a total of 4-6 h or more for a trip that could take 1-2 h). A direct route would not be economically viable due to too few passengers on each flight. Autonomous, smaller and slower aircraft would offset this, when there is no crew cost.
Sorry, both of these assertions are pure nonsense. Ships already run at optimum speed (where possible) and the general direction in air travel is away from hubs and to more direct routes. Witness the success of the airliners made for that (777, 787, 330, 350) and the disaster of the A380 that was made for hub and spoke systems. Aside from EK everyone is moving away from the hub system wherever possible. Boeing foresaw that and decided not to pursue a double-decker 747 (the 747-8 sells reasonably well as freighter, not as pax aircraft), whereas Airbus decided they needed to sink some billions into a prestige four-holer. Which is dying.
