Re: [SystemSafety] Static Analysis

From: Peter Bishop < >
Date: Thu, 06 Mar 2014 10:33:10 +0000

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
Recep:  +44-(0)20-7832 5850
Direct: +44-(0)20-7832 5855
The System Safety Mailing List
Received on Thu Mar 06 2014 - 11:33:28 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:06 CEST