Humans rely upon embedded computational systems for everything from mundane tasks, like building temperature control, to safety-critical tasks, like flight control systems. Design and validation of safety-critical cyber-physical systems requires a rigorous focus on behavioral determinism and correctness. The burgeoning scale and complexity of many safety-critical systems makes fully determining their behavior problematic. The time-triggered approach for system design has been shown to provide a powerful abstraction for reducing the behavioral complexity of distributed systems while increasing the ability to detect and mitigate faults. Time-triggered design principles have been embraced by many design and analysis tools, but no consistent formal definition exists across them. Despite using time-triggered approaches, the task of developing and validating safety-critical systems is not without challenges. Among these are realizing robust time-triggered execution, analyzing the impact of deployment, and scaling simulation platforms for larger systems. In this thesis we formally define a time-triggered model of computation and develop a modeling language and toolchain to exploit this definition for the design and validation of high-confidence embedded systems. Any model of computation must concisely capture the execution semantics of a system while facilitating an analytic understanding of useful properties. Our time-triggered model of computation focuses on the temporal execution of a distributed control system and allows designers to easily analyze properties, such as determinism, schedulability, and response latency. We discuss the ESMoL modeling language for designing systems that conform to our model of computation. Using tools integrated into the modeling environment, designers are able to synthesize executables that realize the deterministic timing properties of the model, analyze the performance impact of deploying models onto actual hardware platforms, and to transform models into distributed and heterogenous simulations.

Industrial control systems are used in countless industries, from electric power distribution to the production of pharmaceuticals. These large networked computer systems, often called SCADA systems, allow computer-based networked control over a geographically distributed process. These systems are critical to the safety and productivity of society, and protecting them from computer-based attacks is an important area of research. Testing novel control algorithms and network attack mitigation strategies is a difficult task, however, because developing simulations involves integrating many diverse simulation engines. <p> The C2WindTunnel platform was developed to ease the development and deployment of large-scale simulations. It makes use of model-based design techniques and an intuitive graphical interface to allow integration of diverse simulation engines. This thesis describes the extension of C2WindTunnel to support SCADA simulation development and deployment, including the adaptation of the simulation integration interface and the addition of network simulation support. A case study is provided to demonstrate the use of the C2WindTunnel platform for development of a SCADA system simulation.

Domain-specific modeling languages (DSMLs) are specialized languages tailored with concepts and features of a particular domain. The abstractions offered by DSMLs allow designers of software systems to ignore implementation details and instead focus on the system at a high level. While higher levels of abstraction can offer many advantages, there are still unresolved issues with DSMLs. One of these is the difficulty of applying formal verification methods. This dissertation presents two contributions that assist with the formal verification of domain-specific models. The first is a unified framework in which Statechart models of different semantic variants can be defined, simulated and verified. The key idea is that the user describes only the structure of a model, and then selects the semantics from a set of pluggable components. This allows a single model to be executed using multiple semantics, and a system comprised of interacting models using different semantics can be simulated and verified in a single environment. A lightweight method for specifying properties based on a pattern system was also developed. To perform analysis, the framework is integrated with Java Pathfinder, a software model checker, and Symbolic Pathfinder, its symbolic execution engine. Symbolic execution allows both test-vector generation and reachability analysis. The second major contribution is an extension to Formula, a modeling language and analysis tool from Microsoft Research, that calculates execution traces of models. The behavioral semantics are defined as a set of model transformations, each of which represents an atomic step of execution. The trace computing extension consists of three components. The first is a component that applies all applicable transformations to an input model at a given step and creates a separate trace for each application. The second component is used to create a separate trace for each non-deterministic choice of the input parameters that are passed to a transformation, making non-determinism inside a single execution step explicit to the trace computing module. The third component stores execution traces efficiently by computing and storing only the differences between consecutive steps in a trace when possible.

This work presents new methods and algorithms concerning fiducial-based registration in the presence of anisotropic fiducial localization error (FLE). Since the introduction of image-guided surgery about twenty years ago, the fiducial registration algorithms on which it is based have assumed that FLE is isotropic. However, even the best modern tracking systems produce error that is highly anisotropic, with FLE components that are two or three times greater in one direction than in the two perpendicular directions. In this work we introduce novel algorithms that allow for anisotropic FLE and for anisotropic weighting by the registration algorithm. Using knowledge of these anisotropies, we present a new method for fiducial registration that is faster and more accurate than comparable algorithms and we provide a general approach for predicting covariances for fiducial registration error (FRE) and for target registration error (TRE). We also present a novel method of tracking when FLE is anisotropic that calculates the anisotropy and uses it for registration in real time. We validate both these algorithms with computer simulations and real data. Finally, we present a new robotic system for performing a mastoidectomy, and we present a new trajectory building algorithm tailored to this application. We present experiments on cadaveric bones that show that accuracy and execution time is comparable to those of a human surgeon. This robotic system represents a tool for future experiments to evaluate new methods and new algorithms for fiducial registration in the presence of anisotropic FLE.

<p>Building preliminary mathematical models to simulate system behavior is an essential part of designing dependable cyber-physical systems (CPS). This thesis presents the implementation of a visual modeling environment that supports compositional component-based modeling and simulation of cyber-physical systems. For this purpose, we have designed a domain specific modeling language (DSML), then implemented two model interpreters, and a Matlab block- and function- library to support the model building and simulation tasks.</p> <p>The modeling language employs the hybrid bond graph formalism to facilitate building cross-domain physical system models, and an extended version of the Grafcet model of computation to formally represent and analyze the discrete behavior evolution of the hybrid system. Domain models complying with the DSML capture the Functional, Behavioral and Structural aspects of the system, by explicitly modeling the interaction of the physical processes and the controlling computational units. The associated model interpreter automates the generation of hybrid simulation models. Grafcet models also incorporate logical constraints to express functional requirements for the system in the form of Hoare triples.</p> <p>Finally, the thesis also presents a case study, which describes the approach to model building and simulation of the Reverse Osmosis subsystem of the NASA Advanced Life Support System. The original test results from the testbed at NASA Johnson Space Center confirm the correctness of our model and simulation results.</p>

Wireless mesh networks have attracted increasing attention and deployment as a high-performance and low-cost solution to last-mile broadband Internet access. The capability of balancing the traffic load along different paths over different spatial regions and across difference spectrums plays a critical role in determining the performance of a wireless mesh network. To investigate the best solution, existing work proposes to formulate the mesh network load balancing problem as an optimization problem. In this problem formulation, traffic demand is usually implicitly assumed as static and known a priori. Contradictorily, recent studies of wireless network traces show that the traffic demand, even being aggregated at access points, is highly dynamic and hard to estimate. Thus, in order to apply an optimization-based solution to practice, the dynamic and volatile nature of wireless traffic demand has to be taken into account. In this dissertation, I propose an integrated framework for wireless mesh network routing under dynamic traffic demand. This framework consists of two important components: traffic estimation and traffic distribution. To perform traffic estimation, I analyze the traffic traces collected from actual wireless networks and build time series models to characterize and predict traffic load at wireless access points. To identify the optimal traffic distribution strategies that can incorporate the uncertainty in traffic estimation and balance the traffic load, I first formulate the uncertainty-aware wireless routing problem for single-channel and single-radio mesh networks as a stochastic optimization problem and develop a fast approximation algorithm to solve it. This baseline routing problem formulation and algorithm are further extended to handle the task of traffic distribution in multi-channel and multi-radio networks via joint channel assignment and routing. Extensive simulation studies are performed at both flow level and packet level. The results show that our integrated traffic estimation and distribution solution can significantly improve the expected network performance under dynamic wireless traffic load.

This thesis introduces graph class C, a recognition algorithm for graphs in the class, and shows that some problems are NP-complete on the class. Class C is a generalization of chordal graphs. Informally, a graph is in class C if successively removing the neighborhoods of its simplicial vertices produces a null graph. More precisely, a graph G is in class C if G is the null graph or G contains a simplicial vertex v such that G - N[v] is in C. A greedy algorithm can recognize whether a graph is in class C in O(nm) time. The maximum independent set problem and the clique cover problem on class C can be solved in linear time using greeedy algorithms. However, the maximum clique problem and the coloring problem are NP-complete on the class. This work also examines class K, the class of graphs in class C whose complements are also in class C, and shows that the maximum weighted independent set problem is NP-complete on the class. Class K generalizes split graphs, the class of graphs that are chordal and co-chordal. The four problems mentioned in relation to class C can be solved in linear time on class K using greedy algorithms. The same is known to be true for split graphs. However, while the maximum weighted independent set problem can be solved in polynomial time on split graphs, this problem is NP-complete on class K.

The recent advancement in compression techniques and networking technologies have resulted in wide deployment of novel content distribution applications. These applications enable the end-users to have ubiquitous access to media streaming services such as live broadcasting, video-on-demand, and video conferencing. Peer-to-peer (P2P) has become the most popular means for media distribution because it provides an application-layer platform that can abstract the underlying network heterogeneity. However, the lack of dedicated bandwidth means that P2P systems must implement proper resource-allocation techniques to optimally utilize available bandwidth. In the thesis, we present bandwidth optimization algorithms for two types of media streams: Continuous and Scalable. In continuous stream, we present an optimization algorithm based on Convex Optimization framework. For scalable stream, we present a distributed message-passing framework for optimization using sum-product update algorithm. Advantage of this approach over existing heuristic-based algorithm is that the optimization algorithm itself is independent of the underlying constraints. The algorithm iteratively updates resource allocation decision based on a given set of codewords. The codewords are binary representation of various network and video constraints. Therefore, any number of constraints can be used to generate a set of codewords without modifying the algorithm.

As distributed and real-time systems become more pervasive, there is growing interest in their performance and reliability. The workloads found in these environments can exhibit variability that results in unpredictable and undesirable system behavior. Therefore, a key requirement in analyzing such systems is developing robust models and tools that accurately replicate the task workload and correctly mimic the variability found in real-world environments. Based on observations made during a case study of an enterprise grid environment, the method of stages modeling technique is adopted and applied to the performance evaluation of soft real-time systems. This approach achieves a two-moment match of performance parameters and allows the effects of variance to be studied in a uniform and systematic manner. Based on this technique, a new discrete-event simulator, the Method Of Stages Simulator (MOSS), is developed and used to conduct sensitivity analysis experiments on the variance of task parameters such as arrival, service, and deadline rates. The Matlab State-space Analysis Tool (MSAT) is also developed, which constructs and analytically solves state-space models representing small real-time systems. Traditional real-time scheduling algorithms such as Rate Monotonic (RM), Earliest Deadline First (EDF), and Least Laxity First (LLF) ignore the variance of performance parameters when allocating resources. However, this variance can directly influence the choice of the best scheduling algorithm, particularly under varying system loads. Explicit incorporation of variance in scheduling decisions leads to hybrid scheduling algorithms that are insensitive to, or unaffected by, the workload variability. Results from MOSS sensitivity analysis experiments suggest a promising new scheduling algorithm, TLAX (Threshold LAXity), that outperforms the traditional algorithms by as much as 50% in heavy load conditions. MSAT is used to analytically validate the results obtained from MOSS and to gain further insight into the robust TLAX algorithm. The explicit incorporation of variance in the performance modeling of scheduling algorithms improves the design, efficiency, and performance of distributed and soft real-time systems.

Mobile devices, such as smartphones, are becoming increasingly common in everyday life, and enable the development of dynamic, data driven applications which werent possible prior to the advent of the smartphone. This paper describes a data distribution system, called AMMO (Android Mobile Middleware Objects), which is designed to allow the efficient construction of such applications, focusing specifically on its server-side component, the AMMO Gateway. The gateway is the centralized system which manages the distribution of data between applications and services using the AMMO system, and provides a point of integration for third-party services outside the AMMO system.