RE: [sc] Testing
> 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 [email@example.com] On Behalf Of Peter Bernard Ladkin [ladkin@xxxxxx]
Sent: Tuesday, June 28, 2011 4:27 PM
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 www.rvs.uni-bielefeld.de
Received on Fri 01 Jul 2011 - 17:08:49 BST