4 ms·

It would be interesting to see what the actual error in the NIC firmware source was. This invalidates my assumption that a shop like Intel probably uses formal

It would be interesting to see what the actual error in the NIC firmware source was. This invalidates my assumption that a shop like Intel probably uses formal verification in firmware development. Its also scary to consider how many very important (nuclear/damn control, etc) systems while themselves might be formally verified are dependent on services of lower level software (OS, drivers) and hardware (firmware) that are not...

fnordfnordfnord 14y ago
Dam control, or damn control? I teach a control systems course, so I know about both kinds. PS You should be very frightened. The industrial control systems industry are slow to adopt new tech/new best practices/anything else new; and even more reticent to touch anything that "works." Tons of vulnerable equipment controlling dangerous things with default passwords (if any at all). I could go on for days.
- kevinherron 14y ago
  Too true... (I work at a SCADA/HMI software company :)
- voidlogic 14y ago
  Sorry typo :(
- pnathan 14y ago
  Absolutely utterly true. (I work at a SCADA-ish vendor).
Joeri 14y ago
Isn't formal verification the unicorn of software development? I know it's rumored to exist, and you will find it in academia, but I've never come across it 'in the wild'.
- voidlogic 14y ago
  It is out there: http://en.wikipedia.org/wiki/Formal_verification#Industry_use http://en.wikipedia.org/wiki/Formal_verification#Industry_us... In the wild what is more common in my experience is to use a formal specification language like Z or Object-Z and then recreate the the program in a "normal" language using pair programmers and/or extensive code review to attempt to ensure it conforms to the specification. While not perfect, for critical things this approach is far more time consuming and less bug prone than typical development. I have also seen limited attempts at writing code generators that take Object-Z specifications as input. My understanding is that this is an area of ongoing research, but even a program that generates code for a subset of a Object-Z specification can save a lot of time. Example research: http://www.jot.fm/issues/issue_2008_11/article6.pdf http://www.jot.fm/issues/issue_2008_11/article6.pdf

fnordfnordfnord 14y ago

Dam control, or damn control? I teach a control systems course, so I know about both kinds. PS You should be very frightened. The industrial control systems industry are slow to adopt new tech/new best practices/anything else new; and even more reticent to touch anything that "works." Tons of vulnerable equipment controlling dangerous things with default passwords (if any at all). I could go on for days.

kevinherron 14y ago
Too true... (I work at a SCADA/HMI software company :)
voidlogic 14y ago
Sorry typo :(
pnathan 14y ago
Absolutely utterly true. (I work at a SCADA-ish vendor).

Joeri 14y ago

Isn't formal verification the unicorn of software development? I know it's rumored to exist, and you will find it in academia, but I've never come across it 'in the wild'.

voidlogic 14y ago
It is out there: http://en.wikipedia.org/wiki/Formal_verification#Industry_use http://en.wikipedia.org/wiki/Formal_verification#Industry_us... In the wild what is more common in my experience is to use a formal specification language like Z or Object-Z and then recreate the the program in a "normal" language using pair programmers and/or extensive code review to attempt to ensure it conforms to the specification. While not perfect, for critical things this approach is far more time consuming and less bug prone than typical development. I have also seen limited attempts at writing code generators that take Object-Z specifications as input. My understanding is that this is an area of ongoing research, but even a program that generates code for a subset of a Object-Z specification can save a lot of time. Example research: http://www.jot.fm/issues/issue_2008_11/article6.pdf http://www.jot.fm/issues/issue_2008_11/article6.pdf