Analysis-aware design of embedded systems software

In the past many different methodologies have been devised to support software development and different sets of methodologies have been developed to support the analysis of software artefacts. We have identified this mismatch as one of the causes of the poor reliability of embedded systems software. The issue with software development styles is that they are ``analysis-agnostic.'' They do not try to structure the code in a way that lends itself to analysis. The analysis is usually applied post-mortem after the software was developed and it requires a large amount of effort. The issue with software analysis methodologies is that they do not exploit available information about the system being analyzed.

In this thesis we address the above issues by developing a new methodology, called "analysis-aware" design, that links software development styles with the capabilities of analysis tools. This methodology forms the basis of a framework for interactive software development. The framework consists of an executable specification language and a set of analysis tools based on static analysis, testing, and model checking. The language enforces an analysis-friendly code structure and offers primitives that allow users to implement their own testers and model checkers directly in the language. We introduce a new approach to static analysis that takes advantage of the capabilities of a rule-based engine. We have applied the analysis-aware methodology to the development of a smart home application.

Commercial testing of concrete

The material included within this report is the result of a series of tests of concrete specimens taken during the construction of various buildings in the cities of Pasadena and Los Angeles over a period of eight months.

The object of the problem is to determine the effect of the water ratio on the ultimate strength of the concrete as obtained from data observed and recorded from specimens taken from actual building practice rather than that from laboratory specimens made under ideal, or at least more nearly standard conditions.

Stability of Electrode-Electrolyte Interfaces during Charging in Lithium Batteries

In this thesis we study the growth of a Li electrode-electrolyte interface in the presence of an elastic prestress. In particular, we focus our interest on Li-air batteries with a solid electrolyte, LIPON, which is a new type of secondary or rechargeable battery. Theoretical studies and experimental evidence show that during the process of charging the battery the replated lithium adds unevenly to the electrode surface. This phenomenon eventually leads to dendrite formation as the battery is charged and discharged numerous times. In order to suppress or alleviate this deleterious effect of dendrite growth, we put forth a study based on a linear stability analysis. Taking into account all the mechanisms of mass transport and interfacial kinetics, we model the evolution of the interface. We find that, in the absence of stress, the stability of a planar interface depends on interfacial diffusion properties and interfacial energy. Specifically, if Herring-Mullins capillarity-driven interfacial diffusion is accounted for, interfaces are unstable against all perturbations of wavenumber larger than a critical value. We find that the effect of an elastic prestress is always to stabilize planar interfacial growth by increasing the critical wavenumber for instability. A parametric study results in quantifying the extent of the prestress stabilization in a manner that can potentially be used in the design of Li-air batteries. Moreover, employing the theory of finite differences we numerically solve the equation that describes the evolution of the surface profile and present visualization results of the surface evolution by time. Lastly, numerical simulations performed in a commercial finite element software validate the theoretical formulation of the interfacial elastic energy change with respect to the planar interface.