Re: High-integrity networking

[Peter Morris <no@spam.please.net>]

On Wed, 10 Oct 2007 20:40:17 +0100, Simon Wright
<simon.j.wright@mac.com> wrote:

>Peter Morris <no@spam.please.net> writes:
>
>> Issues with using Ravenscar and the Ada Distributed Systems Annex for
>> High-Integrity Systems
>> http://www.acm.org/sigada/ada_letters/march2001/103-audsley_1.pdf
>>
>> It identified the following problem:
>>
>> "It is clear that in order to facilitate distributed
>> high-integrity real-time programming, the run-time
>> support for distributed programming itself should conform
>> to the Ravenscar profile. We have illustrated in this paper
>> that this support requires greater expressive power than that
>> afforded by Ravenscar. The result is greater complexity in
>> the run-time � the code is almost certainly less analyzable,
>> and definitely harder to produce and read."
>
>Not clear from the last sentence whether it's the run-time or the user
>code that's harder to analyse, produce or read. (Presumably that's not
>true of Ravenscar itself, or no one would use it? It would be a hard
>sell to management ...)
>
I think they are referring to implementations of the DSA. Eg they say
that the GLADE implementation uses many protected objects that don't
comply with Ravenscar requirements.  

>> I don't know if anyone has solved this problem.
>
>Could a solution be analogous to the SPARK technique of telling the
>Analyser that certain elements can be assumed to behave as specified
>without needing proof? 
>
That should be possible. Eg if an implementation of the DSA had passed
sufficiently rigorous tests.

However I feel there is room for something simpler than the DSA.

>
>Of course, that depends on what problem you are trying to solve; using
>Ravenscar makes it easier to argue for correctness, not using
>Ravenscar probably doesn't make an argiment impossible.
>
I think that is true.


Regards,
Peter Morris