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.

Design, specification, and synthesis of aircraft electric power systems control logic

Cyber-physical systems integrate computation, networking, and physical processes. Substantial research challenges exist in the design and verification of such large-scale, distributed sensing, ac- tuation, and control systems. Rapidly improving technology and recent advances in control theory, networked systems, and computer science give us the opportunity to drastically improve our approach to integrated flow of information and cooperative behavior. Current systems rely on text-based spec- ifications and manual design. Using new technology advances, we can create easier, more efficient, and cheaper ways of developing these control systems. This thesis will focus on design considera- tions for system topologies, ways to formally and automatically specify requirements, and methods to synthesize reactive control protocols, all within the context of an aircraft electric power system as a representative application area.

This thesis consists of three complementary parts: synthesis, specification, and design. The first section focuses on the synthesis of central and distributed reactive controllers for an aircraft elec- tric power system. This approach incorporates methodologies from computer science and control. The resulting controllers are correct by construction with respect to system requirements, which are formulated using the specification language of linear temporal logic (LTL). The second section addresses how to formally specify requirements and introduces a domain-specific language for electric power systems. A software tool automatically converts high-level requirements into LTL and synthesizes a controller.

The final sections focus on design space exploration. A design methodology is proposed that uses mixed-integer linear programming to obtain candidate topologies, which are then used to synthesize controllers. The discrete-time control logic is then verified in real-time by two methods: hardware and simulation. Finally, the problem of partial observability and dynamic state estimation is ex- plored. Given a set placement of sensors on an electric power system, measurements from these sensors can be used in conjunction with control logic to infer the state of the system.

Functional evaluation of noncovalent interactions in neuroreceptors and progress toward the expansion of unnatural amino acid methodology

This dissertation primarily describes chemical-scale studies of G protein-coupled receptors and Cys-loop ligand-gated ion channels to better understand ligand binding interactions and the mechanism of channel activation using recently published crystal structures as a guide. These studies employ the use of unnatural amino acid mutagenesis and electrophysiology to measure subtle changes in receptor function.

In chapter 2, the role of a conserved aromatic microdomain predicted in the D3 dopamine receptor is probed in the closely related D2 and D4 dopamine receptors. This domain was found to act as a structural unit near the ligand binding site that is important for receptor function. The domain consists of several functionally important noncovalent interactions including hydrogen bond, aromatic-aromatic, and sulfur-π interactions that show strong couplings by mutant cycle analysis. We also assign an alternate interpretation for the linear fluorination plot observed at W6.48, a residue previously thought to participate in a cation-π interaction with dopamine.

Chapter 3 outlines attempts to incorporate chemically synthesized and in vitro acylated unnatural amino acids into mammalian cells. While our attempts were not successful, method optimizations and data for nonsense suppression with an in vivo acylated tRNA are included. This chapter is aimed to aid future researchers attempting unnatural amino acid mutagenesis in mammalian cells.

Chapter 4 identifies a cation-π interaction between glutamate and a tyrosine residue on loop C in the GluClβ receptor. Using the recently published crystal structure of the homologous GluClα receptor, other ligand-binding and protein-protein interactions are probed to determine the similarity between this invertebrate receptor and other more distantly related vertebrate Cys-loop receptors. We find that many of the interactions previously observed are conserved in the GluCl receptors, however care must be taken when extrapolating structural data.

Chapter 5 examines inherent properties of the GluClα receptor that are responsible for the observed glutamate insensitivity of the receptor. Chimera synthesis and mutagenesis reveal the C-terminal portion of the M4 helix and the C-terminus as contributing to formation of the decoupled state, where ligand binding is incapable of triggering channel gating. Receptor mutagenesis was unable to identify single residue mismatches or impaired protein-protein interactions within this domain. We conclude that M4 helix structure and/or membrane dynamics are likely the cause of ligand insensitivity in this receptor and that the M4 helix has an role important in the activation process.