In Greek mythology, Urania was able to foretell the future by the possition of the stars.
In the computer age, MUSE is able to foretell the future faults by the Java byte-code.



MUSE - Model checking Using Symbolic Execution


Contents

  1. Introduction
  2. Requirements
  3. Download
  4. Installation
  5. Tool execution
  6. Related projects
  7. Authors
  8. Acknowledgement

1. Introduction

MUSE is a prototype implementation of a tool for verification of LTL properties against Java byte-code which uses symbolic execution technique for combatting the state space explosion problem.

Further informations about our approach can be found in:

  1. P. Braione, G. Denaro, M. Pezze, and B. Krena: Verifying LTL Properties of Bytecode with Symbolic Execution, Bytecode 2008, [pdf]

2. Requirements

  1. Java SE Development Kit 6
  2. Eclipse IDE for Java Developers - in principle, MUSE can be compiled and executed without Eclipse, however, we encountered some problems under the command line.
  3. GNU C/C++ compiler g++ and make - we assume that they are already present under any reasonable UNIX/Linux evnironment while they can be installed under MS Windows operating systems through Cygwin - a Linux-like environment for Windows.
  4. SICStus Prolog or CVC3 is used for expression simplification which is not essential part of symbolic execution, however, it usually leads to a significant reduction of state space provided by symbolic execution. Unfortunately, SICStus Prolog is not available free of charge while CVC3 makes symbolic execution very slow.
  5. Spin or LTL2BA serves for translating LTL formulae to Büchi automata.
  6. JavaCC™ - Java Compiler Compiler™ is used for building a translator from Büchi automata to Java source code.

3. Download

The core of the MUSE tool can be downloaded here.
SICStus interface that is not necessary for MUSE execution can be downloaded separatelly here.
MUSE tool as well as SICStus interface can be used under GNU General Public License.


4. Installation

WARNING: MUSE is a research prototype tool and not one-push-button solution. During its development, we have concentrated on the core ideas (e.g., symbolic execution, LTL model checking) much more than on the easy to use interface. We are sorry for the discomfort of the user, however, the intention of sharing the tool is not to provide ready-to-use tool but to share the ideas inside the tool and the effort already dedicated for its development with other researchers interested in using symbolic execution (not only) for model checking.

  1. Install all the required tools listed in the Requirements section.
  2. Download and expand the zip file(s) provided in the Download section.
  3. Check the path setting in muse/scripts/set_environment.bat and execute it or use it for inspiration for path settings in your environment when the batch does not work properly in your operating system.
  4. When do you want to use SICStus prolog for expression simplification make sure that you have downloaded and expanded SICStus interface and use usual command make (or make clean for cleaning) in the SicstusInterface directory. You will obtain SIIF.exe executable file that should be used for starting SICStus prolog engine before the MUSE tool.

5. Tool execution

1. Manual instrumentation of source code

We have manually injected some instrumentation (i.e., variables _AP0 and _AP1) into this code in order to be able check whether appropriate atomic propositions hold or not whithin the symbolic execution.

2. Description of the LTL property

We describe an LTL property we are interested in. The property can contain only atomic propositions that we have injected into the source code within Step 1. Some examples of such properties can be found in ./pc_spin427/ directory, for instance, 'ForG.ltl' file contains property '<> ( ([] ap0) || ([] ap1) )' which means that at each execution path, property 'ap0' or property 'ap1' will hold from some position forever.

3. Translation from LTL to Buchi automaton

Spin can be used (under Cygwin) for translation from LTL formulae to Buchi automata in so-called "never claim" form. For instance, Test/ListSorting/props/For.ltl contains the LTL formula "<> ( ap0 || ap1 )" used in ListSortingExample. After translation ./spin.exe -F For.ltl > For.nc we get the following Buchi automaton (in For.nc):
never {    /* <> ( ap0 || ap1 ) */
T0_init:
	if
		:: ((((ap0)) || ((ap1)))) -> goto accept_all
		:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}
which can be used (after some unnecessary brackets removing) as the input of ba2j translator and then as the input of MCEngine. After the translation, the Buchi automaton should be checked and some unnecessary brackets can be removed.

4. Translation of Buchi automaton from Never claim to Java

The translator from Never claim to Java source code is in in the directory ./ba2j and it was built by javacc tool (which is in ./javacc directory). When the translator modification needed, see ./ba2j/ba2j.jj and ./ba2j/compile.bat (./javacc/bin must be in the path). The translation can be invoked by the command: java ba2j For > For.java which takes as an input the file For.nc and put the result to the file For.java.

5. Model checking compilation

The model checker is in the directory ./MCEngine. When the all java files including java files of properties are here the compilation can be done by standard javac (for more see compile.bat).

6. Model checking

Start the Sicstus simplifier (by ./linuxCaveat/SIIS.exe under cygwin). Start the model checking by 'run.bat' with the name of the property as a parameter (e.g., 'run.bat ForG'). The verification result including a Buchi automata, process of execution, and eventual state that violates the property will appear in 'For.txt'.

6. Related projects


7. Authors

Pietro Braione (1) - symbolic execution part
Giovanni Denaro (1) - symbolic execution part
Mauro Pezzè (1,2) - project supervision
Bohuslav Křena (3) - model checking part, this web page

Institutions:

  1. Laboratory of Test and Analysis, Dipartimento di Informatica Sistemistica e Comunicazion, Universita degli Studi di Milano - Bicocca, Italy
  2. Faculty of Informatics, University of Lugano, Switzerland
  3. Faculty of Information Technology, Brno University of Technology, Czech Republic

8. Acknowledgment

Research and development of this tool has been supported by:
Feel free to send questions, remarks, comments, or thanks to Bohuslav Křena via e-mail krena@fit.vutbr.cz. Last update: 07/14/09 12:36:42 CEST