Aerial: An Almost Event-Rate Independent Monitor
for Metric Temporal Logic and Metric Dynamic Logic
Department of Computer Science, ETH Zurich, Switzerland
This library is distributed under the terms of the GNU Lesser General
Public License version 3. See files LICENSE and COPYING.
The algorithms behind this tool were developed jointly with David Basin and
Bhargav Bhatt. The theory is described in the paper draft:
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
Aerial depends on a recent (>= 4.04.0) version of the OCaml compiler.
(An outdated PolyML implementation of Aerial referenced in the above
paper can be found in this repository under the tag 'poly'.)
To install ocaml and some additional libraries use opam - ocaml's
package manager. For example:
apt-get install opam
opam switch 4.04.1
eval $(opam config env)
then compile Aerial with
to obtain a binary aerial.native file and
./aerial.native -fmla examples/test1.mtl -log examples/test2.log
to run an example.
provides some additional hints about the tool's user interface.
This repository also contains the bash scripts used to generate log files and
run the experiments reported on in the above paper (directory experiments).
The shell scripts assume the "aerial", "monpoly" and "montre" binary
files to be available in the PATH, a working installation of GNU Parallel and
coreutils package for macOS. Scripts are tested on macOS 10.12.4 and Ubuntu 16.04.
A pre-configured environment for running the experiments can be found on the official
tool website: http://www.infsec.ethz.ch/research/software/aerial.html