Companion Software Installation and Configuration

For each following third party toolkit, we explain:
  • What is the use of the toolkit, i.e., for which purpose TTool uses it.

  • How to configure TTool so that it can use that third party toolkit.
  • An xml configuration file can be provided as input to TTool : the lines to add to this configuration files are explained for each third party toolkit. Carefully read the configuration file section before reading that page.


CADP   [top]

Why installing CADP?

CADP is used by TTool for:
  • Computing a reachability graph from a generated LOTOS specification

  • Minimizing generated reachability graphs

  • Performing bisimulations between two graphs

How to configure CADP for TTool

First, download CADP. Then, configure the following IDCONFIG (see configuration file) as follows:
  • AldebaranHost: host on which you intend to run CADP, e.g., localhost

  • AldebaranPath: path to aldebaran, e.g., /packages/cadp/com/aldebaran

  • BcgioPath: path to bcgio, e.g., /packages/cadp/bin.iX86/bcg_io

  • BcgminPath: path to bcgmin, e.g., /packages/cadp/bin.iX86/bcg_min

  • BisimulatorPath: path to bcg_open, e.g., /packages/cadp/bin.iX86/bcg_open

  • BcgmergePath: path to bcg_open, e.g., /packages/cadp/com/bcg_merge

  • CaesarPath: path to caesar, e.g., /packages/cadp/bin.iX86/caesar

  • CaesarOpenPath: path to caesar.open, e.g., /packages/cadp/com/caesar.open



UPPAAL   [top]

UPPAAL is a model-checker that relies on timed-automata for system description, and on CTL formulae for system properties.

Why installing UPPAAL?

  • Searching from deadlock in a TURTLE, DIPLODOCUS or AVATAR model

  • Studying the reeachability or liveness of a given action of a TURTLE, DIPLODOCUS or AVATAR model

  • Performing simulation from TURTLE, DIPLODOCUS or AVATAR model

How to install UPPAAL

First, download UPP4ALL (formerly known as UPPAAL). Then, configure the following IDCONFIG (see configuration file) as follows:
  • UPPAALCodeDirectory: directory in which the UPPAL specification will be created by TTool from UML diagrams. The created specification is named spec.xml. This directory could be: /homes/mylogin/TTool/uppaal

  • UPPAALVerifierPath: path to the UPPAAL verifier, e.g.,:
    • in Windows: c:\uppaal\bin-win32\verifyta.exe
    • in Linux: /packages/uppaal/bin-Linux/verifyta
    • in MacOS: /Applications/uppaal/verifyta

  • UPPAALVerifierHost: host on which you intend to start the UPPAAL verifier, e.g., localhost

You may also wish to directly start the UPPAAL graphical interface from TTool. For that purpose, you can use one of the two configurable TTool external commands as follows (this example assumes the second configurable command is used):
  • in Windows: c:\uppaal\bin-win32\uppaal.exe c:\TTool\uppaal\spec.xml
  • in Linux: /packages/uppaal/uppaal /homes/mylogin/TTool/uppaal/spec.xml
  • in MacOS: open /Applications/uppaal/uppaal.app /Users/mylogin/TTool/uppaal/spec.xml


RTL   [top]

Why installing RTL?

Basically, RTL takes as input an RT-LOTOS specification and outputs a rechability graph. RTL is used by TTool for:
  • Computing a reachability graph from a generated RT-LOTOS specification (TURTLE, DIPLODOCUS)

How to install RTL

First, download RTL (A static version compiled for Linux is also available here), and install it. Then, configure the following IDCONFIG (see configuration file) as follows:
  • RTLHost: host on which you intend to run RTL, e.g., localhost

  • RTLPath: path to RTL, e.g., /packages/rtl/bin-linux/rtl

  • DTA2DOTPath: path to dta2dot, e.g., /packages/rtl/bin-linux/dta2dot

  • RG2TLSAPath: path to rg2tlsa, e.g., /packages/rtl/bin-linux/rg2tlsa

  • RGSTRAPPath: path to rgstrap, e.g., /packages/rtl/bin-linux/rgstrap



ProVerif  [top]

ProVerif is a toolkit dedicated to the proof of security properties. it takes as input a system described in pi-calculus, and a set of queries, and outputs true / false for each query. Technically speaking, it first translted queries and the pi-calculus specification into a set of Horn clauses, and tries to rsolve the clauses.

Why installing ProVerif?

  • Proving confidentiality and authenticity properties from an AVATAR model

How to install ProVerif

First, download ProVerif, and install it. Then, configure the following IDCONFIG (see configuration file) as follows:
  • ProVerifCodeDirectory: directory in which ProVerif specifications are generated by TTool, e.g., /homes/mylogin/TTool/ProVerif/

  • ProVerifVerifierPath: path to the ProVerif verifier, e.g., /packages/proverif/proverif

  • ProVerifVerifierHost: host on which ProVerif will be executed by TTool, e.g., localhost



Graphviz   [top]

Graphviz is a toolkit for visualizing graphs.

Why installing Graphviz?

  • Displaying reachability graphs generated, e.g., by CADP (TURTLE, DIPLODOCUS)

How to install Graphviz

First, download Graphviz, and install it. Then, configure the following IDCONFIG (see configuration file) as follows:
  • DOTTYPath: Path to the graphviz visualizer, e.g., /usr/bin/dotty

  • DOTTYHost: Host on which you wish to execute dotty, e.g., localhost



A C Compiler (e.g., gcc)   [top]

Why installing a C compiler

  • Compiling the prototyping code generated from AVATAR models

How to install a C compiler

Our prototyping code been tested on various platforms with gcc version 4. Once gcc is installed on your machine, configure the following IDCONFIG (see configuration file) as follows:
  • AVATARExecutableCodeDirectory: directory in which you expect TTool to generate the protptyping code, e.g., in /homes/mylogin/TTool/executablecode/

  • AVATARExecutableCodeHost: Host on which TTool will compile the generated C code, and will execute it, e.g., localhost

  • AVATARExecutableCodeCompileCommand: compilation command called by TTool to compile the generated C code, e.g., make -C /homes/mylogin/TTool/executablecode/

  • AVATARExecutableCodeExecuteCommand: Command used by TTool to start the execution of the prototyping code, e.g., /homes/mylogin/TTool/executablecode/run.x



SocLib / MutekH   [top]

Why installing SoCLib / MutekH

  • Prototyping the code generated from AVATAR model on a given microprocessor

How to install SoCLib / MutekH

  • Download and install SoCLib, as explained on the website of SoCLib

  • Download and install Mutekh, as explained on the website of MutekH

  • Generate a cross-compiler to be able to compile C code - i.e., the code generated from AVATAR model, and MutekH - for the selected SoCLib hardware platform

  • Adapt Makefile.forsoclib for your own configuration. This file is located in TTool/executablecode
You may also want to configure TTool for being able to use SocLib/MutekH with a press-button approach, that is, directly from TTool. Thus, once SoCLib and MutekH are correctly installed on your machine, configure the following IDCONFIG (see configuration file) as follows:
  • AVATARExecutableSoclibCodeCompileCommand: compilation command called by TTool to compile the code generated from AVATAR models (and MutekH), e.g., make -C /Users/ludovicapvrille/TTool/executablecode updategeneratedcode compilesoclib

  • AVATARExecutableSoclibCodeExecuteCommand: command to start SocLib, MutekH and the generate code, e.g. make -C /homes/mylogin/TTool/executablecode runsoclib

You also need to configure AVATARExecutableCodeDirectory and AVATARExecutableCodeHost, see the C compiler section

A C++ Compiler (e.g., gcc)   [top]

Why installing a c++ compiler

  • Compiling the simulation code generated from DIPLODOCUS models

How to install a C++ compiler

Our simulation code has been tested on various platforms with gcc version 4. Once gcc is installed on your machine, configure the following IDCONFIG (see configuration file) as follows:
  • SystemCCodeDirectory: directory in which you expect TTool to generate the simulation code, e.g., in /homes/mylogin/TTool/simulators/c++2/

  • SystemCHost: Host on which TTool will compile the generated C++ code, and will execute it, e.g., localhost

  • SystemCCodeCompileCommand: compilation command called by TTool to compile the generated C++ code, e.g., make -C /homes/mylogin/TTool/simulators/c++2/

  • SystemCCodeExecuteCommand: Command used by TTool to start the simulation in non-interactive mode, e.g., /homes/mylogin/TTool/simulators/c++2/run.x -ovcd /homes/mylogin/TTool/simulators/c++2/vcddump.vcd (in this example, a VCD trace file is generated)

  • SystemCCodeInteractiveExecuteCommand: Command used by TTool to start the interactive simulation, e.g., /homes/mylogin/TTool/simulators/c++2/run.x -server



GTKWave   [top]

Why installing GTKWave

  • Displaying simulation traces generated by DIPLODOCUS simulators

How to install a GTKWave

First, download GTKWave, and install it. Then, to start GTKWave from TTool, you may use one of the custom command as follows:
  • ExternalCommand1Host: host on which TTool will start GTKWave, e.g., localhost

  • ExternalCommand1: command to start GTKWave, e.g., /usr/local/bin/gtkwave /homes/mylogin/TTool/simulators/c++2/vcddump.vcd