Re: High-integrity networking

[Simon Wright <simon.j.wright@mac.com>]

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 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? Could a multi-partition program use different
profiles for different parts?

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.