EFSM models fit nicely with the notion of model checking. We can therefore express properties over EFSMs in LTL and check that these properties are true with a model checker. We present a toolset to convert EFSM models and LTL properties between the Isabelle theorem prover and the SAL model checker. This repository demonstrates our toolset with four case studies.
This repository makes reference to several submodules. When cloning this repository, you should do so with the --recursive
option, i.e. git clone --recursive https://github.com/jmafoster1/efsm-sal.git
You can build the jars from source by simply running make
or make build
from within the efsm-sal
top level directory. This will compile the sources and create a directory called jars
in which to place the compiled .jar
files for the three utilities. These can then be run with java -jar jars/jarname.jar
, in which jarname
is one of the three tools listed below. Of course, this requires Java to be installed on your computer.
Instead of building from the source code, you can simply download precompiled jar files by clicking on "releases".
Our toolset is designed to work with the Symbolic Analysis Laboratory (SAL) model checker. You need to have this installed on your system. Full installation instructions can be found here.
In order to run SAL on these examples, you need to have the lib
directory location in your SALCONTEXTPATH
environment variable. You can set this variable in your .bashrc
file if you're using bash. If you're not using bash, you're on your own!
Our toolset is designed to work with the Isabelle/HOL theorem prover. Full install instructions can be found (here)[https://isabelle.in.tum.de/installation.html].
###AFP Our toolset makes reference to the Extended Finite State Machine entry in Isabelle's Archive of Formal Proofs, which must be [installed separately][https://www.isa-afp.org/using.html] to Isabelle/HOL. The Extended Finite State Machine entry is available from 2020 onwards. If you are using an older version, you will need to upgrade or manually install the entry.
Please note that the reference name changed from EFSM
to Extended_Finite_State_Machines
between the 2020 and 2021 releases. Our tool supports the 2021 name. If you are using the 2020 version, you will need to either update the entry or manually change import Extended_Finite_State_Machines.EFSM
to import EFSM.EFSM
at the top of any generated theory files.
Our tools are located in the jars
directory. Each can be run using java -jar TOOLNAME.jar file/to/convert
, where file/to/convert
is the filepath of the file to convert, and TOOLNAME
is one of the following:
dot2isabelle
- converts DOT files representing EFSMs into an Isabelle representation. This enables EFSMs to be edited graphically. For examples of the syntax to use, see theexamples
directory.isabelle2sal
converts Isabelle representations of EFSMs and LTL properties to SAL for quick and easy counterexample generation.sal2isabelle
converts SAL EFSMs and properties to Isabelle to enable coinductive proofs for the strongest assurance.
If called without a file argument, all three tools will bring up a file chooser window.
Our repository contains a makefile with several supported commands.
dot
- Converts DOT files to PDFs for easy viewingclean
- deletes Isabelle temporary filescleanall
- deletes Isabelle temporary files, dot files, PDF files, and SAL files. This is used for testing and assumes that Isabelle theories are the "original".
The examples
directory also contains a makefile, with several commands relating to the examples.
clean
- similar tocleanall
above but also removes temporary files (e.g. error logs) created by our toolset.testwf
- runs the SAL wellformedness checker on the examples.testsal
- executes SAL on all theorems to ensure they pass and fail as expected.dot
- Same asdot
above.