3 ms·

Keep in mind they don't use C/C++. They use C/C++ with a coding standard (like MISRA), static analysis tools, validated compilers, development processes incorp

Keep in mind they don't use C/C++. They use C/C++ with a coding standard (like MISRA), static analysis tools, validated compilers, development processes incorporating change control, documentation, verification and validation, etc. What alternative are you suggesting?

progman 11y ago
I know that Ada compilers are 100% verified correct but is there really any validated C++ compiler? Which one? AFAIK (partial) assurance in C/C++ can only be handled by additional testing tools, Frama-C for instance. I agree that C/C++ should not be used for security applications. Ada is a much better choice because it was designed for security.
- lambdaelite 11y ago
  Not sure if I'm understanding your question correctly, but Wind River claims their Diab compiler is validated by TÜV NORD and is has been used for stuff up to SIL4. In fact, they (http://windriver.com/products/product-overviews/PO_Diab_Compiler_1211.pdf http://windriver.com/products/product-overviews/PO_Diab_Comp...) say: Diab Compiler has been a reliable code generation tool for avionics products certified for DO-178B, products for the nuclear market certified to IEC 60880, railway applications certified to EN 50128, and industrial products certified to IEC 61508, and is now qualified for use in automotive applications certified to ISO 26262. Ada does have some built-in advantages, but I think my point still stands: the language is a small part of the entire SDLC, and I don't think it's the most important part.
  - castell 11y ago
    Is TÜV Nord/Sued known for extensive software checking?
- CHY872 11y ago
  Are you sure that Ada compilers are verified correct? I'm pretty sure that the only industrial formally verified compiler is CompCert (for C), though I could be wrong. The motivation for CompCert was certainly that Airbus wanted such a compiler. Ada wouldn't be a better choice simply because it's designed for security. It'd be a better choice if it turned out better in practice. I've read some of the studies that have been done, and I haven't found them convincing. Requiring additional tools just isn't a problem, if it works well. Don't criticise the process, criticise the result.
tormeh 11y ago
Ada, of course. Are you saying it wasn't at the forefront of your mind? If I sound patronizing it's because I am.
- lambdaelite 11y ago
  As I said elsewhere, Ada does have some very nice built-in advantages, but I think my point stands: the language is a small part of the entire SDLC, and I don't think it's the most important part. The focus on languages instead of the SDLC is telling, I think.

progman 11y ago

I know that Ada compilers are 100% verified correct but is there really any validated C++ compiler? Which one? AFAIK (partial) assurance in C/C++ can only be handled by additional testing tools, Frama-C for instance. I agree that C/C++ should not be used for security applications. Ada is a much better choice because it was designed for security.

lambdaelite 11y ago
Not sure if I'm understanding your question correctly, but Wind River claims their Diab compiler is validated by TÜV NORD and is has been used for stuff up to SIL4. In fact, they (http://windriver.com/products/product-overviews/PO_Diab_Compiler_1211.pdf http://windriver.com/products/product-overviews/PO_Diab_Comp...) say: Diab Compiler has been a reliable code generation tool for avionics products certified for DO-178B, products for the nuclear market certified to IEC 60880, railway applications certified to EN 50128, and industrial products certified to IEC 61508, and is now qualified for use in automotive applications certified to ISO 26262. Ada does have some built-in advantages, but I think my point still stands: the language is a small part of the entire SDLC, and I don't think it's the most important part.
- castell 11y ago
  Is TÜV Nord/Sued known for extensive software checking?
CHY872 11y ago
Are you sure that Ada compilers are verified correct? I'm pretty sure that the only industrial formally verified compiler is CompCert (for C), though I could be wrong. The motivation for CompCert was certainly that Airbus wanted such a compiler. Ada wouldn't be a better choice simply because it's designed for security. It'd be a better choice if it turned out better in practice. I've read some of the studies that have been done, and I haven't found them convincing. Requiring additional tools just isn't a problem, if it works well. Don't criticise the process, criticise the result.

tormeh 11y ago

Ada, of course. Are you saying it wasn't at the forefront of your mind? If I sound patronizing it's because I am.

lambdaelite 11y ago
As I said elsewhere, Ada does have some very nice built-in advantages, but I think my point stands: the language is a small part of the entire SDLC, and I don't think it's the most important part. The focus on languages instead of the SDLC is telling, I think.