This paper describes the open-source software toolchain developed by the Underwater Systems and Technology Laboratory (LSTS) for supporting networked heterogeneous air and ocean vehicle systems. The toolchain supports the deployment of air and ocean vehicles interacting over limited acoustic and wireless networks combined with disruption-tolerant networking protocols. We present the different components of the toolchain and how they can be deployed and extended for different scenarios. We conclude with descriptions of recent applications to onboard deliberative planning and integration of low-cost micro UAVs into the toolchain.

This paper presents the Inter-Module Communication (IMC) protocol, a message-oriented protocol designed and implemented in the Underwater Systems and Technology Laboratory (LSTS) to build interconnected systems of vehicles, sensors and human operators that are able to pursue common goals cooperatively by exchanging real-time information about the environment and updated objectives. IMC abstracts hardware and communication heterogeniety by providing a shared set of messages that can be serialized and transferred over different means. The described protocol contrasts with other existing application level protocols by not imposing or assuming a specific software architecture for client applications. Native support can be automatically generated for different programming languages and/or computer architectures resulting in optimized code which can be used both for networked nodes and also for inter-process and inter-thread communication. The protocol has already been tested throughout various experiments led by LSTS where it has taken care of communications between vehicles, sensors and operator consoles. We are now developing the protocol in the direction of having multi-vehicle cooperation using live data from environmental sensors and mixed-initiative user interaction.

The design and development of the swordfish autonomous surface vehicle (ASV) system is discussed. Swordfish is an ocean capable 4.5 m long catamaran designed for network centric operations (with ocean and air going vehicles and human operators). In the basic configuration, Swordfish is both a survey vehicle and a communications node with gateways for broadband, Wi-Fi and GSM transports and underwater acoustic modems. In another configuration, Swordfish mounts a docking station for the autonomous underwater vehicle Isurus from Porto University. Swordfish has an advanced control architecture for multi-vehicle operations with mixed initiative interactions (human operators are allowed to interact with the control loops).

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.

Underwater acoustic networks can be quite effective to establish communication links between autonomous underwater vehicles (AUVs) and other vehicles or control units, enabling complex vehicle applications and control scenarios. A communications and control framework to support the use of underwater acoustic networks and sample application scenarios are described for single and multi-AUV operation.