Getting Started

Here we provide a quick overview of the usage of D-VerT for the currently supported data-intensive technologies: Apache Storm (data streaming applications) and Apache Spark (batch applications). In both the cases users start by defining the design of data-intensive applications from the Papyrus modeling perspective.

Verification of Storm topologies

The figure below shows an example of design of a simple Storm topology in the Papyrus perspective. Storm topologies can be defined as DICE-Profiled UML class diagrams, in which each component of the application needs to be conveniently annotated. The class diagram is defined by simply dragging and dropping elements from the palette on the right side of the IDE.

Each component is then configured in the Properties view at the bottom. The relevant settings to configure Storm topologies are: the Name of the component (located under the UML tab), the applied stereotype (Profile tab) and some of the specific parameters provided by the selected profile. As described in the tool documentation, the relevant parameters for each spout are parallelism and avgEmitRate. Each bolt needs the configuration of parallelism, alpha (processing time) and sigma (kind of function performed). Subscription of bolts to other components in the topology is specified by adding an association form the subscriber bolt to the subscribed component. Figure below shows the configuration of bolt B1, whose sigma parameter is given the value of 2.

Once the design of the application is complete, it is possible to configure the tool and run the verification steps below:

• from the Run button dropdown, select Run configurations...

• Create new launch configuration of type DICE Verification as shown in the figure below

• The launch configuration allows the user to define a set of parameters that will be given to the tool in order to run the verification task. As depicted in the figure below, the first parameter is the DICE-profiled UML model, that can be selected by browsing the workspace. It is possible to store some intermediate files in the workspace, such as the JSON file containing a compact representation of the data-intensive application. This can be done by simply selecting the checkbox and the location where to save the files. Next, the user can select the time bound against which run the verification, the Zot plugin to be used and the bolts that will be monitored to detect possible unwanted behaviors.

• Once all the parameters are valued, it is possible to run the verification task by selecting the Run button.

• The verification task is now running on the D-VerT server. A browser tab immediately opens in the DICE IDE, showing the DICE Server dashboard. The dashboard lists all the verification tasks running or already completed on the Server. D-VerT Server Dashboard is reachable by default at port 5000 of the server. In case of local instantiation of the server, simply open http://localhost:5000 on a browser to get to the D-VerT Server Dashboard.

Verification of Spark DAGs

The figure below shows an example of design of a Spark application in the Papyrus perspective. Spark applications can be defined as DICE-Profiled UML activity diagrams, in which each component (opaque action node) represents a Spark operation and needs to be conveniently annotated. The activity diagram is defined by simply dragging and dropping elements from the palette on the right side of the IDE.

Each node is then configured in the Properties view at the bottom. The relevant settings to configure Spark applications are: the Name of the component (located under the UML tab), the applied stereotype (Profile tab) and some of the specific parameters provided by the selected profile. As described in the tool documentation, the relevant parameters for each operation are: duration, operationType and, when applicable, numTasks. Operations (opaque activity nodes) are connected by means of Control Flow edges. Figure below shows the configuration of of a filter operation (which is a transformation), whose MapType parameter is configured as Filter.

Once the design of the application is complete, it is possible to configure the tool and run the verification steps below:

• from the Run button dropdown, select Run configurations...

• Create new launch configuration of type DICE Verification - Spark as shown in the figure below

• The launch configuration allows the user to define a set of parameters that will be given to the tool in order to run the verification task. As depicted in the figure below, the first parameter is the DICE-profiled UML model, that can be selected by browsing the workspace. It is possible to store some intermediate files in the workspace, such as the JSON file containing a compact representation of the data-intensive application. This can be done by simply selecting the checkbox and the location where to save the files. Next, the user can select the kind of analysis she/he wants to perform, the deadline against which check the DAG execution, the time bound to be considered for bounded verification.

• Once all the parameters are valued, it is possible to run the verification task by selecting the Run button.

• The verification task is now running on the D-VerT server. A browser tab immediately opens in the DICE IDE, showing the DICE Server dashboard. The dashboard lists all the verification tasks running or already completed on the Server. D-VerT Server Dashboard is reachable by default at port 5000 of the server. In case of local instantiation of the server, simply open http://localhost:5000 on a browser to get to the D-VerT Server Dashboard.