<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
{mso-style-priority:34;
margin-top:0cm;
margin-right:0cm;
margin-bottom:0cm;
margin-left:36.0pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.apple-converted-space
{mso-style-name:apple-converted-space;}
span.EmailStyle21
{mso-style-type:personal-reply;
font-family:"Arial",sans-serif;
color:black;
font-weight:normal;
font-style:normal;
text-decoration:none none;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:2140225446;
mso-list-type:hybrid;
mso-list-template-ids:132690270 451159604 134807555 134807557 134807553 134807555 134807557 134807553 134807555 134807557;}
@list l0:level1
{mso-level-start-at:0;
mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
margin-left:18.0pt;
text-indent:-18.0pt;
font-family:Symbol;
mso-fareast-font-family:Calibri;
mso-bidi-font-family:Arial;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
margin-left:54.0pt;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
margin-left:90.0pt;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
margin-left:126.0pt;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
margin-left:162.0pt;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
margin-left:198.0pt;
text-indent:-18.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
margin-left:234.0pt;
text-indent:-18.0pt;
font-family:Symbol;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:none;
mso-level-number-position:left;
margin-left:270.0pt;
text-indent:-18.0pt;
font-family:"Courier New";}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:none;
mso-level-number-position:left;
margin-left:306.0pt;
text-indent:-18.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-GB" link="#0563C1" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US">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”.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US">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).<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US">Specifically<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<ul style="margin-top:0cm" type="disc">
<li class="MsoListParagraph" style="color:black;margin-left:-18.0pt;mso-list:l0 level1 lfo1">
<span style="font-size:10.0pt;font-family:"Arial",sans-serif;mso-fareast-language:EN-US">“System” is there because some guidelines can’t be checked at the software unit (or equivalent) level alone e.g. the one about recursions<o:p></o:p></span></li><li class="MsoListParagraph" style="color:black;margin-left:-18.0pt;mso-list:l0 level1 lfo1">
<span style="font-size:10.0pt;font-family:"Arial",sans-serif;mso-fareast-language:EN-US">“Undecidable” is there because compliance to some guidelines cannot be demonstrated through static analysis alone and other methods are needed.<o:p></o:p></span></li></ul>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US">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.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US">David<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:10.0pt;font-family:"Arial",sans-serif;color:black;mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<div>
<div style="border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> systemsafety <systemsafety-bounces@lists.techfak.uni-bielefeld.de>
<b>On Behalf Of </b>Roderick Chapman<br>
<b>Sent:</b> 16 March 2022 09:13<br>
<b>To:</b> systemsafety@lists.techfak.uni-bielefeld.de<br>
<b>Subject:</b> Re: [SystemSafety] Safety and programming languages<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p>I guess I might as well jump in...<o:p></o:p></p>
<p>For SPARK, start with our "greatest hits" compilation here:<o:p></o:p></p>
<p><span style="font-size:10.5pt;font-family:"Arial",sans-serif">R. Chapman and F. Schanda, “Are we there yet? 20 years of industrial theorem proving with SPARK.”<span class="apple-converted-space"> </span><em><span style="font-family:"Arial",sans-serif;color:#333333;border:none windowtext 1.0pt;padding:0cm">Invited
Keynote Paper</span></em><span style="color:#333333">, Proceedings of Interactive Theorem Proving (ITP) 2014. Springer-Verlag LNCS Vol. 8558, pp. 17-26.</span></span><o:p></o:p></p>
<p><span style="font-size:10.5pt;font-family:"Arial",sans-serif">I can supply PDF of that.<br>
<br>
</span><o:p></o:p></p>
<p><span style="font-size:10.5pt;font-family:"Arial",sans-serif">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.</span><o:p></o:p></p>
<p><span style="font-size:10.5pt;font-family:"Arial",sans-serif">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.<br>
<br>
</span><o:p></o:p></p>
<p><span style="font-size:10.5pt;font-family:"Arial",sans-serif">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).</span><o:p></o:p></p>
<p><span style="font-size:10.5pt;font-family:"Arial",sans-serif">That's it for now...</span><o:p></o:p></p>
<p><span style="font-size:10.5pt;font-family:"Arial",sans-serif"> - Rod</span><o:p></o:p></p>
<p><span style="font-size:10.5pt;font-family:"Arial",sans-serif"><br>
<br>
</span><o:p></o:p></p>
<p><span style="font-size:10.5pt;font-family:"Arial",sans-serif"><br>
<br>
</span><o:p></o:p></p>
</div>
<br>
<div><span style="font-size: small;" class="Apple-style-span"><font class="Apple-style-span" size="2" face="arial,helvetica,sans-serif"></font></span></div>
<font class="Apple-style-span" size="2">
<div style="font-size: small;"><strong><font face="arial,helvetica,sans-serif">HORIBA MIRA Ltd</font></strong></div>
<div style="font-size: small;"><font class="Apple-style-span"><br>
<font size="2" face="arial,helvetica,sans-serif"></font></font></div>
<div style="font-size: small;"><span style="font-size: small;" class="Apple-style-span"><font class="Apple-style-span" size="2" face="arial,helvetica,sans-serif">Watling Street, Nuneaton, Warwickshire, CV10 0TU, England</font></span></div>
<div style="font-size: small;"><span style="font-size: small;" class="Apple-style-span"><font class="Apple-style-span"><font size="2" face="arial,helvetica,sans-serif"></font></font></span></div>
<div style="font-size: small;"><span style="font-size: small;" class="Apple-style-span"><font class="Apple-style-span" size="2" face="arial,helvetica,sans-serif">Registered in England and Wales No. 9626352</font></span></div>
<div style="font-size: small;"><span style="font-size: small;" class="Apple-style-span"><font class="Apple-style-span" size="2" face="arial,helvetica,sans-serif">VAT Registration GB 100 1464 84</font></span></div>
<div style="font-size: small;"><span style="font-size: small;" class="Apple-style-span"><font class="Apple-style-span"><br>
<font size="2" face="arial,helvetica,sans-serif"></font></font></span></div>
<div><font face="arial, helvetica, sans-serif">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.</font></div>
</font>
</body>
</html>