[SystemSafety] Safety and programming languages

[David Ward]

I wasn’t going to bite on Rod’s comments about MISRA but I think it’s worth pointing out that the “system” and “undecidable” attributes are there because of limitations in the way people apply MISRA C (or indeed any coding standard).  Often we see people running some basic static analysis checks at the software unit level (or whatever term you prefer to use – let’s not open that can of worms!!) and assuming that if they get no error reports then everything is fine “because I’ve passed MISRA”.

As ever we gently remind readers that MISRA C (or indeed any coding standard) has to be used within the context of a robust software development process (e.g. ISO 26262 Part 6 but others are available) and with a robust approach to identifying which guidelines are complied with, how compliance is demonstrated and how to handle deviations (see MISRA Compliance:2020 in this context which can of course be used for any coding standard not just a MISRA one).

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.

On the subject of Rust this seems to be gaining some traction, there is a new activity within the SAE Functional Safety committee to develop some guidance on use of Rust in safety and security relevant contexts, and there is also a parallel activity within AUTOSAR.

David

From: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de> On Behalf Of Roderick Chapman
Sent: 16 March 2022 09:13
To: systemsafety at lists.techfak.uni-bielefeld.de
Subject: Re: [SystemSafety] Safety and programming languages


I guess I might as well jump in...

For SPARK, start with our "greatest hits" compilation here:

R. Chapman and F. Schanda, “Are we there yet? 20 years of industrial theorem proving with SPARK.” Invited Keynote Paper, Proceedings of Interactive Theorem Proving (ITP) 2014. Springer-Verlag LNCS Vol. 8558, pp. 17-26.

I can supply PDF of that.


You should definitely know about MISRA. If you absolutely have to stick with C, then no excuse for not using MISRA, but be aware of its limitations. Look at how many of the rules are tagged "System" and "Undecideable" and make your own mind up if that's good enough for you.

As for Rust... it shows great promise. The "no_std" profile is interesting. There are research-level static verification tools. I have used MIRAI, Prusti, Kani and Crux-MIR and there are many more in the works. There are several problems: other than trait-bounds for generics, there is no standard contract language, so the different tools all try to define their own, so they're all different and lacking basic features such as quantifiers. None of these tools are commercially supported. Rust also lacks user-defined scalar types and so-called "Liquid Types", which are absolutely essential in SPARK.


See also the "Ferrocene" project from Ferrous Systems - that shows great promise to stabilize things and bring some much-needed provenance to the Rust world (at least for embedded systems).

That's it for now...

 - Rod





HORIBA MIRA Ltd

Watling Street, Nuneaton, Warwickshire, CV10 0TU, England
Registered in England and Wales No. 9626352
VAT Registration  GB 100 1464 84

This email and any files transmitted with it are confidential and intended solely for the use of the individual or entity to whom they are addressed. If you are not the named addressee you should not disseminate, distribute or copy this e-mail. Please notify the sender immediately by e-mail if you have received this e-mail by mistake and delete this e-mail from your system. If you are not the intended recipient you are notified that disclosing, copying, distributing or taking any action in reliance on the contents of this information is strictly prohibited.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20220316/af6ff857/attachment-0001.html>