Tools Demos


Authors: Zhihao Shang, Han Wu and Katinka Wolter
Contact author / presenter: zhihao shang
Demo title: An OpenFlow Controller Performance Evaluation Tool
Demo abstract: SDN (Software Defined Networking) provides a way to flexible networks and makes the management easy. This is achieved by the centralized and programmable controllers. OpenFlow is a popular SDN protocol. In an OpenFlow network, the controller is the only part implemented logically, all the switches can only execute the instructions from the controller. The OpenFlow protocol introduces a new forwarding delay into the networks because of the communications between the switches and the controller. It may become a bottleneck in a large network. Therefore, it is important to understand how a controller impacts an OpenFlow network for researchers and network managers. Many researchers have noticed this problem and built queueing models for OpenFlow networks to measure the impact of the communications. Many studies assume the message processing time of controllers following an exponential distribution. Based on our measurements, the exponential distribution cannot fit the message processing very well. At the same time, there are no tools that offer the response time for individual messages. We present a user-friendly OpenFlow controller performance evaluation tool that aims to help network researchers building performance models of OpenFlow controllers and network manager to understand the behavior of OpenFlow controllers. The tool uses a virtual OpenFlow switch sending OpenFlow messages to a controller and measures the response time. It fits the response time to a hyper-Erlang distribution. Researchers can use this tool to analyze the response time of an OpenFlow controller and obtain the distribution of the response time. They can use the distribution in their model.
Paper title in ValueTools: Performance Evaluation of the Control Plane in Software Defined Networks



Authors: Shireen Seakhoa-King and William Knottenbelt
Contact author / presenter: Shireen Seakhoa-King
Demo title: Revenue-Driven Scheduling in a Drone Delivery Network Simulation using SpatialOS
Demo abstract: Drones are set to revolutionise the courier services industry as the vehicle of choice for “last-mile” logistics, anticipated to contribute £42 billion to the UK economy by the year 2030. In such an environment of increasing demand, drone-based courier service providers will need to make intelligent decisions on how to deploy their limited and highly-utilised resources to enhance profits. A new scheduling algorithm, Least Lost Value (LLV), was developed for optimising the revenue of a drone courier service provider. SpatialOS, a cloud-based distributed platform, was used to implement a drone delivery network simulation to test the effectiveness of LLV in a time-sensitive service delivery system. The SpatialOS platform was selected primarily for scalability of its Entity-Component-Worker model and visualisation capability using its Inspector tool. Results show LLV successfully routing drones to extract increased revenue to the service provider in comparison to traditional scheduling algorithms.
Paper title in ValueTools: Revenue-Driven Scheduling in Drone Delivery Networks with Time-Sensitive Service Level Agreements



Authors: Paolo Ballarini, Benoit Barbot and Nicolas Vasselin
Contact author / presenter: Paolo Ballarini
Demo title: COSMOS
Demo abstract:

Cosmos is a statistical model checker for Hybrid Automata Specification Language (HASL). HASL uses Linear Hybrid Automata (LHA), a generalization of Deterministic Timed Automata (DTA), to describe accepting execution paths of a Discrete Event Stochastic Process (DESP), a class of stochastic models which includes, but is not limited to, Markov chains. As a result, HASL verification turns out to be a unifying framework where sophisticated temporal reasoning is naturally blended with elaborate reward-based analysis. Cosmos takes as input a DESP (described in terms of a Generalized Stochastic Petri Net), a LHA and an expression Z representing the quantity to be estimated. It returns a confidence interval estimation of Z. Cosmos is written in C++ and is freely available to the research community.

Relationship of the tool to the conference topics (100-200 words): COSMOS is very much in the scope of the ValueTools conference as it provides the user with a framework for performance modelling of stochastic systems. Cosmos features Stochastic Petri Nets (both uncoloured and coloured) as modelling formalism which has been proved a powerful language with applications in different domains, including, networks performance analysis, manufacturing systems, biology. The HASL property specification language has also proven extremely powerful formalism particularly suited to performance analysis.

Paper title in ValueTools: Performance modelling of access control mechanisms for local and vehicular wireless network



Authors: Susanna Donatelli and Elvio Amparore
Contact author / presenter: Susanna Donatelli
Demo title: GreatSPN for stochastic and qualitative model-checking of systems
Demo abstract: GreatSPN is a tool for the definition and analysis of Petri nets of various sorts (classical P/T nets, colored nets, stochastic P/T nets and stochastic colored nets). It features a Java-based graphical interface and a large number of analysis tools, fully integrated in the interface.

This tool demo is aimed at emphasizing two complementary aspects of the tool: teaching and research.

For teaching we shall demo the restructuring of the graphical interface to support incremental learning objectives.

For research we shall demo the model-checker of CTL formulas and the stochastic model-checker MC4CSLTA, which verifies CSLTA formula. MC4CSLTA supports the definition of the formula (graphically specified as a timed automaton), an interactive execution of the Petri net paths accepted and rejected by the automaton, and a number of advanced methods to compute the probability of the accepting paths (among this the “on-the-fly approach” presented in the invited talk of Donatelli).

GreatSPN can be downloaded as a virtual machine, or in source code at its gitHub repository.

Github repository:

GreatSPN home page:

Paper title in ValueTools: Keynote speaker