|
3210
|
1 |
<HTML><HEAD><TITLE>HOL/Modelcheck/Readme</TITLE></HEAD><BODY>
|
|
|
2 |
|
|
|
3 |
<H3>Invoking Model Checkers in Isabelle/HOL </H3>
|
|
|
4 |
|
|
|
5 |
Authors: Olaf Mueller, Jan Philipps, Robert Sandner<BR>
|
|
|
6 |
Copyright 1997 Technische Universität München<P>
|
|
|
7 |
|
|
|
8 |
|
|
|
9 |
This directory contains four theories:
|
|
|
10 |
|
|
|
11 |
<UL>
|
|
|
12 |
<li>MuCalculus: A formalization of the relational mu calculus using the fixed point
|
|
|
13 |
theory Lfp and Gfp of HOL.<P>
|
|
|
14 |
<li>CTL: A formulation of some CTL operators in the mu calculus.<P>
|
|
|
15 |
<li>MCSyn: The definition of the output syntax "Eindhoven" tailored for the the model checker due to G. Janssen from Eindhoven using
|
|
|
16 |
the print_mode facilities provided by Isabelle. <P>
|
|
|
17 |
<li>Example: A simple reachability property is formulated in the mu calculus and checked
|
|
|
18 |
by the model checker simply by invoking the tactic mc_tac.
|
|
|
19 |
</UL>
|
|
|
20 |
|
|
|
21 |
Note: The example illustrates the use of the print_mode facility even without actually using the model checker. However, if you like to see the example in full functionality, get the Eindhoven model checker from here (<A HREF="http://www4.informatik.tu-muenchen.de/~mueller/tools.html">Eindhoven Model Checker</A>). It is provided as a Sparc SunOS4 binary which also runs under Solaris2.x.
|
|
|
22 |
|
|
|
23 |
|
|
|
24 |
|
|
|
25 |
</BODY></HTML>
|
|
|
26 |
|
|
|
27 |
|
|
|
28 |
|