Re: [SystemSafety] Static Analysis

From: Michael Jackson < >
Date: Sat, 08 Mar 2014 09:50:19 +0000


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.

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
>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_xxxxxx >
>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_xxxxxx >
>
>--
>
>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_xxxxxx >
>
>_______________________________________________
>The System Safety Mailing List
>systemsafety_at_xxxxxx >
>
>
>--
>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



The System Safety Mailing List
systemsafety_at_xxxxxx Received on Sat Mar 08 2014 - 10:50:33 CET

This archive was generated by hypermail 2.3.0 : Sun Apr 21 2019 - 00:17:07 CEST