[SystemSafety] Machine models under formal methods

[paul_e.bennett at topmail.co.uk]

On 10/11/2017 at 2:39 PM, "Todd Carpenter" <todd.carpenter at adventiumlabs.com> wrote:
>
>Correct me if I'm wrong (I'm sure I am), but the "[SystemSafety]
>Bursting the anti formal methods bubble" discussion seems to 
>assume that
>we have a clue about what's going on beneath our software. As a 
>caveat,

If the developer doesn't know what is going on 'under the hood', then
I agree, they are working with incomplete and dubious quality information.

>I agree with the premise that if you can't even assure your 
>software
>using a simple machine model (instruction X copies the values 
>stored in
>memory locations to/from registers, instruction Y performs ALU
>operations on registers, and memory values don't change unless you 
>use
>instructions X or Y), then you can't hope to know what your 
>software
>does on a complex machine.

Fortunately I can be that certain. Then I prefer to use simple machines
that are fully understandable. The abstract machine I programme for, 
and which has been realised in hardware, is now coming up to its fiftieth
anniversary year. With reviews that include a Fagan Inspection, Functional
Testing and Limitations Testing, I can certify that each software component
behaves as advertised in the software components datasheet.

>Unfortunately, we no longer have simple machines. I've heard 
>claims from
>microkernel, RTOS, and secure OS vendors that they verify their 
>code
>(using a variety of means, including formal proofs, analysis, etc.)
>against instruction set models. But those instruction sets are 
>often
>backed by microcode, which was not developed under formal methods.
>Worse, on some processors, that microcode is mutable, and loaded at
>run-time. Furthermore, there are all sorts of other things going on
>under your simple ALU, including Turing complete MMUs, IOMMUs, and 
>DMA
>engines.

There has been a recent interest in the use of FPGA's for implementing
processor architectures. Some of those implementations are also getting
quite complex.

One colleague is developing a Space App, in which he is adjusting the
model to eventually remove the processor from a Safety Critical solution
just before it goes to ASIC. The processor being in there helps to develop
the logic of what will be left and assists in developing tests for the eventual
ASIC to prove the logic was implemented properly.

Goal guided Component Oriented Development and System Architecting
guided selection of suitable components should be the way we consider
things. Components have data-sheets which explicitly state functionality
and the limitations on using the components. Selected components should
arrive with a CofC attached. That brings the hardware style certainties into
the software engineering world. Think on it.

Regards

Paul E. Bennett IEng MIET
Systems Engineer
Lunar Mission One Ambassador
-- 
********************************************************************
Paul E. Bennett IEng MIET.....
Forth based HIDECS Consultancy.............
Mob: +44 (0)7811-639972
Tel: +44 (0)1392-426688
Going Forth Safely ..... EBA. www.electric-boat-association.org.uk..
********************************************************************