TiPEX: A Tool Chain for Timed Property Enforcement During eXecution

Abstract

The TiPEX tool implements the enforcement monitoring algorithms for timed properties proposed in [1]. Enforcement monitors are generated from timed automata specifying timed properties. Such monitors correct input sequences by adding extra delays between events. Moreover, TiPEX also provides modules to generate timed automata from patterns, compose them, and check the class of properties they belong to in order to optimize the monitors. This paper also presents the performance evaluation of TiPEX within some experimental setup.

A Demonstration of TiPEX

We illustrate the features of TiPEX discussed in the paper via some examples. All the source files with examples, prerequisites, and some documentation are available at:

http://srinivaspinisetty.github.io/Timed-Enforcement-Tools/

1.1 A.1 Modules EMTA and EME

In the following subsections, we describe how to test the input-output behavior of an enforcement monitor, and how to collect performance data for a property.

Testing the Behavior of an Enforcement Monitor. We present how the input-output behavior of enforcement monitors for some properties is tested. We consider three example properties (used in Sect. 3). We also provide the TAs defining these properties in UPPAAL format (.xml files) inside the source folder.

• Example_Safety.xml defines a safety property expressing that “There should be a delay of at least 5 t.u. between any two request actions”.

• Example_CoSafety.xml defines a co-safety property expressing that “A request should be immediately followed by a grant, and there should be a delay of at least 7 t.u. between them”.

• Example_Response.xml defines a regular property, and expresses that “Resource grant and release should alternate. After a grant, a request should occur between 15 to 20 t.u.”. Note that this property is neither a safety nor a co-safety property.

To test the functionality, with these properties for some input traces, simply run the test script testFunctionality.py (available inside the source folder). For each property, the input trace provided and the output of the EM is printed on the console. On the console, we can observe that for each property, for the provided input, the output satisfies the property (soundness) and the other constraints (transparency, optimality).

Collecting Performance Data. We explain via an example how the main test method is invoked via Python command line to collect performance data for a property (see Fig. 5).The steps are the following:

Fig. 5.

Collecting performance data.

• Import the MainTest module.

• Specify the property by indicating its path.“Example_Safety.xml” is the property in this example, which is a UPPAAL model stored as “.xml”.

• Specify the accepting locations in the input TA. For instance, by typing “accLoc=[‘S1, ‘S2’]”, one specifies that the set of accepting locations in the input TA is {S1, S2}.

• Specify the possible actions. For instance by typing “actions = [‘a,’r’]” one specifies that the set of actions is {a, r}.

• Define the range of possible delays.

• Invoke method testStoreProcess in module MainTest, providing the following arguments in order: property, accepting locations, actions, delays, # traces incr.

“#traces” is the number of traces used for testing (3 in the example above), each trace varying in length, and “incr” is the increment in length per trace (1,000 in the example above). As shown in Fig. 5, a list of triples (trace length, total execution time of the Update function, average time per call of the Update function) is returned as the result.

1.2 A.2 Module TAG

Module TAG has a basic GUI. The following lines demonstrate how to launch the GUI via Python command line.

Fig. 6.

GUI.

• Browse to the folder containing the source code.

• Execute the script GUI_TAG_Tool.py entering the following line in the command prompt python GUI_TAG_Tool.py.

• A GUI will be launched (shown in Fig. 6a), using which the user can select to generate a basic TA, or to combine TAs, or to check the class of a TA.

We demonstrate how to use each feature via an example.

Generating Basic Timed Automata. We present some TAs generated using module TA Generator. Clicking “Generate Basic TA” launches the GUI shown in Fig. 6b. To generate a TA defining the requirement “In any time interval of 10 t.u., there cannot be 3 or more a actions”, the values of the input parameters provided the tool are:

Fig. 7.

Automaton belonging to the precedence pattern.

• PATTERN = absence,

• COMPLEXITY_CONSTANT = 3,

• TIME_CONSTRAINT_CONSTANT = 10,

• ACTION1 = a, and ACTION2 = b.

Figure 8 shows the representation in UPPAAL. In this TA, $\mathrm L0$ is initial location, {L0, L1, L2, L3} is the set of accepting locations, and the only non-accepting location is Final_NA. In $\mathrm L0$, upon action $\mathrm a$, if the value of clock $x\ge 10$, then the clock x is reset and the TA remains in the same location. We can see that the TA moves to a non-accepting (trap location) $\mathrm {Final\_NA}$ upon 3 a actions within 10 time units. To generate a TA defining the requirement “A sequence of 3 a actions enables action b after a delay of at least 5 t.u.”, the values of the input parameters provided to the tool are:

Fig. 8.

Automaton belonging to the absence pattern.

• PATTERN = precedence,

• COMPLEXITY_CONSTANT = 3,

• TIME_CONSTRAINT_CONSTANT = 5,

• ACTION1 = a, and ACTION2 = b.

Figure 7 shows its representation in UPPAAL tool. In this TA, $\mathrm L0$ is the initial location, $\left\{ \mathrm L0, L1, L2, L3 \right\}$ is the set of accepting locations, and the only non-accepting location is NAcc. We can see that from locations $\mathrm L0$, $\mathrm L1$, and $\mathrm L2$, if a $\mathrm b$ action occurs then the TA moves to the trap state, since 3 preceding $\mathrm a$ actions are missing.

Composing Timed Automata. Clicking “Combine TAs” launches the GUI shown in Fig. 9. Clicking “Select File” button allows the user to select an input UPPAAL model. The input UPPAAL model (stored as .xml) selected by the user, should contain two input TAs (defined as two different templates). Note that in the input TAs, names of accepting locations should be prefixed by “Final”. The user should select an operation. The resulting TA will be written as another template in the UPPAAL model file given as input by the user.

Fig. 9.

Combine TA GUI.

Fig. 10.

Example: Combining TAs using Boolean operations.

Let us now see an example of the resulting TA obtained after combining two TAs using the Boolean Operations functionality. The two input TAs are shown in Figs. 10a and b. Figure 10c shows the resulting TA after combining the two input TAs using Union operation.