Abstract
The use of unmanned vehicle networks for diverse applications is becoming widespread. It is generally hard to program unmanned vehicle networks as a "whole", however. The coordination of multiple vehicles requires careful planning through intricate human intervention, and a high degree of informality is implied in what concerns the specification of a "network program" for an application scenario. In this context, we have been developing a programming language for expressing global specifications of coordinated behavior in unmanned vehicle networks, the Networked Vehicles' Language (NVL). In this paper we illustrate the use of the language for a thermal pollution plume tracking scenario employing unmanned underwater vehicles.

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
Uncoordinated Frequency Hopping (UFH) has been proposed as a mechanism to address denial-of-service attacks, and consists of legitimate devices hopping uniformly at random between frequencies to cope with an attacker that aims to disrupt communication. We consider the use of UFH against an eavesdropper adversary that aims to overhear as much information as possible. We characterize the secrecy level of wireless networks under UFH, showing the harmful security effect of broadband eavesdropper adversaries capable of overhearing in multiple frequencies. To counter such eavesdroppers, we consider the use of broadband friendly jammers that are available to cause interference on eavesdroppers. Our results show that adding a limited number of broadband friendly jammers effectively improves the security level of such systems.

Abstract
Uncoordinated Frequency Hopping (UFH) has been proposed as a mechanism to address denial-of-service attacks, and consists of legitimate devices hopping uniformly at random between frequencies to cope with an attacker that aims to disrupt communication. We consider the use of UFH against an eavesdropper adversary that aims to overhear as much information as possible. We characterize the secrecy level of wireless networks under UFH, showing the harmful security effect of broadband eavesdropper adversaries capable of overhearing in multiple frequencies. To counter such eavesdroppers, we consider the use of broadband friendly jammers that are available to cause interference on eavesdroppers. Our results show that adding a limited number of broadband friendly jammers effectively improves the security level of such systems. © 2015 IEEE.

Abstract
Most of current physical-layer security techniques rely on a degraded eavesdropper, thus warranting some sort of advantage that can be relied upon to achieve higher levels of security. We consider instead non-degraded eavesdroppers, that possess equal or better capabilities than legitimate receivers. Under this challenging setup, most of current physical-layer security techniques become hard to administer and new dimensions to establish advantageous periods of communication are needed. For that, we characterize the secrecy level of two schemes for physical-layer security under non-degraded eavesdroppers: a spread spectrum uncoordinated frequency hopping scheme, and a jamming receiver with self-interference cancellation.