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
Real-time monitoring applications may generate delay sensitive traffic that is expected to be delivered within a firm delay boundary in order to be useful. In this context, a previous work proposed an End-to-End Delay (EED) estimation mechanism for Wireless Sensor Networks (WSNs) to preview potential useless packets, and to early discard them in order to save processing and energy resources. Such estimation mechanism accounts delays using timers that make use of an Exponentially Weighted Moving Average (EWMA) function where the smoothing factor is a constant defined prior to the WSN deployment. Later experiments showed that, in order to enhance the estimation results, such smoothing factor should be defined as a function of the network load. The current work proposes an optimization of the previous estimation mechanism that works by evaluating the network load and by adapting the smoothing factor of the EWMA function accordingly. Results show that this optimization leads to a more accurate EED estimation for different network loads.

Abstract
Wireless Sensor Networks (WSNs) can be deployed using available hardware and software. The Contiki is an operative system compatible with a wide range of WSN hardware. A Contiki development environment named InstantContiki is also available and includes the Cooja simulator, useful to test WSN simulation scenarios prior to their deployment. Cooja can provide realistic results since it uses the full Contiki's source code and some motes can be emulated at the hardware level. However this implies extending the simulation runtime, which is heightened since the Cooja is single threaded, i.e, it makes use of a single core per instant of time, not taking advantage of the current multi-core processors. This chapter presents a framework to automate the configuration and execution of Cooja simulations. When a multi-core processor is available, this framework runs multiple simultaneous Cooja instances to reduce simulations runtime in exchange of higher CPU load and RAM usage.

Abstract
WSN can be deployed using widely available hardware and software solutions. The Contiki is an open source operative system compatible with a wide range of WSN hardware. A Contiki development environment named InstantContiki is also available and includes the Cooja simulation tool, useful for the simulation of WSN scenarios, prior to their deployment. This simulation tool can provide realistic results since it uses the full Contiki's source code and some motes can be emulated at the hardware level. However, the Cooja simulator uses one process per simulation, not taking advantage of multiple core processors. In this paper we propose a framework to automate the execution of simulations of multiple scenarios and configurations in Cooja. When a multiple cores processor is available, this framework can run multiple simultaneous Cooja instances, taking advantage of processing resources and contributing to reduce the total simulation runtime.