TiPEX: A Tool Chain for Timed Property Enforcement During eXecution

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://​srinivaspinisett​y.​github.​io/​Timed-Enforcement-Tools/​ 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:

“#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. 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. Module TAG has a basic GUI. The following lines demonstrate how to launch the GUI via Python command line.

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:

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:

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.

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.

1 2 3