No description available.

Thesis (Ph.D.)--Boston University / PLEASE NOTE: Boston University Libraries did not receive an Authorization To Manage form for this thesis or dissertation. It is therefore not openly accessible, though it may be available by request. If you are the author or principal advisor of this work and would like to request open access for it, please contact us at open-help@bu.edu. Thank you. / This dissertation is dedicated to optimization of Stochastic Hybrid Systems (SHS). The concentration is on both online optimization of these systems and extending the known optimal policies in Discrete-Event Systems (DES) to a broader context of SHS. A SHS involves both continuous and discrete dynamics and is suitable for modeling almost any physical system of interest. The first part of this dissertation focuses on applications of SHS and, particularly, a subclass known as Stochastic Flow Models (SFM) used in fluid scheduling. To this end, a classic problem for optimally allocating a resource to multiple competing user queues is considered in the DES context and placed in the framework of SFMs. Infinitesimal Perturbation Analysis (IPA) is used to calculate the gradient estimates for the average holding cost of this system with respect to resource allocation parameters. The monotonicity property of these estimates allows us to prove the optimality of a well-known rule called the "c - mu-rule" under non-idling policies. Furthermore, nonlinear cost functions are considered, yielding simple distribution-free cost sensitivity estimates. Next, we take the first step in using IPA for optimally calculating timeout thresholds in SHS. A Transmission Control Protocol (TCP) communication link is used to examine the effectiveness of SHS and IPA in calculating derivative estimates of a goodput objective with respect to a timeout parameter. The analysis is also extended to the case of multinode communications. Our results reveal a great potential in using IPA to control delay thresholds and motivate more investigations in future. Finally, we propose a general framework for analysis and on-line optimization of SHS which facilitates the use of IPA. In doing so, we modify the previous structure of a Stochastic Hybrid Automaton (SHA) and show that every transition is associated with an explicit event which is defined through a "guard function." This enables us to uniformly treat all events observed on the sample path of the SHS. As a result, a unifying matrix notation for IPA equations is developed which eliminates the need for the case-by-case analysis of event classes as usually done in prior works involving IPA for SHS. / 2031-01-01

No description available.

This thesis discusses the security of sensor networks. First, an overview of the security architectures of two dominant implementations of sensor networks in the market today is presented: the TinyOS stack and the IEEE 802.15.4 stack. Their similarities and differences are explored and their strength and limitations are discussed. Where applicable, comparisons are made with IEEE 802.11 Wireless LAN to highlight improvements and lessons learned. It is pointed out that in general, IEEE 802.15.4 offers better security, but replay protection is effectively missing in today's implementations and access control is poorly implemented. Consequently, TinyOS is still the better option for devices with severe resource constraints. Finally, as a tool to aid in the security analysis of sensor network, the design and implementation of a TinyOS sniffer is presented and captured frames for a simple sensor network application are analyzed for the purpose of validation.

<p>Various engineering systems have become rapidly automated and intelligent as sensing, communication, and computing technologies have been increasingly advanced. The dynamical behaviors of such systems have also become complicated as they need to meet requirements on performance and safety in various operating conditions. Due to the heterogeneity in its behaviors for different operating modes, it is not appropriate to use a single dynamical model to describe its dynamics, which motivates the development of the stochastic hybrid system (SHS). The SHS is defined as a dynamical system which contains interacting time-evolving continuous state and event-driven discrete state (also called a mode) with uncertainties. Due to its flexibility and effectiveness, the SHS has been widely used for modeling complex engineering systems in many applications such as air traffic control, sensor networks, biological systems, and etc.</p><p>One of the key research areas related to the SHS is the inference or estimation of the states of the SHS, which is also known as the hybrid state estimation. This task is very challenging because both the continuous and discrete states need to be inferred from noisy measurements generated from mixed time-evolving and event-driven behavior of the SHS. This becomes even more difficult when the dynamical behavior or measurement contains nonlinearity, which is the case in many engineering systems that can be modeled as the SHS.</p><p>This research aims to 1) propose a stochastic nonlinear hybrid system model and develop novel nonlinear hybrid state estimation algorithms that can deal with the aforementioned challenges, and 2) apply them to safety-critical applications in air traffic control systems such as aircraft tracking and estimated time of arrival prediction, and unmanned aircraft system traffic management.</p>

During the decade of 1950s, the intensive rural to urban migration, in search for new job opportunities, created a high housing demand that was partially solved by the dictatorial government of Marcos Perez Jimenez. However, in the absence of effective public policy and failed housing projects, the population started to create solutions of their own to satisfy their housing needs, settling themselves in an improvised way around the urbanized areas and constituting what we know today as informal settlements or barrios. By 1957, around 35% of the population of Caracas lived in barrios. During the past decade, Venezuela has experienced a series of changes that have modified the economic, political and social model that governed the country. During Chavez's government, there have been many policy changes regarding property, land, economic and social organization, in search for solutions to the housing problem that integrate the marginalized sector of the population. However, a different pattern of informal settlements has emerged. Some organized communities have started to invade not only vacant land in the city peripheries; they are now invading buildings that are inserted in the center of the city, contrasting to the formal systems already existing in the city. There is now a new interpretation of what is legal and what is not. We are experiencing the changes and understanding the consequences of their implementation. The purpose of this research is to understand the current processes of housing production and acquisition in formal and informal communities in Caracas through a review of existing literature and qualitative studies of the relationships between stakeholders. I analyze the new policies and the current housing production organization system and contrast it to what is actually happening in practice. I also investigated how incremental changes in existing practices can contribute to the development of safe and legible housing production processes. My recommendations are the result of hybrid systems that consider different actors and perspectives of the same reality in order to find a healthier and more sustainable building culture in Caracas. / text

Thesis (Ph.D)--Electrical and Computer Engineering, Georgia Institute of Technology, 2010. / Committee Chair: Egerstedt, Magnus; Committee Co-Chair: Wardi, Yorai; Committee Member: Riley, George; Committee Member: Taylor, David; Committee Member: Tovey, Craig; Committee Member: Yezzi, Anthony. Part of the SMARTech Electronic Thesis and Dissertation Collection.

This thesis is concerned with the problem of formal verification of correctness specifications for continuous and hybrid dynamical systems. Our main focus will be on developing and automating general proof principles for temporal properties of systems described by non-linear ordinary differential equations (ODEs) under evolution constraints. The proof methods we consider will work directly with the differential equations and will not rely on the explicit knowledge of solutions, which are in practice rarely available. Our ultimate goal is to increase the scope of formal deductive verification tools for hybrid system designs. We give a comprehensive survey and comparison of available methods for checking set invariance in continuous systems, which provides a foundation for safety verification using inductive invariants. Building on this, we present a technique for constructing discrete abstractions of continuous systems in which spurious transitions between discrete states are entirely eliminated, thereby extending previous work. We develop a method for automatically generating inductive invariants for continuous systems by efficiently extracting reachable sets from their discrete abstractions. To reason about liveness properties in ODEs, we introduce a new proof principle that extends and generalizes methods that have been reported previously and is highly amenable to use as a rule of inference in a deductive verification calculus for hybrid systems. We will conclude with a summary of our contributions and directions for future work.

Thesis (MTech (Electrical Engineering))--Cape Peninsula University of Technology, 2009 / Traditional high voltage power transformers feature sensors measuring basic parameters from oil and gas and are limited to on-site monitoring. Unforeseen failures and breakdowns on these transformers have led to extensive financial losses even with planned maintenance schedules in place. A distinct need has arisen to actively monitor and identify causes of such failures. However, no or little infrastructure exists for effective remote condition monitoring. Wireless sensor networks can be introduced to actively monitor and identify causes of such failures. Sensor motes in the network are battery operated and therefore constrained by limited energy in these batteries. An alternative to battery-powered sensor motes is the conversion of available energy harvested from the surrounding environment into useable electrical energy powering the sensor motes. The primary objective of this research was to examine methods to harvest energy from both the environment and high voltage power transformer. A low cost and feasibly sized hybrid energy harvesting power management prototype was successfully developed that enabled sustained sensor mote operation for prolonged condition monitoring of high voltage transformers. The sensor mote utilised a piezoelectric cantilever to generate usable electrical energy from the transformer tank vibration. Together with solar energy harvesting, the system allowed for a battery-less self-sustained wireless sensor mote capable of autonomously monitoring its surroundings. The power management system's modular architecture provided for the inclusion of additional energy harvesting techniques. This allowed condition monitoring solutions not exclusively for power transformers but proposed an extensible condition monitoring solution for various applications.

A hybrid dynamical system is a mathematical model for a part of the real world where discrete and continuous parts interact with each other. Typically such systems are complex, and it is difficult to know how they will behave for general parameters and initial conditions. However, the method of formal verification gives us the ability to prove automatically that certain behaviour does or does not happen for a range of parameters in a system. The challenge is then to define suitable methods for proving properties on hybrid systems.This thesis looks at using formal verification for proving liveness properties on hybrid systems: a liveness property says that something good eventually happens in the system. This work presents the theoretical background and practical application of various methods for proving and disproving inevitability properties (a type of liveness) in different classes of hybrid systems. The methods combine knowledge of dynamical behaviour of a system with the brute-force approach of model checking, in order to make the most of the benefits of both sides. The work on proving liveness properties is based on abstraction of dynamical systems to timed automata. This thesis explores the limits of a pre-defined abstraction method, adds some dynamical knowledge to the method, and shows that this improvement makes liveness properties provable in certain continuous dynamical systems. The limits are then pushed further to see how this method can be used for piecewise-continuous dynamical systems. The resulting algorithms are implemented for both classes of systems.In order to disprove liveness properties in hybrid systems a novel framework is proposed, using a new property called deadness. Deadness is a dynamically-aware property of the hybrid system which, if true, disproves the liveness property by means of a finite execution: we usually require an infinite execution to disprove a liveness property. An algorithm is proposed which uses dynamical properties of hybrid systems to derive deadness properties automatically, and the implementation of this algorithm is discussed and applied to a simplified model of an oilwell drillstring.