[SystemSafety] The bomb again

[Peter Bernard Ladkin]

On 10/10/13 12:39 PM, Nancy Leveson wrote:
> I have been traveling and unable to comment (just too much to type on an iPhone).

I'm somewhat pressed for time also now (something to do with writing long messages.....) but I do 
need to respond. I'm impressed at your ability with an iPhone! I used a keyboard with the iPad.

> I don't know where Peter got the impression that I ever formally verified TCAS. _I did not_!!!

Sorry, that was misleading phraseology I now see. But what I meant was not entirely wrong.
You wrote a formal requirements spec which was - obviously and necessarily - verified in certain 
ways. You did, I had thought, some formal verification. Checking, I now see that it wasn't you, but 
another team which did that.

Here is the sentence from the paper with Mats and Jon Reese where you say verification was performed:
> After the specification of the CAS logic was completed, an independent verification and validation was performed to compare
> the pseudocode specification and the RSML specification. The verifiers experienced the same problems that we did, and a
> large number of identified discrepancies between the pseudocode and the RSML specification resulted in no change to the RSML
> specification because they merely represented design peculiarities of the pseudocode and not requirements.

I can also agree now that mentioning that in the same breath as the work of Nancy Lynch was possibly 
misleading, because it is not the same kind of verification which she and her team performed.

The anonymous engineers I mentioned who claim that TCAS has been "formally verified" usually cite 
your RSML work, not Nancy Lynch's. They usually don't know about the other Nancy's team's work with 
I/O Automata. So my use of the phrase in my note is quite consistent with "folk use".

As I said previously, the words "formal verification" without context are an incomplete statement. 
One has to say *what* was formally verified against *what*. You say that the independent team 
verified the RSML spec against the pseudocode (discrepancies were found). As far as I am concerned, 
that verification is ipso facto formal because RSML is formal, and the pseudocode must have some 
semantics otherwise no verification at all could have been performed.

>   .... At no time
> did I ever do any formal analysis on TCAS....... These people took my formal specification (which most of the formal methods
> community has dismissed as not formal enough to be a formal specification

Developing a formal requirements specification and verifying it against some expression of user 
intent (here, the pseudocode) counts to me as analysis and is also formal. So, formal analysis. I 
don't think one can write any decent requirements specification without doing some analysis.

> ..... As I remember, Lincoln Labs has worked
> for at least 30 years doing trajectory analysis on various versions of TCAS/ACAS starting in the
> early 80s.

I have spoken with people who do trajectory analysis of collision avoidance algorithms. No one has 
pointed me to a solution of the trajectory problem I identified.

[Concerning the Brühl analysis and use of WBA and STAMP]

> I work in engineering, not law. Unfortunately, lots of law has fallen behind our quickly moving
> ability to engineer very complex and technologically advanced systems. To argue that the engineering
> should stop because the law has not been updated is unrealistic.

No one was arguing that, certainly not me.

> The law is going to have to catch
> up because people are not going to compromise on what they build and, in fact, have not done so.

That might be true in the US, for all I know. Here, rail equipment can't be used unless it has been 
certified by the government agency EBA, and the EBA won't certify it unless it conforms with the 
existing law. If one's kit doesn't, somebody else's does and that is what will be bought and installed.

> Also, the argument that an incident that did not hurt anyone should be ignored also seems unwise to
> me.

Yes, I think it would be unwise too. What is wise, indeed what is standard engineering practice, is 
to use severity to classify an incident. Indeed, in DB operations all typical incidents - hundreds 
of them - are classified according to severity. It is even European law now that you have to do that 
(according to CSM). But according to the notion of legal responsibility for a particular accident, 
the number of people actually killed or injured is relevant (as well as their names and other 
details of their lives), not the engineering severity.

> I'm not following Peter's argument about not changing the law because the scenario _of a real
> event_ does not follow the Counterfactual Test. It would seem to me that the event occurring shows
> that the CT is not adequate in today's engineering world.

I don't follow you here either. The STAMP analysis identified certain features of DB procedures 
which were not causally implicated in the accident according to the CT. Therefore, according to the 
usual legal criteria, they were not causally implicated in the accident. That is the definition of 
cause which the law uses. I suggested that proposing to change German railroad law because of an 
accident in which the features one wants changed are not causally implicated is a non-starter. You 
are welcome to regret that. You are also welcome to try to change the German legal understanding of 
"cause" if you like.

PBL

Prof. Peter Bernard Ladkin, Faculty of Technology, University of Bielefeld, 33594 Bielefeld, Germany
Tel+msg +49 (0)521 880 7319  www.rvs.uni-bielefeld.de