[SystemSafety] Static Analysis

[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 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
>Recep:  +44-(0)20-7832 5850
>Direct: +44-(0)20-7832 5855
>_______________________________________________
>The System Safety Mailing List
>systemsafety at TechFak.Uni-Bielefeld.DE