Over the past decade, wireless sensor networks have advanced in terms of hardware design, communication protocols, resource efficiency, and other aspects. Recently, there has been much focus on mobile wireless sensor networks, and several small-profile sensing devices that are able to control their own movement have already been developed. Unfortunately, resource constraints inhibit the use of traditional navigation methods, because these typically require bulky, expensive, and sophisticated sensors, substantial memory and processor allocation, and a generous power supply. Therefore, alternative navigation techniques are required. In this paper we present TripNav, a localization and navigation system that is implemented entirely on resource-constrained wireless sensor nodes. Localization is realized using radio interferometric angle of arrival estimation, in which bearings to a mobile node from a small number of infrastructure nodes are estimated based on the observed phase differences of an RF interference signal. The position of the mobile node is then determined using triangulation. A digital compass is also employed to keep the mobile node from deviating from the desired trajectory. We demonstrate using a real-world implementation that a resource-constrained mobile sensor node can accurately perform waypoint navigation with an average position error of 0.95 m.

In the past decade, numerous consensus protocols for networked multi-agent systems have been proposed. Although some forms of robustness of these algorithms have been studied, reaching consensus securely in networked multi-agent systems, in spite of intrusions caused by malicious agents, or adversaries, has been largely underexplored. In this work, we consider a general model for adversaries in Euclidean space and introduce a consensus problem for networked multi-agent systems similar to the Byzantine consensus problem in distributed computing. We present the Adversarially Robust Consensus Protocol (ARC-P), which combines ideas from consensus algorithms that are resilient to Byzantine faults and from linear consensus protocols used for control and coordination of dynamic agents. We show that ARC-P solves the consensus problem in complete networks whenever there are more cooperative agents than adversaries. Finally, we illustrate the resilience of ARC-P to adversaries through simulations and compare ARC-P with a linear consensus protocol for networked multi-agent systems.

$m$-Triangular Systems are dynamical physical systems which can be described by $m$ triangular subsystem models. Many physical system models such as those which describe fixed-wing and quadrotor aircraft can be realized as $m$-Triangular Systems. However, many control engineers try to fit their dynamical model into a $1$-Triangular System model. This is commonly seen in the backstepping control community in which they have developed pioneering adaptive control laws which can explicitly account for operating state constraints. We shall demonstrate that such control laws can even be implemented in a non-adaptive form while still addressing actuator limitations such as saturation. However, most importantly, by removing the adaptation component, a {\em strictly output passive} input-output mapping can be realized. This important property is most applicable to the networked control community. For the networked control community, this {\em key property} allows us to integrate an aircraft into our framework such that a {\em discrete-time lag compensator} can be used by a ground control station for remote navigation in a {\em safe and stable manner in spite of time-varying delays and random data loss}. The applicability of our result shall be made clear as we demonstrate how an inertial navigation system for a quadrotor aircraft can be constructed. Specifically: i) the desired inertial position ($\zeta_s=[\zeta_{Ns},\zeta_{Es},\zeta_{Ds}]\tr$) and yaw ($\psi_s$) setpoints can be concatenated to consist of the {\em virtual} desired setpoint ($\bar{u}=[\zeta_s \tr, \psi_s]\tr$); ii) the {\em virtual} desired setpoint corresponds to the $m=3$-concatenated state outputs $\bar{x}=[x_{(1,1)}\tr,x_{(2,1)}\tr,x_{(3,1)}\tr]\tr = [[\zeta_{N},\zeta_{E}],\zeta_{D},\psi]\tr$; which iii) are augmented such that the output $\bar{v}$ equals $\bar{x}$ at steady-state operation; iv) using Lemma~\ref{L:sop_bstep} we can show that the backstepping framework renders the quadrotor aircraft to be strictly output passive (sop) ($\dot{V}(v) \leq -\epsilon_b \bar{v}\tr \bar{v} + \bar{v}\tr \bar{u}$) such that $V(v)=\frac{1}{2}v\tr v$ is a Lyapunov function in terms of all concatenated system states $v$ associated with the $m$-Triangular System. Lemma~\ref{L:PassiveClosedLoop} then shows how the resulting continuous-time strictly output passive system involving the quadrotor aircraft can be integrated into an advanced digital control framework such that a strictly output passive {\em discrete-time lag} compensator can be used to control the inertial position from a ground-station in an $L^m_2$-stable manner such that time-delays and data loss will not cause instabilities.

In model-based development, verification techniques can be used to check whether an abstract model satisfies a set of properties. Ideally, implementation code generated from these models can also be verified against similar properties. However, the distance between the property specification languages and the implementation makes verifying such generated code difficult. Optimizations and renamings can blur the correspondence between the two, further increasing the difficulty of specifying verification properties on the generated code. This paper describes methods for specifying verification properties on abstract models that are then checked on implementation level code. These properties are translated by an extended code generator into implementation code and special annotations that are used by a software model checker.

Component-based middleware, such as the Lightweight CORBA Component Model, are increasingly used to implement large-scale distributed real-time and embedded (DRE) systems. In addition to supporting the quality of service (QoS) requirements of individual DRE systems, component technologies must also support bounded latencies when effecting deployment changes to DRE systems in response to changing environmental conditions and operational requirements. This paper makes three contributions to the study of predictable deployment latencies in DRE systems. First, we describe OMG's Deployment and Configuration (D\&C) specification for component-based systems and discuss how conventional implementations of this standard can significantly degrade deployment latencies. Second, we describe architectural changes and performance optimizations implemented within the Locality-Enhanced Deployment and Configuration Engine (LE-DAnCE) implementation of the D\&C specification. Finally, we analyze the performance of LE-DAnCE in the context of component deployments on 10 nodes for a representative DRE system consisting of 1,000 components. Our results show LE-DAnCE's optimizations provide a bounded deployment latency of less than 2 seconds with 4 percent jitter.

The rapidly increasing use of information technology in constructing real-world systems has led to the urgent need for a sound systematic approach in designing networked control systems. Communication delays and other uncertainties complicate the development and analysis of these systems. This paper describes a prototype modeling language for the design of networked control systems using passivity to decouple the control design from network uncertainties. The modeling language includes an integrated analysis tool to check for passivity and code generators for simulation in MATLAB/Simulink using the TrueTime platform modeling toolbox and for running actual experiments. The resulting designs are by construction robust to platform effects and implementation uncertainties.

This paper is aimed at presenting a concept of a flexible diagramming framework for building engineering and educational applications. The framework was designed to serve as a platform for online services and collaborative environments where users typically work on remotely stored, shared data through a browser-based user interface. The paper summarizes the common requirements towards such services, overviews related approaches and gives insights into some design challenges through the analysis of use-cases. The design problem is examined from a user-centered view: the key motivation of our research is to find innovative, possibly device-independent solutions that enable seamless user experiences. Finally a generic framework based on a HTML-JavaScript library is proposed, which could be employed for implementing wide range of software solutions from e-learning to cloud-based modeling environments.

Traditional wireless sensor network architectures are based on low-power microcontrollers and highly integrated short range radio transceiver chips operating in one of the few ISM bands. This combination provides a convenient and proven approach to design and build inexpensive sensor nodes rapidly. However, the black box nature of these radio chips severely limit experimentation and research with novel and innovative technologies in the wireless infrastructure. Our team previously proposed a revolutionary architecture for wireless nodes based on Flash FPGA devices. This paper shows the rst results of our work through the implementation and evaluation of a simple baseband FSK modem in the SmartFusion FPGA fabric. We also demonstrate how we could leverage existing software radio projects to use the baseband modem in a wide range of radio frequency bands.

In large programs such as NASA Exploration, multiple systems that interact via safety-critical protocols are already designed with different Statechart variants. To verify these safety-critical systems, a unified framework is needed based on a formal semantics that captures the variants of Statecharts. We describe Polyglot, a unified framework for the analysis of models described using multiple Statechart formalisms. In this framework, Statechart models are translated into Java and analyzed using pluggable semantics for different variants operating in a polymorphic execution environment. The framework has been built on the basis of a parametric formal semantics that captures the common core of Statecharts with extensions for different variants, and addresses previous limitations. Polyglot has been integrated with the Java Jathfinder verification tool-set, providing analysis and test-case generation capabilities. We describe the application of this unified framework to the analysis of NASA/JPL's MER Arbiter whose interacting components were modeled using multiple Statechart formalisms.

The paper presents a novel sensor fusion technique to shooter localization using a wireless network of single-channel acoustic sensors. The unique challenge is that the number of available sensors is very limited. The first contribution of the work is an approach to estimate the miss distance of the shot and the range to the shooter from a single shot using a single sensor. The second contribution is the novel sensor fusion algorithm itself that fuses the miss distance and range estimates of the individual nodes as well as their Time of Arrival observations of the shockwave and the muzzle blast. The performance of both the single sensor method and the network fusion are very promising.

Metamodeling is foundational to many modeling frameworks, and so it is important to formalize and reason about it. Ideally, correctness proofs and test-case generation on the metamodeling framework should be automatic. However, it has yet to be shown that extensive automated reasoning on metamodeling frameworks can be achieved. In this paper we present one approach to this problem: Metamodeling frameworks are specified modularly using algebraic data types and constraint logic programming (CLP). Proofs and test-case generation are encoded as CLP satisfiability problems and automatically solved.