[SystemSafety] proofs

[Olwen Morgan]

In my experience, most small-to-medium microcontroller applications 
(say, targetted on Cortex M or Cortex R cores, just to give a benchmark) 
could quite easily be constructed by glueing together small 
pre-validated components selected from application-oriented libraries.

It's significant, IMO, that much PLC programming now works like this, 
using function-block programming. I have a lot of respect for the 
PLC-programming/machine-safety community, because it does things in a 
disciplined way from which other software safety constituencies could, 
IMO, learn a great deal.


Olwen


On 23/11/2018 12:53, paul_e.bennett at topmail.co.uk wrote:
> On 23/11/2018 at 12:10 PM, "Peter Bernard Ladkin" <ladkin at causalis.com> wrote:
>> Paul,
>>
>> how is what you envisage different from strong typing + pre-
>> /postconditions?
>> (The example you give fits that description.)
> My preferred programming environment is generally untyped unless
> the programmers themselves force that by their own extensions to the
> basic language. There is, though, a very clear data passing mechanism
> which is always used and the declarations will refer to the intended type
> that the function will handle. Hence, stating what pre-call data is available
> and what post-call data is produced in the documentation allows others
> selecting the function see if it fits their needs.
>
> The difference I see, is that the compilers (and it is possible in my systems
> to have many of those, but they are all quite simple single focus) do not do
> the automated checking that you might be implying by your own viewpoint.
>
> Regards
>
> Paul E. Bennett IEng MIET
> Systems Engineer
> Lunar Mission One Ambassador