NFM2019.md

Experiments Data for NFM 2019

MONAA

Extending MONAA, we implemented and evaluated our online algorithms for parametric timed pattern matching. We compiled our implementation using GCC 7.3.0. See also READMD.md. The source code we used in the experiment is available here.

IMITATOR

As a baseline, we used our previous implementation of parametric timed pattern matching based on IMITATOR [AHW18] (version 2.10.4).

Download

• Source code from GitHub
• Binary (Ubuntu-like, Debian-like 64 bits); this binary is standalone and can hence be executed without any external library

Experimental raw data

We conducted the experiments on an Amazon EC2 c4.large instance (2.9 GHz Intel Xeon E5-2666 v3, 2 vCPUs, and 3.75 GiB RAM) that runs Ubuntu 18.04 LTS (64 bit). We compiled PPL [BHZ08] with the following options.

--disable-dependency-tracking --enable-coefficients=checked-int64 --disable-silent-rules --enable-optimization=speed

• timed words
• raw experiment results generated by GNU time

Description of the Benchmarks

In addition to the following benchmarks, we also used the non-parametric variants Gear-np, Accel-np, Blowup-np, and OnlyTiming-np where the parameters are substituted to specific concrete values. In Gear-np, the parameter is substituted to 2. In Accel-np, the parameter is substituted to 3. In Blowup-np, the parameters are substituted to (10, 2, 1). In OnlyTiming-np, the parameter is substituted to 1.

Gear and Accel

Benchmark Gear inspired by the scenario of monitoring the gear change of an automatic transmission system. We conducted simulation of the model of an automatic transmission system [HAF14]. We used Breach to generate an input to this model; it generates a gear change signal that is fed to the model. A gear is chosen from {g_1,g_2,g_3,g_4}. The generated gear change is recorded in a timed word.

The of benchmark Accel is also constructed from the Simulink model of the automated transmission system [HAF14]. For this benchmark, the (discretized) value of three state variables are recorded in W: engine RPM (discretized to "high" and "low" with a certain threshold), velocity (discretized to "high" and "low" with a certain threshold), and 4 gear positions. We used Breach to generate a input sequence of gear change.

Blowup

As a third experiment, we considered a (toy) benchmark that acts as a worst case situation for parametric timed pattern matching, coming from [AHW18].

OnlyTiming

As a fourth experiment, we considered another (toy) benchmark. In OnlyTiming, the parametric skip values are greater than the non-parametric skip values.

Calling MONAA-based implementations

For all case studies, the following command was used for PTPM:

./build/[program] -f [pta.dot] < [timed_word.txt]

Calling IMITATOR

For all case studies, the following command was used for PTPM:

./imitator [case_study.imi] -mode EFunsafe -no-inclusion-test-in-EF -incl -verbose experiments -output-result

References

[AHW18]

Étienne André, Ichiro Hasuo and Masaki Waga (和賀 正樹). Offline timed pattern matching under uncertainty. In Anthony Widjaja Lin and Jun Sun (eds.), ICECCS’18, IEEE CPS, pages 10–20, December 2018.

[BHZ08]

Roberto Bagnara, Patricia M. Hill and Enea Zaffanella. The Parma Polyhedra Pibrary: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems. Science of Computer Programming, 72(1–2):3–21, 2008.

[HAF14]

Bardh Hoxha, Houssam Abbas, Georgios E. Fainekos: Benchmarks for Temporal Logic Requirements for Automotive Systems. ARCH@CPSWeek 2014: 25-30.