[SystemSafety] Static Analysis

[Nick Tudor]

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 <jacksonma at acm.org> wrote:

> 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
>>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
>


-- 
Nick Tudor
Tudor Associates Ltd
Mobile: +44(0)7412 074654
www.tudorassoc.com

*77 Barnards Green Road*
*Malvern*
*Worcestershire*
*WR14 3LR*
*Company No. 07642673*
*VAT No:116495996*

*www.aeronautique-associates.com <http://www.aeronautique-associates.com>*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20140307/3b1679d6/attachment.html>