From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,eb0daafec4ae827a X-Google-Attributes: gid103376,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!news2.google.com!border1.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!news1.optus.net.au!optus!newsfeeder.syd.optusnet.com.au!news.optusnet.com.au!not-for-mail From: Peter Morris Newsgroups: comp.lang.ada Subject: Re: High-integrity networking Date: Thu, 11 Oct 2007 22:30:25 +0930 Message-ID: <9p1sg31bj47b0dvk39vlcis33boa5k3a9s@4ax.com> References: <1191845623.383675.190820@d55g2000hsg.googlegroups.com> X-Newsreader: Forte Free Agent 2.0/32.652 MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit NNTP-Posting-Host: 58.110.80.234 X-Trace: 1192107623 6925 58.110.80.234 X-Original-Bytes: 2632 Xref: g2news2.google.com comp.lang.ada:2429 Date: 2007-10-11T22:30:25+09:30 List-Id: On Wed, 10 Oct 2007 20:40:17 +0100, Simon Wright wrote: >Peter Morris 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