<div dir="ltr">Thanks Dewi<div><br></div><div>So far I have declined the opportunity to comment on this thread as I simply don't have the time.  Today, I'm on a long webex call, some of which is interesting, and therefore have some 'spare' time.....or rather multi-tasking time.</div><div><br></div><div>To be clear, D-RisQ Kapture enables English [like] Software High Level Requirements (HLR) to be written. It helps avoid some of the problems of writing verifiable HLR, among a bunch of other features.  The D-RisQ Kapture tool enables an automatic translation to a formal representation (hidden) which is why it can be useful in both formal and non-formal developments.  It is currently targeted at control systems and has been used to describe the behaviour for FCS (as Dewi highlighted) and, among plenty of other uses, to describe the required behaviour of unmanned systems.  All aimed at meeting DO-178C/DO-333 Objectives in Table FM.A-3 (it won't meet all of them; some review is needed eg for 'derived requirements'). It has been used (in the US) in retrospect to find issues in flight ready code that had failed system test and, in using Kapture, enabled the discovery of hidden issues which would have meant system failure in other tests, possibly post delivery given the corner case of one of the issues discovered (lots of $$$ savings as a result). In future issues of D-RisQ Kapture, we will be able to automatically check between requirements that they are [self] consistent, among a few other features.  This assists with CbyC.</div><div><div><br></div></div><div>We also intend to develop a System Requirements version of the tool; similar features to Kapture.  This will link to Kapture and will enable a formal refinement check to be undertaken (automatically).  The System level tool will have similar features to Kapture.  This effectively will mean that the English [like] System statements have been correctly and completely, etc refined into software HLR.  Lots of effort still to come. </div><div><br></div><div>If a formal process is to be followed and the design is in Simulink/Stateflow, we can independently, formally and automatically verify that the design satisfies the HLR (from Kapture) using the D-RisQ Modelworks.  Again, this supports various Objectives in DO-333 Table FM.A-4; in this case it meets all but 3 of the 13 objectives completely, the remainder are partially met.  Again, supports the notion of CbyC.</div><div><br></div><div>CLawZ for C is under development and will independently, formally and automatically verify automatically produced C code (from OTS coders such as initially dSPACE TargetLink) against the design.  The template for this tool is the version we did for Ada some years ago.  It will enable claims against DO-333 Table FM.A-5 Objectives (all but 2, ignoring PDI ...for now).  The aim is to have this ready by the end 2020.  Meanwhile, we aim to develop FEVER which will independently, formally and automatically verify automatically produced EOC (ie the compiled code) against the source code and enable clams to be made against all but one of the DO-333 Table FM.A6 Objectives; the remainder will require some manual test, but not necessarily unit test. Aim is for mid 2021 if all goes according to plan.  Both tools support CbyC.  Note that the use of all 4 tools gives claims for all but one of the FM.Table A-7 Objectives. </div><div><br></div><div>While the above is an overview, I will emphasise that some testing will be required.  This will not necessarily mean 'unit test', but some other aspects of checking how the code functions in the hardware will be needed. Nevertheless, it will significantly speed up development, enable changes to be inserted quickly and assuredly and certification support given.</div><div><br></div><div>Hope that is clear.  If you want to contact me for details of the technology, please do : <a href="mailto:njt@drisq.com">njt@drisq.com</a> </div><div><br></div><div>Cheers</div><div><br clear="all"><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><span></span><span></span>Nick Tudor<div>Tudor Associates Ltd</div><div>Mobile: +44(0)7412 074654</div><div><a href="http://www.tudorassoc.com" target="_blank">www.tudorassoc.com</a></div><div><img src="http://www.tudorassoc.com/wpimages/wpb4e71a5c_0f.jpg" width="200" height="40"></div><div><font color="#00144d" face="Arial, Helvetica, sans-serif" size="1"><b><br></b></font></div><div><span style="color:rgb(0,20,77);font-family:Arial,Helvetica,sans-serif"><font size="1"><b><span></span><span></span>77 Barnards Green Road</b></font></span></div><div><span style="color:rgb(0,20,77);font-family:Arial,Helvetica,sans-serif"><font size="1"><b>Malvern</b></font></span></div><div><span style="color:rgb(0,20,77);font-family:Arial,Helvetica,sans-serif"><font size="1"><b>Worcestershire</b></font></span></div><div><span style="color:rgb(0,20,77);font-family:Arial,Helvetica,sans-serif"><font size="1"><b>WR14 3LR</b><strong><br>Company No. 07642673</strong></font></span></div><div><span style="color:rgb(0,20,77);font-family:Arial,Helvetica,sans-serif"><font size="1"><strong>VAT No:116495996</strong></font></span></div><div><span style="color:rgb(0,20,77);font-family:Arial,Helvetica,sans-serif"><font size="1"><strong><br></strong></font></span></div><div><strong style="color:rgb(0,20,77);font-family:Arial,Helvetica,sans-serif;font-size:x-small"><a href="http://www.aeronautique-associates.com" target="_blank">www.aeronautique-associates.com</a></strong>
</div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, 15 Jul 2020 at 12:13, Dewi Daniels <<a href="mailto:dewi.daniels@software-safety.com">dewi.daniels@software-safety.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Michael,<br><br>At Altran, they use Z to express requirements. I believe that Altran are moving to Alloy. At Callen-Lenz, we're using D-RisQ's Kapture requirements language.<br><br>You make a good point about the physical problem world. Your observation highlights the boundaries of Correctness by Construction. Consider a flight control system. Just because we can prove that the code is a correct implementation of a PID controller (for example) doesn't mean that the flight control system flies the aircraft accurately (or at all). That depends on how the PID controller is tuned and how it interacts with the airframe. We can verify the flight control system using a flight model, though the flight model itself is an abstraction of the real aircraft. Even if we can show that the flight control system flies the aircraft accurately, it doesn't necessarily mean that the aircraft has desirable handling qualities.<br><br>This doesn't mean that Correctness by Construction has no value. At Callen-Lenz, we're developing a flight control system for air taxis and personal air vehicles. We're using formal methods (specifically D-RisQ's Modelworks, CLawZ and FEVER tools) to verify that the binary is a correct implementation of the software requirements, which are expressed in Kapture. That greatly reduces the number of tests that we need to write (it does not eliminate testing altogether), meaning that we can deploy working, certifiable code very quickly using our model-based development environment.<br><br>One of the best compliments I've received was when someone said, "Dewi has the ability to just write working code". I'm not sure that person appreciated how much thought I'd put into the requirements and the design before I wrote a single line of code.<br><div><a name="m_-5038383606645057224_SignatureSanitizer_SafeHtmlFilter_UNIQUE_ID_SafeHtmlFilter__MailAutoSig"><span style="font-size:10pt;font-family:Arial,sans-serif"><br></span></a></div><div><a name="m_-5038383606645057224_SignatureSanitizer_SafeHtmlFilter_UNIQUE_ID_SafeHtmlFilter__MailAutoSig"><span style="font-size:10pt;font-family:Arial,sans-serif">Yours,</span></a></div><div><div dir="ltr"><div dir="ltr"><p><span style="font-family:Arial,sans-serif;font-size:10pt">Dewi Daniels | Director | Software Safety Limited</span><br></p><p><span style="font-size:10pt;font-family:Arial,sans-serif" lang="FR">Telephone +44 7968 837742 | Email </span><span style="font-size:10pt;font-family:Arial,sans-serif;color:purple" lang="FR"><a href="mailto:ddaniels@verocel.com" target="_blank">d</a><a href="mailto:ewi.daniels@software-safety.com" target="_blank">ewi.daniels@software-safety.com</a></span></p><p><font face="Arial, sans-serif">Software Safety Limited is a company registered in England and Wales. Company number: </font><font face="Arial, sans-serif">9390590</font><font face="Arial, sans-serif">. Registered office: Fairfield, 30F Bratton Road, West Ashton, Trowbridge</font><span style="font-size:small;font-family:Arial,sans-serif">, United Kingdom </span><span style="font-size:small;font-family:Arial,sans-serif">BA14 6AZ</span></p></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 14 Jul 2020 at 10:14, Michael Jackson <<a href="mailto:jacksonma@acm.org" target="_blank">jacksonma@acm.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dewi: <br>
<br>
Yes: but how are requirements to be expressed and communicated to the software developers? And if the requirements are communicated, how are the software developers to reason reliably about the physical problem world where the important requirements are located and defined, and will---or will not---be satisfied? And is 'correctness' a proper word to use about artifacts in the physical world at the scales relevant to software engineering? <br>
<br>
Yours, <br>
<br>
-- Michael<br>
<br>
> On 13 Jul 2020, at 20:55, Dewi Daniels <<a href="mailto:dewi.daniels@software-safety.com" target="_blank">dewi.daniels@software-safety.com</a>> wrote:<br>
> <br>
> Michael,<br>
> <br>
> In the context of “Correctness by Construction”, I would say that Correctness means “compliance with requirements”.<br>
> <br>
> Yours,<br>
> Dewi<br>
> <br>
> On Mon, 13 Jul 2020 at 13:59, Michael Jackson <<a href="mailto:jacksonma@acm.org" target="_blank">jacksonma@acm.org</a>> wrote:<br>
> Hoping for illuminating replies, I ask an open question. <br>
> <br>
> In the phrase "Correctness by Construction", what does 'correctness' mean? <br>
> <br>
> -- Michael<br>
> _______________________________________________<br>
> The System Safety Mailing List<br>
> <a href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE" target="_blank">systemsafety@TechFak.Uni-Bielefeld.DE</a><br>
> Manage your subscription: <a href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety" rel="noreferrer" target="_blank">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a><br>
> -- <br>
> Yours,<br>
> <br>
> Dewi Daniels | Director | Software Safety Limited<br>
> <br>
> Telephone +44 7968 837742 | Email <a href="mailto:dewi.daniels@software-safety.com" target="_blank">dewi.daniels@software-safety.com</a><br>
> <br>
> Software Safety Limited is a company registered in England and Wales. Company number: 9390590. Registered office: Fairfield, 30F Bratton Road, West Ashton, Trowbridge, United Kingdom BA14 6AZ<br>
> <br>
<br>
</blockquote></div>
_______________________________________________<br>
The System Safety Mailing List<br>
<a href="mailto:systemsafety@TechFak.Uni-Bielefeld.DE" target="_blank">systemsafety@TechFak.Uni-Bielefeld.DE</a><br>
Manage your subscription: <a href="https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety" rel="noreferrer" target="_blank">https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety</a></blockquote></div>