TTool
Main Installation Download Support TTool-AI DIPLODOCUS AVATAR SysML-Sec TTool-AMS Reference Public git Contact

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.

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 reachability 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

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


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/. This configuration is optional when using TTool projects. In that case, the default sub directory of the project in which the code is generated is "AVATAR_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

  • AVATARExecutableCodeExecuteCommand: Command used by TTool to start the execution of the prototyping code, e.g., 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 to version 8 (We do not offer support for other compilers, e.g. clang). 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


(c) L. Apvrille, Institut Mines-Telecom, Telecom Paris
Invisible border