[SystemSafety] Static Analysis

[Peter Bishop]

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