Fully verified model checker for realtime systems
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
ML
Worklist_Algorithms
benchmarks
document
library
.hgignore
.travis.yml
Approx_Beta.thy
Bisimilarity_Abstraction.thy
Closure.thy
DBM.thy
DBM_Basics.thy
DBM_Normalization.thy
DBM_Operations.thy
DBM_Operations_Impl.thy
DBM_Operations_Impl_Refine.thy
DBM_Zone_Semantics.thy
Export_Checker.thy
FW_Code.thy
FW_More.thy
Floyd_Warshall.thy
Infinite_TA_Runs.thy
LICENSE
Networks.thy
Networks_Impl.thy
Networks_Impl_Refine.thy
Normalized_Zone_Semantics.thy
Normalized_Zone_Semantics_Impl.thy
Normalized_Zone_Semantics_Impl_Extra.thy
Normalized_Zone_Semantics_Impl_Refine.thy Added state counting in HOL and fixed issue with free type variables Feb 23, 2018
Normalized_Zone_Semantics_Impl_Semantic_Refinement.thy Cleaning. Use more abstract notions for proofs about reachability Nov 8, 2017
Paths_Cycles.thy
README.md
ROOT
Reachability_Benchmarks.thy
Recursion_Combinators.thy
Regions.thy
Regions_Beta.thy
Sepref_Acconstraint.thy
Simulation_Graphs.thy
Simulation_Graphs_Certification.thy
Simulation_Graphs_TA.thy
State_Networks.thy
State_Networks_Impl.thy First executable code for networks of TA with discrete state Nov 21, 2016
State_Networks_Impl_Refine.thy
Subsumption_Graphs.thy
TA_Impl_Misc.thy
TA_Misc.thy
TA_More.thy
Timed_Automata.thy
UPPAAL_Asm.thy
UPPAAL_Asm_Clocks.thy
UPPAAL_Model_Checking.thy
UPPAAL_Reachability_Benchmarks.thy
UPPAAL_State_Networks.thy
UPPAAL_State_Networks_Impl.thy
UPPAAL_State_Networks_Impl_Refine.thy
UPPAAL_State_Networks_Impl_Refine_Calc.thy Fixes Nov 14, 2017

README.md

MUNTA -- Fully Verified Model Checker for Timed Automata

Introduction

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

Graphical User Interface

MUNTA now features a graphical user interface:

Building

The following instructions should work on all Unix systems.

To build the checker:

Install the MLton compiler. Then run:

cd ML
make

To build the checker with OCaml:

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

To browse the sources interactively in Isabelle:

Install Isabelle and the AFP. Then run:

isabelle jedit -l Refine_Imperative_HOL

and open one of the .thy files.

To build the Isabelle sources and extract the checker source code:

Install Isabelle and the AFP. Then run:

isabelle build -d . TA_Code

and build the checker as described above.

Verification Server

After building, you can run the verification server via:

cd ML
python server.py

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

Running

Pick one of the files from benchmarks and run:

ML/munta < benchmarks/<the_benchmark>.munta

Documentation

Input Format

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.

Isabelle Formalizations

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

Benchmarks

The benchmarks are derived from the UPPAAL and TChecker benchmarks.