Timeline for An example of something you can formally verify with proofs in Software Development
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 24, 2018 at 15:30 | history | edited | xuq01 | CC BY-SA 4.0 |
added 284 characters in body
|
| Jun 24, 2018 at 6:53 | comment | added | Basile Starynkevitch | I don't know for sure how current aircrafts coming out from Airbus factories in june 2018 have their software compiled (today), and the Airbus folks knowing that exactly are not allowed to tell all the details. But a year ago, I was explained that upgrading the compilation process -for the code inside Airbus- is a lot of hassle. It is not as simple as some engineer coming in the factory and saying please put the file on that USB key as the flight control firmware.... There are lots of (social) procedures involved (and lot of red tape paper work). | |
| Jun 24, 2018 at 6:42 | comment | added | xuq01 | @BasileStarynkevitch Thanks. I'll update my answer accordingly when I get back. | |
| Jun 24, 2018 at 6:17 | comment | added | Basile Starynkevitch | Compcert is indeed used on aviation software, but that does not means that the corresponding binary (produced by Compcert) is used today in commercial flights. You can't imagine how bureaucratic and conservative the aircraft industry is (for excellent reasons, most of the time). Even the software tools in actual use have to be somehow "certified" : the guy coding Airbus critical software is not allowed to switch from some GCC 3.4 to some Compcert compiler without a lot of written authorisations (and the whole certification process takes years!) | |
| Jun 24, 2018 at 6:12 | comment | added | xuq01 | @BasileStarynkevitch TBH I am not sure. Of course I have seen their paper on using CompCert for aviation stuff, but I do not know Xavier Leroy personally and have not talked to him about anything like that. But I would trust what he said personally... | |
| Jun 24, 2018 at 4:59 | comment | added | Basile Starynkevitch | Are you so sure that Airbus is really using -in june 2018- Compcert to compile production safety critical code. Last time I asked Xavier Leroy about that, he told me that it is not yet the case... and Airbus is still considering changing its production compiler to Compcert. For Airbus, changing its toolset requires a lot of (administrative) work (notably convincing the regulating authorities) that might take years. In real life the civilian aircraft industry is very conservative. | |
| Jun 23, 2018 at 22:00 | vote | accept | Lance Pollard | ||
| Jun 29, 2018 at 3:27 | |||||
| Jun 23, 2018 at 18:00 | history | answered | xuq01 | CC BY-SA 4.0 |