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-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,ac31ec0a3cebb176 X-Google-Attributes: gid103376,public From: Robert Dewar Subject: Re: Are un-validated compilers unsafe? Date: 1999/04/25 Message-ID: <7fv6cc$5eh$1@nnrp1.dejanews.com> X-Deja-AN: 470665058 References: X-Http-Proxy: 1.0 x17.dejanews.com:80 (Squid/1.1.22) for client 205.232.38.14 Organization: Deja News - The Leader in Internet Discussion X-Article-Creation-Date: Sun Apr 25 13:46:53 1999 GMT Newsgroups: comp.lang.ada X-Http-User-Agent: Mozilla/4.04 [en] (OS/2; I) Date: 1999-04-25T00:00:00+00:00 List-Id: In article , Mark Elson wrote: > This question was prompted by the fact that a new space > project may be using GNAT in conjunction with an > un-validated RTOS on the grounds that > the combination is in widespread use and that GNAT is a > "very good" compiler (also due to the abundance of > developers as well as users). I > was somewhat surprised that they could get away with this > (although their requirement is more reliability than > safety). Does this mean there is not much motivation for > vendors to get their compilers validated these days? There is no magic in validation. The ACVC suite is a useful test suite, and a formal validation is a useful way of ensuring that a given compiler passes this suite. Whether validation is required for a given project is of course the decision of the project. In the case of GNAT, we validate mainstream native compilers, and selected cross-products. The latter are validated either because we see a very general demand, or in response to specific customer requirements. We find three situations with users of cross-GNAT systems (and there is no particular correlation with size of project, or reliability requirements). 1. There is no specific validation requirement, and it is simply not an issue. 2. There is a contract requirement with respect to the behavior of the compiler on the ACVC suite (and possibly other test suites), but no requirement for formal validation. 3. There is a formal requirement for validation (this for example is the situation for the VxWorks/68K target we recently validated). For a given project, you need to decide what you need, and talk to your vendor. For example, if you are considering something like an RTEMS/PowerPC combination, then of course this can be validated, but it will not be a zero-cost proposition. If you think validation is an important criterion, then discuss it with us. If a large support contract is involved, we may be willing to provide validation as part of this contract. Otherwise we can quote an add-on price. But check things out carefully to make sure that you really need this requirement. > In any case, does the fact that a compiler-OS-processor > has not been validated mean that it is unsafe (or > unreliable), i.e. that it is not suitable for use in > safety-critical applications? Of course not! There are compilers that are not formally validated that are considered highly reliable. For example, the Aonix/CSMART product is I think one that people would consider to be at the forefront of high reliability tools, but it is not even possible to validate it, since it is an Ada subset. Our own GNORT (GNAT No Run-Time) product aimed at safety critical applications (and in use by customers for such applications) has similar restrictions. > I'm guessing, looking > at a number of software safety requirements, that if you > don't use a validated combination then the onus is on you > is to verify down to object code level, i.e. validation > may save you work. This is the most worrisome statement in your post. The idea that validation guarantees, even informally, let alone from a formal verification process, that you can trust the compiler 100% and do not need to do your own verification is seriously flawed. A validated compiler is simply one that has passed a batch of tests. It's quite a useful batch of tests, but we would not rely on the ACVC suite, even for the testing that we do on a wavefront delivered to a customer. It is entirely inadequate for such a purpose. Our testing involves running a very large suite of tests, of which the ACVC is just one portion (and it is getting to be a smaller portion every day, as we add new tests to our own internal regression testing procedures). You will find the same is true for all other Ada vendors. Validation does not guarantee *anything* about a compiler other than that it passed a particular, very incomplete, set of tests. Why very incomplete? Because for a compiler, we don't begin to know how to make a complete set of tests, and we don't begin to know how to verify or validate an Ada compiler in the sense of rigorous procedures like FAA certification. > I've had a look at the EDS site and the choice for > embedded applications using Ada 95 seems restricted, > especially wrt. to the RTOS choice. Are > vendors not bothering to validate their compilers &OSs. See above > (or is it something that's done on demand and so > additions are only likely to occur if a particular > project can afford the validation). Is obtaining > validation an expensive exercise anyway? It depends on the situation > Do vendors subsidise it if a > projects chooses to go that route? It depends on the situation. If you are using a system that the vendor anticipates selling to others, the answer may be yes, if not, the answer may be no. I think you may get a more accurate answer to this question if you ask your vendor. CLA while it may sometimes be able to answer some questions is hardly the place to ask about pricing policies of specific vendors, especially when we don't know what configuration you are talking about! If indeed you are considering GNAT, this is something you should discuss with the sales folks at ACT Europe (sales@act-europe.fr). > Are there other means by which compiler/OS/target > combinations get certified You are looking for something that does not exist, namely a certification mark that will guarantee a compiler is safe to use. There are no "other means", because there are no means at all. Validation of a compiler does NOT provide this assurance. > or even proven by common use? Is there a list of such? The only list that would be meaningful here is references to existing projects. You should ask your vendor for references, they may be more significant than any validation certificate. > Many thanks for any replies. Sorry for all the questions - I'm new to > Ada and safety-critical software. Your questions are good ones. The choice of the word validation for Ada compilers was an unfortunate one with respect to the safety critical community. When that community talks about validation or certification, they really mean it! I am afraid that our technology in compilers just has not reached that stage. We don't even know how to make useful formal specifications for languages like Ada (the EEC sponsored effort in this area with Ada 83 resulted in several telephone books full of mathematical formulae and did not even address the hard parts of the language like rep clauses and allowed optimizations. The end result was essentially useless to the Ada community, although as a research project in learning more about formal specification techniques it was useful). We can address the issue of certifying runtimes, and for that two approaches have been used, as mentioned above. Aonix provides a subset implementation that uses a very small, very well defined run-time that can and has been subjected to standard FAA certification procedures (this is CSMART, the certified small Ada run time system). A more recent product (Raven I believe is the name) extends this to include a small subset (Ravenscar) of the tasking capability of Ada (CSMART excludes tasking). You should consult Aonix for further details. For GNAT, we have a product GNORT that has no run time at all. Again it is a small subset (the inspiration for the subset is the SPARK language from Praxis). A nice thing about this approach is that since there is no run-time, there is nothing to certify! Indeed the GNORT approach is an interesting product of the open source approach. One leading person in the Ada safety critical vendor community told me once that their company had considered a zero-byte runtime approach, but one of the reasons they had rejected it was a commercial one, there would be nothing to sell :-) In the case of GNAT, we are basically selling support, rather than shrink wrapped software, so such commercial considerations do not apply. For more details on the GNORT approach, contact sales@gnat.com or sales@act-europe.fr, or if you have general technical issues which would be of interest to the CLA community, then you could post questions here and I would be happy to answer them (I like to be careful to stay on the right side of the information/advertising line) Robert Dewar Ada Core Technologies -----------== Posted via Deja News, The Discussion Network ==---------- http://www.dejanews.com/ Search, Read, Discuss, or Start Your Own