[SystemSafety] Static Analysis

Sat Mar 8 10:50:19 CET 2014

Nick:

Yes. I did not mean to imply that the problem can be solved by eschewing
formal representations and reasoning. And I agree that the very activity of
formalisation raises questions and demands answers that might otherwise
be neglected.

The problem I had in mind is inherent in the control of complex behaviours
in the physical world by software---which is effectively formal. This is what
Brian Cantwell Smith called the "model-world relationship" in his paper on
"The Limits of Correctness" (and I like to refer to as the "right-hand side
problem"). He characterises the problem in Section 5 of:

The Limits of Correctness; Prepared for the Symposium on Unintentional
Nuclear War; Fifth Congress of the International Physicians for the
Prevention of Nuclear War; Budapest, Hungary, June 28-July 1, 1985;
ACM SIGCAS Computers and Society, Volume 14,15, Issue 1,2,3,4,
pages 18-26, January 1985.

-- Michael

At 20:41 07/03/2014, Nick Tudor wrote:
>And any non formal representation of the physical world is also 
>similarly limited. Actually, in most cases, not. This is because the 
>very activity of formalisation forces the analyst to ask relevant 
>questions whereas other approaches often do not.
>
>On Thursday, 6 March 2014, Michael Jackson 
><<mailto:jacksonma at acm.org>jacksonma at acm.org> wrote:
>Peter:
>
>And course any formal model of the physical world is always limited 
>by our understanding of the physical world.
>
>
>Yes, and it's even worse than that. Formalisation is abstraction. We
>are consciously compelled to omit much that we know, judging that
>its effects will be negligibly small or will be manifested with negligibly
>small probability.
>
>-- Michael
>
>
>
>At 10:33 06/03/2014, Peter Bishop wrote:
>Michael Jackson wrote:
>Alvery:
>Yes, indeed. And a large part of the difficulty lies in formalising
>the given properties and behaviours of the domain (which it possesses
>independently of the controller) and formalising the constraints
>which the controller will impose on those properties and behaviours
>and the resultant actual behaviours that will be exhibited in system 
>operation.
>Some formal methods (for example, Event-B) do attempt formal 
>verification of the whole system (controller plus domain). Event-B is
>concerned (so far as I know) with discrete systems only. Its approach
>to formalising the physical world is not beyond criticism; but it is
>strong on formal (often automated) proofs of invariant 
>properties---safety properties in the sense of 'not liveness'. The 
>resulting formal models are still, however, very far from any
>practical implementation language for controller programs.
>
>
>And course any formal model of the physical world is always limited 
>by our understanding of the physical world.
>
>Peter Bishop
>
>Best wishes,
>-- Michael
>
>
>
>
>At 14:08 03/03/2014, GRAZEBROOK, Alvery N wrote:
>Absolutely, I agree. My point was that current practice in formal 
>methods doesn't cross this boundary. My understanding is that you 
>could define a formal methods process roughly as:
>1. Understand the safety implications of the system and define the 
>safety properties
>2. Prove that your controller behaviour is consistent with the 
>safety properties, for the domain where the controller can affect them.
>
>The "wider physical world" bit happens at step 1, and only the 
>outcome is expressed formally in the safety properties.
>
>This interpretation covers SPARK process, and a formal process using 
>SCADE. It could also be said to cover the application of proof 
>checkers to VHDL in chip-design, and formal microprocessor designs 
>or proof of properties of communication protocols. In these cases, 
>rather than define safety properties, they select a set of 
>correctness properties and prove those.
>
>I would be interested in any examples where the formal verification 
>did cross the "physical world" boundary.
>
>Cheers,
>         Alvery
>
>** the opinions expressed here are my own, not necessarily those of 
>my employer
>
>-----Original Message-----
>From: Michael Jackson [mailto:jacksonma at acm.org]
>
>Yes. Surely "taking the discussion on to the system behaviour 
>applied to the wider physical world" beyond "the control / 
>measurement systems" is what it's all about, isn't it? It's only in 
>the wider physical world that the system purpose has meaning and the 
>real costs of safety failures are felt.
>
>
>This email (including any attachments) may contain confidential 
>and/or privileged information or information otherwise protected 
>from disclosure. If you are not the intended recipient please notify 
>the sender immediately and delete this email and any attachments 
>from your system.  Do not copy this email or any attachments and do 
>not use it for any purpose or disclose its content to any 
>person.  Airbus Operations Limited disclaims all liability if this 
>email transmission has been corrupted by virus, altered or falsified.
>
>Airbus Operations Limited, a company registered in England and 
>Wales, with registration number 3468788.  Registered 
>office:  Pegasus House, Aerospace Avenue, Filton, Bristol, BS99 7AR, UK.
>
>_______________________________________________
>The System Safety Mailing List
>systemsafety at TechFak.Uni-Bielefeld.DE
>
>
>--
>
>Peter Bishop
>Chief Scientist
>Adelard LLP
>Exmouth House, 3-11 Pine Street, London,EC1R 0JH
><http://www.adelard.com>http://www.adelard.com
>Recep:  +44-(0)20-7832 5850
>Direct: +44-(0)20-7832 5855
>_______________________________________________
>The System Safety Mailing List
>systemsafety at TechFak.Uni-Bielefeld.DE
>
>
>_______________________________________________
>The System Safety Mailing List
>systemsafety at TechFak.Uni-Bielefeld.DE
>
>
>
>--
>Nick Tudor
>Tudor Associates Ltd
>Mobile: +44(0)7412 074654
><http://www.tudorassoc.com>www.tudorassoc.com
>
>77 Barnards Green Road
>Malvern
>Worcestershire
>WR14 3LR
>Company No. 07642673
>VAT No:116495996
>
><http://www.aeronautique-associates.com>www.aeronautique-associates.com