Re: [SystemSafety] systemsafety Digest, Vol 29, Issue 7

From: Nick Lusty < >
Date: Mon, 15 Dec 2014 00:09:34 +0000


Hi Rod,
As a subcontractor, I really have no idea. It all worked in the end, but like most late phase bodges it wasn't efficient, nor did one have the confidence of real SPARK code, as although peer reviewed, there was always the risk that the SPARK shadows did not correspond to the original Ada. The lack of constrained Ada types also did not help getting the proofs together.

On 14/12/2014 14:26, Roderick Chapman wrote:
>
> On 12/12/2014 11:00,
> systemsafety-request_at_xxxxxx >> The new Mission Computer software was still in
>> Ada, but not in a SPARK compatible subset
>
> That's interesting. Who paid the bill for you to put it right and
> repeat the analysis? Lockheed? MoD? RAF?
> - Rod
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety_at_xxxxxx



The System Safety Mailing List
systemsafety_at_xxxxxx Received on Mon Dec 15 2014 - 01:09:46 CET

This archive was generated by hypermail 2.3.0 : Thu Apr 25 2019 - 20:17:06 CEST