Commit 4d7c1a99 authored by Tanwir Ahmad's avatar Tanwir Ahmad

initial commit

MBM ÅA can be used for academic use only. Any other use would require permissions from the authors. We consider only work performed by researchers or students at institutions delivering academic degrees, as academic use.
\ No newline at end of file
# Model-based Monitoring from Åbo Akademi (MBMÅA) tool
The MBMÅA tool uses UPPAAL timed automata for creating the behavioral model of the system under test. The UPPAAL model can be edited using a graphical user interface. The test adapter for MBMÅA tool can be specified using Jython. The model can be simulated and verified using UPPAAL with respect to the requirements of the system. MBMÅA can analyze execution traces specified in textual format.
## Installation
The tool can be executed on Windows and Linux machines.
1. Download and install Jython 2.5.4
1. Java SE Runtime Environment 6 or later
1. Download the binaries of the Spread from
Unpack the spread-bin-4.x.tar.gz file into the target directory and go to bin directory to run the Spread
1. Download TRON 1.5 from
1. Download Dtron 4.9.1
1. Set an environment variable TRON_HOME to the directory of UPPAAL TRON
export TRON_HOME=/home/test/uppaal-tron-1.5-linux
## Usage
- Select path for log file: edit Adapter/ or OldAdapter/
- Execute startup.bat
- Four MSDOS Command Prompt windows appear
- Select window called Adapter (“having text “press any key to start adapter….”) and press any key
### Configurations
$ java -jar dtron.jar -f <FILE> -o <UNITS> [-s <HOST>] -u <MSEC> -p <PORT>
-f,--file <FILE> UPPAAL model file to be used.
-o,--timeout <UNITS> TRON timeout in timeunits.
-s,--spread <HOST> Spread host addres, with port (default: localhost)
-u,--timeunit <MSEC> TRON timeunit in msec.
-p,--port <PORT> UPPAAL Reporter port (default: 666)
#### Test Tracker
$ java -jar TestTracker-0.2.jar -m <file> -coverageTypes <types> -t <templates> -outputFile <file> -details
-channel <channel> Channel to listen for messages on
-coverageTypes <coverageTypes> Requirement types, separated by ,. Available types are: edge, edge-pair, join-pointW, join-pointS, user-story
-details Set this flag to print a more detailed coverage report.
-fileOutput Enable reporting to file
-help Print this message and exit.
-m <modelFile> UPTA model file with counters on edges.
-outputFile <outputFile> File name for coverage output, use auto for automatic file name generation
-silent No output to console
-spread <spread> Host of the spread network. (default: localhost)
-t <templates> Provides templates names for test coverage. Separated by ','
-time <time> Time intervall of coverage output in ms. (default: 5000)
$ java -jar TestTracker-0.2.jar -m CLIC.xml -coverageTypes user-story -t IOAC -outputFile report.txt -details
- m CLIC.xml UPTA model file with counters on edges.
- coverageTypes user-story Coverage criteria is user-story
- t IOAC IOAC template for test coverage.
- outputFile <outputFile> File name for coverage output, use auto for automatic file name generation
- details Set this flag to print a more detailed coverage report.
#### Adapter
1. Set following parameters in ** file to configure the adapter:
speed_factor adjust the time scaling (default :1 )
log_path path of BTS log file
counter_timeout counter timeout
1. Dtron jar file should be set in the python path.
1. Run adapter with the following command:
$ jython -Dpython.path=dtron-4.9.1.jar -Dpython.cachedir=/tmp/jython
- Dpython.path: set the path for dtron library
- Dpython.cachedir: the directory to use for caches
- start the adapter
#### Spread
1. Run Spread with following command:
$ spread -n localhost
#### DTRON
1. Run dtron to simulate the model:
$ java -jar dtron-4.9.1.jar -f CLIC.xml -o 10000 -u 1000000 -p 6666
- jar dtron.4.12.jar: dtron java executable file
- f CLIC.xml: UPTA model file
- o 10000: simulation timeout in timeunit
- u 1000000: defined here that 1 timeunit should be equal to 1 second
- p 6666: UPPAAL Reporter port
*PS: There is no need to specify the Spread host address if the spread and dtron are running on same machine.*
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment