[SystemSafety] Safety and programming languages

[Roderick Chapman]

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/20220316/6f64650a/attachment.html>