Model Checking in Education (MCiE)

The purpose of the Model Checking in Education (MCiE) project is to demonstrate the implementation of a symbolic model checker based on ROBDDs.

See:
          Description

Packages
de.upb.swt.mcie.formulas This package implements formulas, which can be state formulas, transition formulas or temporal formulas.
de.upb.swt.mcie.mc This package implements models with the corresponding model checking procedures, and the main method for invoking the model checker.
de.upb.swt.mcie.parser This package implements a parser and compiler for formulas and models.
de.upb.swt.mcie.parser.token This package implements the tokens for the scanner and parser of package de.upb.swt.mcie.parser.
de.upb.swt.mcie.robdds This package implements reduced ordered binary decision diagrams (ROBDDs).

 

The purpose of the Model Checking in Education (MCiE) project is to demonstrate the implementation of a symbolic model checker based on ROBDDs. It was implemented by Ekkart Kindler as supplementary material for the students of the course on model checking in the winter term 2003/04 at Paderborn University.

Since this first course, MCiE has been extended and improved when used in other projects and during the course "Advanced Topics on Software Engineering" at Denmark's Technical University.

Since the main purpose of this application was educational, it is not particularly tuned to efficiency, but for a clear structure and a safe usability of the libraries. At some places in the code, comments indicate what could be done for improving efficiency - apart from using a compiled programming language such as C instead of Java.

Release notes


Copyright (C) 2004, 2006 Ekkart Kindler, University of Paderborn, kindler@upb.de

Copyright (C) 2009, 2010 Ekkart Kindler, Denmark's Technical University (DTU), eki@imm.dtu.dk

The MCiE project is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; version 2 of the License.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA

Version:
0.3.7
Author:
Ekkart Kindler