The Fortuna Model Checker

We introduce Fortuna, the first tool for model checking priced probabilistic timed automata (PPTAs). Fortuna can handle the combination of real-time, probabilistic and cost features. This is required for addressing key design trade-offs that arise in many practical applications such as the Zeroconf, Bluetooth, IEEE802.11 and Firewire protocols, protocols for sensor networks, and scheduling problems with failures. PPTAs are an extension of probabilistic timed automata (PTAs) with cost-rates and discrete cost increments on states. Fortuna is able to compute the maximal probability by which a state can be reached under a certain cost-bound (and time-bound). Although this problem is undecidable in general, there exists a semi-algorithm that produces a non-decreasing sequence of probabilities converging to the maximum. Fortuna uses a number of crucial optimizations on that algorithm. We compare the performance of Fortuna with existing approaches for PTAs. Surprisingly, although PPTAs are more general, our techniques exhibit superior performance.

 goddess Fortuna or Tyche

More information can be found in the next and the related publications at the end of this page:

mcpta models

In the PhD thesis of Jasper Berendsen, Fortuna was compared to the mcpta tool. The ZIP file mcpta_models.zip contains a README and the models and scripts that were used in the comparison.

Download

Fortuna is distributed under the terms of the GNU General Public License version 3.

Disclaimer: Fortuna is still in its early development stages. We apologize for any bugs, but can not assume any responsibility for the correctness of the results or any damages caused.

The complete source code can be downloaded here.

Getting Started

The directory Release contains an executable that runs the case studies from the paper/technical report. The executable is compiled for a standard PC running Linux. If the executable does not run on your computer, you need to compile Fortuna yourself. To run the executable see/run the Bash script Release/fortuna.sh.

Fortuna displays the number of steps taken and the maximum probability on standard output. More verbose information is written to the file "systemLog.txt". Fortuna depends on a number of shared libraries from external parties. Versions of these libraries for a standard PC running Linux are included in the distribution. See below which libraries these are.

Fortuna is still in its early stages. For now the PPTA model is compiled into the executable which can then be run to do the model checking. Therefore, when doing your own models compiling Fortuna yourself is necessary. The PPTA model should reside in the file src/model.h which can be found in the src directory in the distribution. Initially model.h contains the case studies of the paper. From these examples it becomes clear how a parallel composition of PPTAs can be built with helper functions, that allow for a nice syntax. Turning of some optimizations like in the paper can be done by removing the definitions HASSEDIAGRAM and GOSUPERZONE in the file src/defines.h and compiling.

Fortuna was developed in C++ using Eclipse together with Eclipse C/C++ Development Tooling - CDT, and the GCC C++ Compiler 4.3.3. We recommend using Eclipse for making changes and compiling Fortuna. The Fortuna distribution contains the complete Eclipse project. For small changes that do not change the source files being used (like removing HASSEDIAGRAM), it may suffice to run the command "make" at the command prompt in either the subdirectory Release or Debug.

External Libraries

Fortuna depends on a number of external libraries. The libraries needed to run the executable as it comes with the distribution are included. Note that when you are compiling Fortuna yourself you may need to install the libraries yourself. Libraries are looked up in fortuna/lib, fortuna/Debug/lib (only for the Debug version), and in the standard path (e.g. /usr/lib. Headers are looked up in fortuna/include, and in the standard path (e.g. /usr/include. In Ubuntu the libraries can all be simply installed using the Synaptic Package Manager. The external libraries are the following:

The paths used by the Eclipse project have the typical settings for the used libraries. However, these settings may be different for your system. They are the following:

Background Information script fortuna.sh

To run the executable one needs to dynamically link to the libraries. At the command prompt the easiest way is to set the variable LD_LIBRARY_PATH or something similar. Typically this is done by a command of the following form:

export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:gmp_path:gmpxx_path:ppl_path:lpsolve55_path

, where gmp_path, gmpxx_path, ppl_path, and lpsolve55_path are the paths to the gmp, gmpxx, ppl, and lpsolve55 libraries, respectively.

Contact

For questions, suggestions or comments, please contact Jasper Berendsen under J dot Berendsen at cs dot ru DOT nl.

Related Publications