In this repository are the models used in my thesis "Formal Network Behaviour Analysis using Model Checking" (https://eprints.qut.edu.au/93693/).
To perform the checks in the topologies, install git and the Symbolic Analysis Laboratory (http://sal.csl.sri.com) on either Linux or MacOS, then execute the run.sh script. If executed without the argument of a topology file name (e.g. ./run.sh topology1.sal), it will sequencially perform the checks in all topology files. The output of the checks can be found in the Data directory. Please read Section 1.6 of the thesis and the run.sh file itself for more information.
Copyright 2016 Douglas Graeme Brown. All rights reserved.