3 ms·

Do you take the plane much? The overwhelming majority of these systems are verified using rigorous but non-formal methods (tests and code reviews). An applicat

Do you take the plane much? The overwhelming majority of these systems are verified using rigorous but non-formal methods (tests and code reviews). An application of formal methods here or there is so exceptional that it's publication-worthy (for instance http://www.springerlink.com/content/h33p602vh34634v8/ http://www.springerlink.com/content/h33p602vh34634v8/ ). The currently applicable standard (that has been applied in the design of all the planes you have taken), DO-178B, does not even mention formal methods, so that when you want to apply them in substitution to the rigorous mandatory process (instead of just applying them in addition to it and doubling your costs wrt your competitors), you need lengthy explanations. Things are changing, but they are changing slowly (I think you want this culture to be conservative, in fact). The next revision of the aforementioned standard will mention formal methods (but certainly not make them mandatory).

Craiggybear 15y ago
Things have indeed changed, then. I used to write software destined for avionics (assembler stuff in the 80s) and that was required to apply formal considerations. I think that conservatism in certain avenues of software implementation is essential and one can't even truly be considered an engineer (or software engineer, whatever that currently means) without exposure to formal discipline. Edit: I've never considered myself to be an engineer of any kind nor have I claimed to be one.
- arethuza 15y ago
  Out of interest, what formal methods were used then? I remember there being some CPU designs in the 80's (e.g. VIPER) that had been formally verified but that all seemed to die out in the 90s.
  - Craiggybear 15y ago
    Good point -- VIPER isn't essential and one could argue that an assembler of any kind isn't guaranteed to give rise to totally engineering quality results (ADA and Eiffel were probably better for that at the time) but there were things like VDM, Z notation, ASM's, etc, BNF and Model Checking approaches.
    - pascal_cuoq 15y ago
      Thanks for taking the time to provide your point of view. My initial comment was harsher than it should have been. I have no excuse, but if I had one, it would be that I see many academics in the field of formal methods act and speak as if these were used everywhere they could be useful, which is vexing when one's job is precisely of doing what is necessary to transfer them. The Z notation / B method community is still strong (though they seem a bit defensive when met at conferences). I only know about VDM because some of the syntax in Caveat is inspired from it (Caveat is the tool whose application is described in the link I provided. It was developed at the lab I work at, but before I was hired). Just in case, here is what we are now working on. One description is "successor to Caveat", but it's more than that. For one thing, it's Open Source (type "apt-get frama-c" or equivalent in most Linux distributions). It allows to combine techniques that range from static analysis to formal verification of functional properties using Hoare logic: http://frama-c.com/try_out.html http://frama-c.com/try_out.html (automatic analyses) http://frama-c.com/jessie/jessie-tutorial.pdf http://frama-c.com/jessie/jessie-tutorial.pdf (verification based on Hoare logic)
      - Craiggybear 15y ago
        You are welcome. I found your comments very interesting. Not harsh at all. Many thanks for the additional links above. I found them well worthwhile reading.

Craiggybear 15y ago

Things have indeed changed, then. I used to write software destined for avionics (assembler stuff in the 80s) and that was required to apply formal considerations. I think that conservatism in certain avenues of software implementation is essential and one can't even truly be considered an engineer (or software engineer, whatever that currently means) without exposure to formal discipline. Edit: I've never considered myself to be an engineer of any kind nor have I claimed to be one.

arethuza 15y ago
Out of interest, what formal methods were used then? I remember there being some CPU designs in the 80's (e.g. VIPER) that had been formally verified but that all seemed to die out in the 90s.
- Craiggybear 15y ago
  Good point -- VIPER isn't essential and one could argue that an assembler of any kind isn't guaranteed to give rise to totally engineering quality results (ADA and Eiffel were probably better for that at the time) but there were things like VDM, Z notation, ASM's, etc, BNF and Model Checking approaches.
  - pascal_cuoq 15y ago
    Thanks for taking the time to provide your point of view. My initial comment was harsher than it should have been. I have no excuse, but if I had one, it would be that I see many academics in the field of formal methods act and speak as if these were used everywhere they could be useful, which is vexing when one's job is precisely of doing what is necessary to transfer them. The Z notation / B method community is still strong (though they seem a bit defensive when met at conferences). I only know about VDM because some of the syntax in Caveat is inspired from it (Caveat is the tool whose application is described in the link I provided. It was developed at the lab I work at, but before I was hired). Just in case, here is what we are now working on. One description is "successor to Caveat", but it's more than that. For one thing, it's Open Source (type "apt-get frama-c" or equivalent in most Linux distributions). It allows to combine techniques that range from static analysis to formal verification of functional properties using Hoare logic: http://frama-c.com/try_out.html http://frama-c.com/try_out.html (automatic analyses) http://frama-c.com/jessie/jessie-tutorial.pdf http://frama-c.com/jessie/jessie-tutorial.pdf (verification based on Hoare logic)
    - Craiggybear 15y ago
      You are welcome. I found your comments very interesting. Not harsh at all. Many thanks for the additional links above. I found them well worthwhile reading.