Abstract

Abstract
Developing safe, concurrent (and parallel) software systems is a hard task in multiple aspects, particularly the sharing of information and the synchronization among multiple participants of the system. In the message passing paradigm, this is achieved by sending and receiving messages among different participants, raising a number of verification problems. For instance, exchanging messages in a wrong order may prevent the system from progressing, causing a deadlock.MPI is the most commonly used protocol for high-performance, message-based parallel programs, and the need for formal verification approaches is well acknowledged by much recent work (e.g., see [1]). © 2012 Springer-Verlag.

Abstract
This paper describes the layered control architecture and its software implementation developed and used at the Underwater Systems and Technology Laboratory. The architecture is implemented as a toolchain which consists on three main entities: DUNE onboard software, Neptus command and control software and a common IMC message-based communication protocol. The LSTS software toolchain has been tested throughout various field deployments where it was used to control heterogeneous autonomous vehicles like AUVs, ASVs, UAVs and ROVs in both single and multi-vehicle operations.

Abstract
A viability algorithm is developed to compute the constrained minimum time function for general dynamical systems. The algorithm is instantiated for a specific dynamics (Dubin's vehicle forced by a flow field) in order to numerically solve the minimum time problem. With the specific dynamics considered, the framework of hybrid systems enables us to solve the problem efficiently. The algorithm is implemented in C using epigraphical techniques to reduce the dimension of the problem. The feasibility of this optimal trajectory algorithm is tested in an experiment with a Light Autonomous Underwater Vehicle (LAUV) system. The hydrodynamics of the LAUV are analyzed in order to develop a low-dimension vehicle model. Deployment results from experiments performed in the Sacramento River in California are presented, which show good performance of the algorithm.

Abstract
The Hierarchical Timing Language (HTL) is a real-time coordination language for distributed control systems. HTL programs must be checked for well-formedness, race freedom, transmission safety (schedulability of inter-host communication), and time safety (schedulability of host computation). We present a modular abstract syntax and semantics for HTL, modular checks of well-formedness, race freedom, and transmission safety, and modular code distribution. Our contributions here complement previous results on HTL time safety and modular code generation. Modularity in HTL can be utilized in easy program composition as well as fast program analysis and code generation, but also in so-called runtime patching, where program components may be modified at runtime.

Abstract
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.