5 ms·
"It is well-known in our community that there is no scientific, firm way of actually completely verifying and validating software". Mr Rizzoni, "expert in fail
by Entlin 17y ago
"It is well-known in our community that there is no scientific, firm way of actually completely verifying and validating software".
Mr Rizzoni, "expert in failure analysis" must have never heard of Ada before.
Or, of its use in Airbag steering computers, where the code is mathematically proven to be running correctly.
- Frazzydee 17y agoHonest question: Is there something about Ada that makes it easier to mathematically prove that the code functions as intended?
- duncanj 17y agoAda does have useful things like a formal "denotational" semantics that make it easier than certain other languages. http://www.google.com/search?client=safari&rls=en&q=ada+denotational+semantics&ie=UTF-8&oe=UTF-8 http://www.google.com/search?client=safari&rls=en&q=... Years ago, when I looked into it, an "operational" semantics hadn't been defined for Ada, but it seems that the modern language has a defined subset or profile.
- shin_lao 17y agoThere is a difference between proving a small amount of code that controls airbag (and you just prove the written code, not the compiler, not the os, not the hardware) and millions of lines of code running in a complex machine that run in arbitrary conditions (the car).
- nitrogen 17y agoIn a computer that critical and that simple, there is no OS, and the compiler (or assembler) is tested for the program in question. The hardware design can be demonstrated to correctly execute every permutation of every instruction.
- m0th87 17y agoThe hardware design can be demonstrated to correctly execute every permutation of every instruction. Isn't that impossible vis-a-vis the halting problem?
- nitrogen 17y agoI should rephrase that "every permutation of every instruction executed by the program". I'm not trying to prove that every program is correct, only that my program is correct. That is possible by using a well-defined and fully-proven subset of the available features of the language and processor. For example, designing your program and CPU as a set of state machines allows you to define all possible states of the system (which are deliberately limited), define all the state transitions, then verify that every input condition for each state results in the correct state transition. Even if you simply brute force your way through every state and every transition instead of using mathematical generalizations, you've still proven that the program is correct.
- elblanco 17y agoAs it turns out, this doesn't actually work. State derived program analysis has been shown to not be provable for all cases. Particularly when the state-space is very large, and when state transitions are non-atomic in the code, e.g. two or more state transitions in a code block. The best research I've seen on this was done with Access Control Matrices in the Computer Security field. e.g. can you prove in a general sense that a sequence of atomic state changes to an ACM result in no violations of access control? The answer is, for atomic state changes you can prove that they are internally consistent, but not that they do not introduce a flaw in the ACM. In other words, because proving software reduces to proving correctness, it only proves that the software is internally consistent. Basically it's a circular proof. It doesn't prove that the software is without flaw.
- RevRal 17y agoWhoa, I didn't that realize Ada was still being used. My dad used it in defensive programming, missiles I think.
- nikolajsheller 17y agohttp://ertos.nicta.com.au/research/l4.verified/ http://ertos.nicta.com.au/research/l4.verified/