We have created a video demonstration of TPV that can be viewed below or through YouTube TPV Demonstration.

This repository contains a modified distribution of USE that includes our TPV plug-in. To install the tool, download the repository files as a zip folder and extract them in the desired install directory.

Note: You must install the Java Runtime Environment in order to run USE.

We have used MDE technologies to define, implement, and package the code of the TPV tool as a plugin for the UML-based Specification Environment (USE). We provide a video overview of how to create UML design class diagrams and load them into USE for analysis. This tutorial can be watched below and can also be acessed on YouTube.

Running USE on Windows

Open the bin folder and run the ‘use’ executable.

Running USE on Mac

1. Open a terminal window.
2. Traverse to the lib directory of the downloaded USE files
3. Execute the following command: java -jar use.jar

Launching TPV

After running USE, a user needs to open the TPV plugin by clicking the icon shown below.

Figure 1. USE Main Window

This opens the TPV Main Window shown below:

Figure 2. TPV Main Window

Refer to the Overview of USE section above for a demo of how to create UML class diagrams in USE specification. Alternatively, you can create a class diagram using any other UML tool and extract it as an XMI file that can then be opened using TPV. We provide a couple of examples in this repository to make it easier for a user to get started with the tool.

The first input of TPV is the class diagram to be analyzed. TPV can take UML class into the following two formats:

1. The USE specification format saved in .use files.
2. The standard UML format saved in .uml files.

To choose a class diagram, click Select (Figure 2-1), which opens the following window. Then, select the file containing the class diagram that will be analyzed and press Open.

Figure 3. Choose Input Model File Window

The second input necessary for TPV is a TOCL temporal property to be checked. A user can input a property in three different ways.

1. Using a prespecified TOCL property saved in a .tocl file.
2. Specifying a TOCL property manually from scratch.
3. Using the specification patterns to specify a propety.

We show how to specify a property using the above three ways. The first is inputting a .tocl file containing a TOCL property (Figure 2-2). Click Select, which opens a window that asks for a .tocl file.

Figure 4. Choose Input TOCL File Window

Select a file containing a temporal property to analyze against and press Open.

It is also possible to input a TOCL temporal property by specifying it within the plug-in interface (Figure 2-3). Clicking Specify opens the following window:

Figure 5. Specify TOCL Property Window

The first specification method involves typing a TOCL property into the text box labeled Enter TOCL temporal properties (Figure 5-a).

Alternatively, clicking the Use Patterns button (Figure 5-d) will bring up the temporal pattern specification window below.

Figure 6. Choose pattern window

This window offers a choice to use different temporal specification patterns as templates for defining TOCL properties. After choosing one, you will then be directed to choose a scope for the property in the window below.

Figure 7. Choose scope window

Choosing a scope results in the final window below, which includes a description of the pattern considering the scope, an example with explanation, and instructions on how to use the pattern.

Figure 8. Response in global scope pattern window

Specified properties can then be saved using the Save to File option. (Figure 5-e).

To use a specified TOCL property for analysis, click Apply (Figure 5-c). Any syntax errors generated by specified properties will be displayed in the dialog labeled Feedback (Figue 5-b).

The state explosion problem is a known difficulty in model checking when analyzing complex models. As such, TPV includes an optimization technique to improve analysis efficiency. The optimization algorithm finds elements in a model that are related to a given property and returns an optimized model that only includes elements relevant for the analysis of the property. This technique reduces the search space for analysis and was found to improve analysis times by up to 90% during prior testing. A user needs to click the checkbox (Figure 2-4) to use it.

The next step is configuring the analysis (Figure 2-5). There are two ways to configure the analysis. The first method is entering a new analysis configuration. The second method is using a previously defined configuration stored in a .properties file.

Creating an analysis configuration is done by specifying a search-scope and search-depth for the analysis. Search-scope defines the maximum number of objects of each class that can be instantiated during analysis. Search-depth defines the maximum number of transitions considered for analysis. For instance, if you wanted to analyze a Restaurant model where the maximum number of customers (along with every other class) is 10 and you want to perform at most 8 operations on the system, then you might specify a search-scope of 10 and a search-depth of 8. However, the tool may produce a smaller counterexample if it is enough to illustrate an error. Once scope and depth have been specified, it is possible to enter an advanced configuration mode. In this advanced mode, an individual analysis configuration can be created for each class and association present in the model.

To use a previously created configuration, click on the Configuration method dropdown (Figure 2-5) and select Upload .properties file. The option Enter a .properties File should become visible. Click Select and choose the .properties file containing the desired analysis configuration.

Finally to perform the analysis and search for a counterexample, press Validate. You can also press Cancel to close the window.

Figure 9. Example counterexample

Optionally, you can extract a sequence diagram from a produced counterexample. After pressing Validate in the last step, the window below pops up in the bottom right corner.

Figure 10. Snapshot Transition to Sequence Diagram Window

Pressing OK converts the counterexample to a sequence diagram like the one below:

Figure 11. Example sequence diagram

Along with the tool, we have provided a few examples in the examples folder including a Traffic Light model and a Steam Boiler Control System Model, both with temporal properties.

Figure 12. TrafficLight example folder

This folder includes a .uml file of the model, which can be used as the class diagram input in Step 3. It also includes a folder of temporal properties; any of these can be used as the temporal property input in Step 4.

Evaluation Methodology

To evaluate TPV, we used a survey based on the innovative user needs experience (NX) evaluation method proposed by Zarour, 2020. The method is based on three pillars:

1. Evaluation theory from the social sciences.
2. The ISO/IEC SQuaRE 25000 series standards.
3. The NX dimension of the UX framework.

The survey contains a total of 44 questions grouped into four sections focusing on:

1. Usefulness: How useful do you find TPV?
2. Pleasure: How much do you enjoy using TPV?
3. Aesthetics: How appealing do you find the user interface of TPV?
4. Trust: How much do you trust TPV to be reliable and secure?

After each group of questions, the survey includes a section where users can provide qualitative feedback on each section or suggestions for improvement. To get insights into the user experience of TPV, we collected responses from a sample of student participants in the software design and software engineering courses at Texas A&M International University. We wanted to make the study as realistic as possible for actual TPV users, so we did not provide the students with formal training on MDE, model checking, or temporal property specification. Instead, we instructed the students to download TPV from this GitHub repository, watch a few tools overview videos, and follow the instructions to download and run the tool. Additionally, we provided the students with an evaluation guide that gave them some basic training on software specification and validation and two specification and validation case studies that they should complete before responding to the survey questions. We gave the students two weeks to complete the survey independently, without supervision. A total of 19 student participants responded to the study.

Evaluation Guide

We have created the following linked simple document to guide through the evaluation process--TPV Evaluation Guide. After completing the tasks in the guide, the students completed the survey and gave ratings of each question.

Survey Questions

The actual questions of the survey can be accessed through the following link (Questions.)

Evaluation Results

The table below summarizes the student survey results on the four criteria. The results show that TPV is generally perceived as useful, but there is room for improvement in the four user experience categories. The user interface is also generally well-liked, but there are some areas that could be improved. Overall, the students felt they could depend on TPV to work correctly and do its tasks.

Evaluation Participation

We would love to hear your feedback about TPV. If you would like to provide your feedback, you can fill out the following survey at TPV Survey. Your thoughtful feedback is greatly appreciated.