[SystemSafety] systemsafety Digest, Vol 29, Issue 7
Nick Lusty
nl887 at my.open.ac.uk
Mon Dec 15 01:09:34 CET 2014
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 lists.techfak.uni-bielefeld.de wrote:
>> 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 TechFak.Uni-Bielefeld.DE
More information about the systemsafety
mailing list