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 [safety-critical-request@xxxxxxk.ac.uk] 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.

PBL

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  www.rvs.uni-bielefeld.de
Received on Fri 01 Jul 2011 - 17:08:49 BST