|
      |
Model Checker for Validating Other Model Checkers
|
Hyunjun Eo and
Nikolay Shilov
ROPAS
Computer Science
Korea Advanced Institute of Science and Technology
Introduction
Model checking is an important technique to verify the correctness of software and hardware systems.
Validation of model checkers is a very important issue due to their automatic nature. In general there are two approaches to validation:
- extensive testing,
- formal verification.
Manual extensive testing of model checkers seems to be problematic since test-generation is a non-trivial problem.
A formal verification can be an alternative to manual exhaustive testing, but formal verification of model checkers is a new developing research domain.
We conjuncture that the most appropriate approach to validation of model checkers is an overall automatic testing against a formally verified reliable model checker on automatically generated test suits. In this case, the reliable model checker should be easy to verify.
|
Our reliable model checker consists of three parts FC, GC, and MC.
- FC is a formula compiler which interprets muC(,CTL,LTL,2M,...) in an auxiliary second order propositional logic SOEPDL.
- GC is a game compiler which construct model checking finite games for finite models and SOEPDL formulae.
- MC is a specialized model checker for muC formula WIN which expresses an existence of a winning strategy in finite games.
A modified 4x4 American checker game can be verified by MC.(result)
Each part is simple, transparent, and easy-to-verify
|
Implemenation
Our goal is implementing model checker in nML and C, and comparing both implementations in performance and transparency.
Currently, we implemented model checker in nML(tar.gz).
Input model is a famous problem - a man with a wolf, goat, and cabbage crossing a river.
- It has 10 states, 4 action variables, and 4 propositional variables.
- Size of input formula is 21. It has 1 fixpoint operation.
- Checking this model takes about 10 minutes, and 150MB memory.
Papers
-
Easy-to-verify Model Checker for Propositional Mu-Calculus in Finite Models
[ps/
abstract]
Nikolay V. Shilov and Kwangkeun Yi,
draft
-
A Note on Model Checkers Reuse
[ps/
abstract]
Nikolay V. Shilov and Kwangkeun Yi,
submitted to Information Processing Letters
-
A Note on Model Checking Reuse
[ps.gz/
bibtex/
abstract]
Nikolay V. Shilov and Kwangkeun Yi,
2nd Australasian Workshop on Computational Logic AWCL'01,
Gold Cost, Australia, Jan 31 - Feb 1, 2001
-
A Note on Model Checkers Reuse and Validation
[ps.gz/
bibtex/
abstract]
Nikolay V. Shilov and Kwangkeun Yi,
First Asian Workshop on Programming Languages And Systems,
Singapore, Dec 18-20, 2000