Re: Ada in command / control systems

[russ lyttle <lyttlec@removegmail.com>]

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.