[SystemSafety] Static Analysis

[GRAZEBROOK, Alvery N]

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.