RE: [sc] Testing

RE: [sc] Testing

From: Robert Schaefer <schaefer_robert_at_xxxxxx>
Date: Fri, 1 Jul 2011 12:08:35 -0400
Message-ID: <F3393DEC5D93334E9D99DC587C2DA082132B923087@xxxxxx>
> Suppose, rather than testing, I had asked about books that would tell me about model checking.

How do you believe that a model (to be tested) is any different from any specification (whose implementation may be a model (to be tested))?
From: safety-critical-request@xxxxxx [] On Behalf Of Peter Bernard Ladkin [ladkin@xxxxxx]
Sent: Tuesday, June 28, 2011 4:27 PM
To: safety-critical@xxxxxx
Cc: Martyn Thomas
Subject: Re: [sc] Testing

Suppose, rather than testing, I had asked about books that would tell me about model checking.

On 6/28/11 2:21 PM, Martyn Thomas wrote:
> It seems to me that Peter's question starts in the wrong place. Surely the place to start is with the
> question "what do I need to know" then "how can I find it out?". If "[model checking]" is the answer to
> the second question then the nature of the [model checking] should be self-evident. Otherwise, how would
> you know it was the right answer?

I don't think, having done it and published on it, that it is at all "self-evident" how one goes
about designing model-checking procedures for arbitrary properties that I might wish to assess. I
need a book, say, such as Holzmann's on SPIN, to tell me how I go about it in general. Or a
collection of a few dozen or hundred conference papers, whatever one prefers. I almost always prefer
a (tasteful) book; if there isn't one, I wonder why not.

(That is why I was a little flumoxed about testing. If it is so thorough and well-understood and
apparently well-served by 30-year-old conferences at which lots goes on, why did it seem to me that
all the books were OOP? I suspect, looking again at Beer and Peischl, that the references in the
standards just haven't been updated for - in 61508's case, 13 years. So the then-hot books are OOP.
But there are still only two references to new texts. Almost as bad as safety, indeed.)

> As for the ontology of [model checking]. I'd like to ask, for each form of [model checking], precisely
> what you know after the [model checking] that you did not know before.

Whether the property you are checking for is satisfied, to a certain confidence level (model
checking need not be exact, but may sample the problem space) or whether there is a counterexample.
Much the same, indeed, as with any sort of test.


Peter Bernard Ladkin, Professor of Computer Networks and Distributed Systems,
Faculty of Technology, University of Bielefeld, 33594 Bielefeld, Germany
Tel+msg +49 (0)521 880 7319
Received on Fri 01 Jul 2011 - 17:08:49 BST