[SystemSafety] Correctness by Construction

[Michael Jackson]

Thank you all for your emails on this topic. I have quoted below what I think are the most relevant parts. My own comments follow the double dashed line after the last quote. 

----------------------

> On 14 Jul 2020, at 20:20, David Crocker <dcrocker at eschertech.com> wrote:
> 
> On 14/07/2020 17:06, Brent Kimberley wrote:
>> >> how are the software developers to reason reliably about the physical problem world where the important requirements are located and defined, and will---or will not---be satisfied? 
>> 
>> An automated World view inquiry framework? epistemology automation? ;)
> The way I suggested doing that when using Perfect Developer to develop and (to some extent) verify the software requirements is to include a model of the external physical system in the requirements specification. It is then possible to reason and construct proofs about the combined behaviour of the software + physical system, including the effects of external inputs. This approach is in principle applicable to other tool-supported formal specification languages, for example Z.
> 
> Although this is conceptually simple, the problem lies in constructing a model of the physical system and possible external inputs that is sufficiently accurate and complete to make the proofs meaningful and useful.
> 
> Cheers
> 
> David Crocker, Escher Technologies Ltd.

----------------------

On 15 Jul 2020,at 04.21, Brent Kimberley wrote:

Hi Michael.
Perhaps I misinterpreted the question.  I though the question was how can software developers reason reliability about the physical world?

My response was write more code.  ;)   
More precisely have the software to develop inferences WRT sensor / actuator / FRU / logic / bus  - failure & train operators. ;)

For example write the requested logic plus an engine to progressively refine world view.  


For example for a fly by wire or environmental controls system: there may be certain assumptions about the physical sensors, actuators, structural members, buses, DAQs, energy sources, clocks, FRUs, by which the logic engages with the physical world.  The epistemology engine would continuously update it's world view assumptions and inform an ontology layer - used by the requested software logic - to interact with the physical world.

For four engines delivering power (and data) to four propulsion units - transmission grid.  The epistemology engine identifies events such as faults, updating the ontology model, and the requested software logic using the ontology layer could to control available propulsion units - routing power (and data) around faults - in a way which ideally preserves assets. 

-----------------------

On 15 Jul 2020, at 21.10, Olwen Morgan wrote: 

On 14/07/2020 20:20, David Crocker wrote:
<snip>
> 
> include a model of the external physical system in the requirements specification. It is then possible to reason and construct proofs about the combined behaviour of the software + physical system, including the effects of external inputs. This approach is in principle applicable to other tool-supported formal specification languages, for example Z.
> 
> Although this is conceptually simple, the problem lies in constructing a model of the physical system and possible external inputs that is sufficiently accurate and complete to make the proofs meaningful and useful.
> 
Just so. And in my experience an even greater problem lies in the difficulty of persuading people that it is, in some cases , necessary. I once walked out of and blew the whistle on a train safety project where fellow engineers ignored me on this issue.


Olwen

----------------------
----------------------

Some comments:

1.   One way to think about a bipartite cyber-physical system is to regard the interface between the processor hardware and the physical problem world as providing a (bidirectional and hugely complex) API allowing the processor to monitor and control phenomena of the problem world. This API needs a full, maximally reliable, model of the physical domains and phenomena of the problem world, showing the causal chains terminated at the actuators and sensors and involving phenomena that are not directly connected to the interface. 

2.   As David says: "Although this is conceptually simple, the problem lies in constructing a model of the physical system and possible external inputs that is sufficiently accurate and complete to make the proofs meaningful and useful." Yes. But this problem is exactly parallel to the problem of describing the semantics of the programming language---both the source code and the binary code executed by the processor. It can't be relegated to an optional extra: without a solution the software developer is programming a machine---the physical problem world---for which there is no adequate semantic definition. 

3.   For a realistic system, the problem world is a large and complex system, and modelling demands some major help from structure. One approach to the problem is to structure the physical model according to the structure of the desired system behaviour. (This is what I aim at in my current work.) This approach makes sense because the physical world model supports the behaviour exactly as the processor supports the software execution. Each 'constituent behaviour' (my terminology) relies on certain properties of the problem world expressed in an associated model. 

4.   Perhaps the structuring of the physical model according to the structure of the system behaviour is also a characteristic of Brent's suggestion: "... to include a model of the external physical system in the requirements specification." That depends, of course, on the structure, format, and content of the Requirements Specification. I am keen to hear more about Requirements from anyone here who deals with them either as a consumer or a producer. 

5.   A fundamental difficulty for formal models of the physical world is that it is not itself a formal system. Brian Cantwell Smith explained the difficulty in his 1986 paper "The Limits of Correctness", pointing out the absence of a theory of informal-to-formal modelling. I think that a discipline, rather than a theory, is needed (and I aim at this too in my current work). 

-- Michael 

www.theworldandthemachine.com