[SystemSafety] systemsafety Digest, Vol 29, Issue 7

[Nick Lusty]

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