[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[patch #5873] Model checker and initial datasheet review

From: Ben Pfaff
Subject: [patch #5873] Model checker and initial datasheet review
Date: Wed, 18 Apr 2007 23:28:42 +0000
User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv: Gecko/20061205 Iceweasel/ (Debian-


                 Summary: Model checker and initial datasheet review
                 Project: PSPP
            Submitted by: blp
            Submitted on: Wednesday 04/18/2007 at 16:28
                Category: None
              Item Group: None
                  Status: Ready For Test/Review
             Assigned to: None
        Originator Email: 
             Open/Closed: Open
         Discussion Lock: Any



This set of changes implements a model checker and a PSPP syntax interface to
the model checker.  My goal is to check these into the main branch after
applying reviewers' comments; they are already in the simpler-proc branch.

These changes also include the current draft of the datasheet implementation
for use by the GUI.  This is because the datasheet code is currently the
model checker's only client, so it can serve as an example use of the model
checker for the enlightenment of reviewers.  I don't intend to immediately
check the datasheet code into the main branch, because it depends on the
casereader code that isn't yet in the main branch (and is not itself ready
for check-in), and because the datasheet's name is likely to change before
final check-in (and I don't think we came to a final decision on its new
name).  I'd still be happy to receive any or all feedback on the datasheet's
code or design.

A model checker is a tool for software testing and verification
that works by exploring all the possible states in a system and
verifying their internal consistency.  A conventional model
checker requires that the code in a system be translated into a
specification language.  The model checker then verifies the
specification, rather than the code.

This is instead an implementation-level model checker, which does
not require a separate specification.  Instead, the model checker
requires writing a second implementation of the system being
checked.  The second implementation can usually be made almost
trivial in comparison to the one being checked, because it's
usually acceptable for its performance to be comparatively poor,
e.g. O(N^2) instead of O(lg N), and thus to use much simpler

The "models" used by model checkers have little or nothing to do with the
"models" used in statistics.  I didn't use the prefix "model_" for that
reason; PSPP is about statistics, not about model checking, so it seems
better to reserve "model_" for statistical purposes.


File Attachments:

Date: Wednesday 04/18/2007 at 16:28  Name: datasheet.tar.gz  Size: 32kB   By:



Reply to this item at:


  Message sent via/by Savannah

reply via email to

[Prev in Thread] Current Thread [Next in Thread]