MUNTA is

• a model checker for the popular realtime systems modeling formalism of Timed Automata
• formally verified with Isabelle/HOL: there is a machine-checked proof that it only computes correct results!

MUNTA is at an early stage of development. Nevertheless, you can:

• run the model checker on a number of benchmarks
• browse the Isabelle/HOL proof
• try its graphical user interface here

MUNTA now features a graphical user interface:

• try it
• source code
• instructions on how to run the verification server

The following instructions should work on all Unix systems.

Install the MLton compiler. Then run:

cd ML
make

Install Isabelle and the AFP. Then run:

isabelle jedit -l Refine_Imperative_HOL

and open one of the .thy files. A good starting point is the file where the model checker is exported to executable code: Simple_Networks/Simple_Network_Language_Export_Code.thy.

Install Isabelle and the AFP. Then run:

isabelle build -d . TA_Code

and build the checker as described above.

After building, you can run the verification server via:

cd ML
python2 server.py

The server will run under port 3069 and communicates with the GUI.

Pick one of the .muntax files from benchmarks and run:

ML/munta -m benchmarks/<the_benchmark>.muntax

To list MUNTA's command line options, run:

ML/munta -h

MUNTA accepts a simple modeling language, which is formally described in the file Simple_Networks/Simple_Network_Language.thy. Input models and formulas are specified in the JSON format (MUNTA's file ending: .muntax). Examples can be found in the folder benchmarks.

The benchmarks are derived from the UPPAAL and TChecker benchmarks.

The following instructions are outdated and in the progress of being updated:

MUNTA is aimed at understanding bytecode produced by UPPAAL. However, for the time being, this bytecode needs to be pre-processed slightly. You can find some pre-processed benchmarks in benchmarks. The input format is documented in UPPAAL_Asm.thy and ML/Checker.sml.

Replace Big_int with Big_int_Z in UPPAAL_Model_Checker.ml and to_int with int_of_big_int. Then run

cd ML
ocamlfind ocamlopt -package zarith -package angstrom -linkpkg nums.cmxa -linkpkg UPPAAL_Model_Checker.ml -linkpkg Checker.ml

Human readable .pdf documents (with textual annotations) of the formalizations can be produced by Isabelle. Run

isabelle build -d . TA
isabelle build -d . TA_All

and you will get the following:

• output/abstract_reachability.pdf: the abstract formalization of reachability checking for Timed Automata
• output/model_checking.pdf: the formalization of MUNTA and the route from the abstract formalization to the correctness proof for MUNTA
• output/abstract_reachability_proofs.pdf, output/model_checking_proofs.pdf: variants of the above documents with proofs