[SystemSafety] C for OSs

[Olwen Morgan]

This might ruffle a few feathers ... but here goes ...

I often wonder whether RTOSs or hypervisors are solutions looking for 
problems. Albeit on small systems, I've found that modelling required 
behaviour using Coloured Petri-Nets leads to verifiable designs that do 
not actually need RTOS capabilities. If you're paying close attention to 
avoiding unnecessary complexity, you find very few control applications 
that cannot be implemented robustly with rate-monotonic time-triggered 
loops. Naturally, however, these are much easier to implement on small 
microcontroller architectures (comparable with Cortex M and Cortex R) 
than on x86_64 targets. Once you need the power of x86_64, the RTOS is 
there to manage the metal much more than it is actually to support the 
application. In such cases, my inclination would be to ask whether some 
might not be simpler to implement using several Cortex R level 
controllers rather than a single x86_64 monstrosity. COTS industrial 
x86-64 boards are, IMO, a very mixed blessing.

And BTW, significant parts of the UK ATC s/w infrastructure are written 
in C owing to the use of X libraries to paint radar display screens. Use 
of C in IFACTS was subsetted to an (unavoidably) less-strict-than-MISRA 
level. And, when I last looked at it, it still generated over 12,000 
MISRA C violation warnings for which technical concessions were approved 
and for which controlled suppressions had been put into the code at my 
suggestion. After the suppressions were in, there remained around 300 
unsuppressed MISRA C violation messages - mainly to do with X macros -  
that were avoidable but were, reasonably IMO, deemed less risky to leave 
in place with concessions than to change.

regards,

Olwen





On 06/09/2019 16:42, Roderick Chapman wrote:
> On 06/09/2019 16:17, Martyn Thomas wrote:
>
>> SFAIK, the iFACTS air traffic control tools were written in SPARK and
>> run on the bare hardware.
>
> No... iFACTS runs on the same infrastructure as NERC, which is IBM 
> hardware running AIX (albeit a _very_ stable and well-controlled 
> release of AIX). For SPARK, this is something of an oddity, since most 
> SPARK system do indeed run bare-metal or on some sort of small RTOS.
>
> The Muen hypervisor is an interesting an example - an entire x86_64 
> hypervisor, that is written in SPARK, and has been subject to proofs 
> of type-safety and so on.  It's open source and here
>
>  https://muen.codelabs.ch
>
>  - Rod
>
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: 
> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety