[SystemSafety] Static Analysis

[Michael Jackson]

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.

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.