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:

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.

Papers