pefribeiro / csp-prover Goto Github PK

           (*-------------------------------------------*
            |                                           |
            |             << CSP-Prover >>              |
            |                                           |
            |                August 2004                |
            |               January 2005  (modified)    |
            |              February 2005  (modified)    |
            |                  June 2005  (modified)    |
            |                  July 2005  (modified)    |
            |              November 2005  (modified)    |
            |                 April 2006  (modified)    |
            |             September 2006  (modified)    |
            |                August 2007  (modified)    |
            |              February 2008  (modified)    |
            |                  July 2008  (modified)    |
            |                  July 2009  (modified)    |
            |               January 2010  (modified)    |
            |               October 2010  (modified)    |
            |                 April 2011  (modified)    |
            |              November 2012  (modified)    |
            |                  June 2013  (modified)    |
            |                   May 2016  (modified)    |
            |                                           |
            |            (on Isabelle 2016)             |
            |                                           |
            |        Yoshinao Isobe    (AIST JAPAN)     |
            |        Markus Roggenbach (SU UK)          |
            |                                           |
            *-------------------------------------------*)

1. Introduction

CSP-Prover [1,2,3,4] is an interactive theorem prover dedicated to
refinement proofs within the process algebra CSP [5]. It aims
specifically at proofs on infinite state systems, which may also
involve infinite non-determinism.


2. Directory

      CSP-Prover ---+--- CSP
                    |
                    +--- CSP_T
                    |
                    +--- CSP_F
                    |
                    +--- FNF_F
                    |
                    +--- DFP
                    |
                    |
                    +--- ep2
                    |
                    +--- DM
                    |
                    +--- Test
                    |
                    +--- SA_Kung
                    |
                    +--- NBuff
                    |
                    +--- UCD

o CSP    : the reusable part of CSP-Prover

o CSP_T  : the instantiated part for T

o CSP_F  : the instantiated part for F

o FNF_F  : full normalising for F

o DFP    : (Deadlock Freedom Proof) on CSP_F, theorems given in [6]

o ep2    : an example (electronic payment system) on CSP_F

o DM     : an example (Dining Mathematicians) on CSP_F

o Test   : small examples on CSP_F

o SA_Kung: an example on DFP (Kung's Systolic array [3])

o NBuff  : an example (Linked n one-buffers)

o UCD    : an example (Uniform Candy Distribution Puzzle [1])


3. Installation

This CSP-Prover needs Isabelle2016.  

At first, the environment-variable "CSP_PROVER_HOME" is set to
the directory containing CSP, CSP_T,..., and ROOT of CSP-Prover.

To make heap-files of CSP, CSP_T, CSP_F, and FNF_F once, execute the
command "make_heap" in this directory (CSP_PROVER_HOME).

Please read "User Guide CSP-Prover". The latest version can be
downloaded from the CSP-Prover's web-site:

   http://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html

4. User interface

To start Iasbelle/jEdit with the logic of CSP_F, execute the following
command:

   isabelle jedit -d '$CSP_PROVER_HOME' -l CSP_F

5. Licence agreement

Following the ideas of open source software, we allow anyone to use
CSP-Prover without fee, under the CSP-Prover licence, which is similar
to the Lesser Gnu Public License (LGPL). The details are given in

   http://staff.aist.go.jp/y-isobe/CSP-Prover/licence.txt

You have to agree with the licence before using CSP-Prover.


6. X-symbols

X-symbols are used for expressing conventional CSP operators in
CSP-Prover, but X-symbols may causes some warnings on syntax.
Therefore, we separated the definitions of X-symbols from the main
definitions and theorems, and collected them into new files
"CSP_*_xsymbols". If you do not use X-symbols of CSP-Processes, it is
recommended to use the theories

  CSP_Main, CSP_T_Main, and CSP_F_Main,

instead of

  CSP, CSP_T, and CSP_F.

CSP_*_Main contains all the definitions and theorems of previous
CSP-Prover except the definitions on X-symbols, and CSP_* imports
CSP_*_Main and CSP_*_xsymbols.


References

[1] Y.Isobe and M.Roggenbach: CSP-Prover -- a Proof Tool for the
    Verification of Scalable Concurrent Systems, Journal of Computer
    Software, Japan Society for Software Science and Technology
    (JSSST), Vol.25, No.4, pp.85--92, 2008.

[2] Y.Isobe and M.Roggenbach: A complete axiomatic semantics for the
    CSP stable-failures model, CONCUR 2006 (17th International
    Conference on Concurrency Theory), LNCS 4137, Springer,
    pp.158-172, August 2006.

[3] Y.Isobe, M.Roggenbach, and S.Gruner, Extending CSP-Prover by
    deadlock-analysis: Towards the verification of systolic arrays,
    FOSE 2005 (12th Workshop on Foundation of Software Engineering),
    Japanese Lecture Notes Series 31, pp.257-266, Kindai-kagaku-sha,
    November 2005.

[4] Y.Isobe and M.Roggenbach: A generic theorem prover of CSP
    refinement, TACAS 2005 (11th Inter\national Conference on Tools
    and Algorithms for the Construction and Analysis of Systems), LNCS
    3440, Springer, pp.108-123, April 2005.

[5] A.W.Roscoe, "The Theory and Practice of Concurrency",
    Prentice Hall, 1998.

[6] A.W.Roscoe and N.Dathi, "The pursuit of deadlock freedom",
    Information and Computation, Vol.75, No.3, pp.289-327, 1987.