Re: [SystemSafety] Static Analysis

From: Michael Jackson < >
Date: Mon, 03 Mar 2014 17:50:53 +0000


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

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,

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.
> 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 Received on Mon Mar 03 2014 - 18:50:59 CET

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