[SystemSafety] Safety and programming languages

[Daniel Kästner]

"Undecidable" means that there is no algorithm which can give a precise 
yes/no answer in every possible case. It does not mean you cannot prove the 
property. If you have a sound analyzer which does not report uninitialized 
variable accesses there are none. Unless there is a failure in the tool - 
which is why safety norms require tool qualification. In a sense, the 
purpose of a tool like Astrée is to check Rule 1.3. without false negatives.



Best regards,

  Daniel.

---

Dr.-Ing. Daniel 
Kaestner --------------------------------------------------------------------
AbsInt Angewandte Informatik GmbH      Email: kaestner at AbsInt.com
Science Park 1                                                Tel: 
+49-681-3836028
66123 Saarbruecken                                     Fax: 
+49-681-3836020
GERMANY 
<http://www.absint.com/> http://www.AbsInt.com
----------------------------------------------------------------------------------------------------
Geschaeftsfuehrung: Dr.-Ing. Christian Ferdinand
Eingetragen im Handelsregister des Amtsgerichts Saarbruecken, HRB 11234





Von: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de> Im 
Auftrag von Roderick Chapman
Gesendet: Mittwoch, 16. März 2022 14:22
An: systemsafety at lists.techfak.uni-bielefeld.de
Betreff: Re: [SystemSafety] Safety and programming languages



On 16/03/2022 12:56, David Ward wrote:

Specifically

*        “System” is there because some guidelines can’t be checked at the 
software unit (or equivalent) level alone e.g. the one about recursions

*        “Undecidable” is there because compliance to some guidelines cannot 
be demonstrated through static analysis alone and other methods are needed.

I've applied a more pragmatic interpretation of those terms in the context 
of MISRA.

To me...

"System" means "this rule can't be checked on a single-translation unit, so 
it requires whole program analysis, which will be slow, and you'll only get 
really reliable results when you've finished the program, which is a bit 
late..."

"Undecideable" means "This rule is tough to check, so there will some 
mixture of false negatives and false positives. Exactly what you get depends 
on the whim of your chosen tool vendor..."

I also can't help noticing that all the _really_ important rules in MISRA 
are "System" and "Undecideable" - for example rules 1.3, 9.1, 13.2, 17.5 and 
17.8 from MISRA 2012. Admitting false negatives for 1.3 ("don't have 
undefined behaviour") is particularly nasty, since any missed UB effectively 
undermines everything else.

SPARK and Rust both take a very different approach.

 - Rod



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20220317/0d2edc76/attachment.html>