Abstract
The coordinated use of multiple unmanned vehicles over a network can be employed for numerous real-world applications. However, multi-vehicle operations are often deployed through a patchwork of separate components that informally "glue" together during operation, as they are hard to program as a "whole". With this aim, we developed the Networked Vehicles' Language (NVL) for coordinated control of unmanned vehicle networks. A single NVL program expresses an on-the-fly selection of multiple vehicles and their allocation to cooperative tasks, subject to time, precedence, and concurrency constraints. We present the language through an example application involving unmanned underwater vehicles (UUVs) and unmanned aerial vehicles (UAVs), the core design and implementation traits, and results from simulation and field test experiments.

Abstract
We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We develop a protocol language based on a dependent type system for message-passing parallel programs, which includes various communication operators, such as point-to-point messages, broadcast, reduce, array scatter and gather. For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for C. We successfully verified several MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with alternative techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-of-the-art tools for MPI to conclude that our approach offers a scalable solution.

Abstract

Abstract

Abstract
We describe a case study application for untethered video dissemination using a hybrid edge-cloud architecture featuring Android devices, possibly organised in WiFi-Direct groups, and Raspberry Pi-based cloudlets, structured in a mesh and also working as access points. The application was tested in the real-world scenario of a Portuguese volleyball league game. During the game, users of the application recorded videos and injected them in the edge-cloud. The cloudlet servers continuously synchronised their cached video contents over the mesh network, allowing users on different locations to share their videos, without resorting to any other network infrastructure. An analysis of the logs gathered during the experiment shows that such portable setups can easily disseminate videos to tens of users through the edge-cloud with low latencies. We observe that the edge-cloud may be naturally resilient to faulty cloudlets or devices, taking advantage of video caching within devices and WiFi-Direct groups, and of device churn to opportunistically disseminate videos.

Abstract
FLUX is a platform for dynamically reconfigurable crowd-sensing using mobile devices like smartphones and tablets, programmed under a notion of region-based sensing. Each region is defined by a set of physical constraints that determine the sensing scope, e.g., based on device position or other environmental variables, plus a set of periodic tasks that perform the actual sensing. The resulting behavior is inherently dynamic: as a device's state changes, e.g., moves in space, it enters and/or leaves different regions, thereby changing the set of active tasks; moreover, regions can be added, deleted, and reprogrammed on-the-fly. FLUX makes use of a domain-specific language for sensing tasks that is compiled into abstract bytecode, later executed by a low-footprint virtual machine within a device, guaranteeing runtime safety by construction. For region/task dissemination, FLUX employs a broker that holds a changeable region configuration plus gateways that mirror the configuration throughout different network access points to which devices connect. Sensing data is streamed by devices to gateways and then back to the broker. Live or archived data streams are in turn fed by the broker to data-processing clients, which interface with the broker using a publish/subscribe API. We conducted two case-study experiments illustrating FLUX: a single-region deployment to monitor WiFi signal quality, and a multi-region deployment to monitor noise, temperature, and places-of-interest based on device movement.