Home

DICE-Verification Tool (D-VerT)

Welcome to the DICE-Verification wiki!

• Introduction
• Prerequisites
• Installation
  • Client
  • Server
• Getting Started

Introduction

The DICE Verification tool (D-VerT) allows the designers to specify the design of their data-intensive applications and to automatically run safety analysis on them exploiting formal verification techniques. The tool is part of the DICE IDE.

Prerequisites

• Eclipse Neon
• Docker

Installation

D-VerT has a Client-Server architecture: the client consists is distributed distributed as Eclipse plugin, while the server can be installed as a multi-container Docker application.

Client (Eclipse Plugin)

In the Eclipse Menu bar, select Help -> Install New Software... and use http://dice-project.github.io/DICE-Verification/updates

Server (multi-container Docker application)

Get the docker-compose.yml from here or clone the DICE-Verification repository. From the directory same directory of the file, run the docker-compose up command to fetch the docker images and run the server application.

Getting Started

Here we provide a quick overview of the usage of D-VerT. Users define the design of data-intensive applications from the Papyrus modeling perspective. 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 from by selecting the Run button.