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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED.7FNRKtgi3I/d6D55i78OBw.user.gioia.aioe.org!not-for-mail From: russ lyttle Newsgroups: comp.lang.ada Subject: Re: Ada in command / control systems Date: Wed, 27 Feb 2019 12:49:44 -0500 Organization: Aioe.org NNTP Server Message-ID: References: <2199b15b-d704-403f-a6c4-00fab29792d5@googlegroups.com> NNTP-Posting-Host: 7FNRKtgi3I/d6D55i78OBw.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.5.1 X-Notice: Filtered by postfilter v. 0.9.2 Content-Language: en-US Xref: reader01.eternal-september.org comp.lang.ada:55704 Date: 2019-02-27T12:49:44-05:00 List-Id: On 2/27/19 9:17 AM, Niklas Holsti wrote: > On 19-02-27 15:22 , russ lyttle wrote: >> On 2/26/19 6:09 PM, Simon Wright wrote: >> >>> I'm having a bit of trouble working out what you're trying to do. You >>> seem to be targeting a wide range of platforms, from Linux to embedded >>> MCUs. The need to control sizes etc is much less in a Unix-like >>> environment, and I doubt very much you'd want to use EEPROM (do you mean >>> that, by the way? MCUs seem to use Flash) or even bother to think about >>> how the linker arranges things so that the program starts up properly. >>> >> Should have said Flash. >> Watch >> https://www.youtube.com/watch?v=3jstaBeXgAs > > Hacking automotive computers? You could have said. I suppose you are > aiming at hack-resistant or hack-proof distributed (but closed) systems. > >> Not my project, but you get the idea. Lots of (small) computers >> networked. Penney's count so the lowest cost mcu must be used. > > Minimizing repeating HW costs usually means increasing the design and > development costs. Be sure to have your balance right, especially if you > want to push the state of the art in safety and reliability proofs. > Having more HW resources may allow simpler SW designs that are easier to > prove and/or validate. > >> The life of the software will be long, even though some of the mcu >> might change. > > Even more reason to allow margin in HW resources. You don't want to > invest in super-optimizing your SW for a specific, minimal HW, because > that usually reduces SW portability. > >> We will have one or more R-Pi class devices that need a provably secure >> and correct OS. While Raspbian is much better than Windows 10, how would >> you show that it is correct? > > So the central question is what services this "OS" should provide. > Presumably not the full set provided by a typical Linux distro? > Yes > Even with a reduced OS, the usual approach is to partition and separate > the critical services from the less critical services, for example using > a "separation kernel" like Muen. > Muen might be the answer. It is SPARK and Ada. Can it target anything other than X86/64? >>> ... A lot of this will have been looked after by >>> whoever provides your runtime. >> "Whoever provides your runtime" is me. > > Why should you provide runtimes yourself, when you can buy them from the > Ada compiler vendors -- presumably at smaller total cost, with faster > delivery? At most, you might yourself tailor the COTS runtimes for your > targets. > Yep, those are the problems we face. A big problem is convincing management that 40% free-board on all resources is required. Run-time licensing fees could run into millions per year.There are lots of buy-vs-build discussions going on.