Refinement methods for software architecture design using the software architecture model

Modern software systems are often large and complicated. To better understand, develop, and manage large software systems, researchers have studied software architectures that provide the top level overall structural design of software systems for the last decade. One major research focus on software architectures is formal architecture description languages, but most existing research focuses primarily on the descriptive capability and puts less emphasis on software architecture design methods and formal analysis techniques, which are necessary to develop correct software architecture design. ^ Refinement is a general approach of adding details to a software design. A formal refinement method can further ensure certain design properties. This dissertation proposes refinement methods, including a set of formal refinement patterns and complementary verification techniques, for software architecture design using Software Architecture Model (SAM), which was developed at Florida International University. First, a general guideline for software architecture design in SAM is proposed. Second, specification construction through property-preserving refinement patterns is discussed. The refinement patterns are categorized into connector refinement, component refinement and high-level Petri nets refinement. These three levels of refinement patterns are applicable to overall system interaction, architectural components, and underlying formal language, respectively. Third, verification after modeling as a complementary technique to specification refinement is discussed. Two formal verification tools, the Stanford Temporal Prover (STeP) and the Simple Promela Interpreter (SPIN), are adopted into SAM to develop the initial models. Fourth, formalization and refinement of security issues are studied. A method for security enforcement in SAM is proposed. The Role-Based Access Control model is formalized using predicate transition nets and Z notation. The patterns of enforcing access control and auditing are proposed. Finally, modeling and refining a life insurance system is used to demonstrate how to apply the refinement patterns for software architecture design using SAM and how to integrate the access control model. ^ The results of this dissertation demonstrate that a refinement method is an effective way to develop a high assurance system. The method developed in this dissertation extends existing work on modeling software architectures using SAM and makes SAM a more usable and valuable formal tool for software architecture design. ^

Analysis and design of tall concrete buildings : an investigation regarding the use of cracked versus un-cracked moment of inertia

A debate is currently prevalent among the structural engineers regarding the use of cracked versus un-cracked moment of inertia of the structural elements in analyzing and designing tall concrete buildings. (The basic definition of a tall building, according to the Journal of Structural Design of Tall Buildings Vol. 13. No. 5, 2004 is a structure that is equal to or greater than 160 feet in height, or 6 stories or greater.) The controversy is the result of differing interpretations of certain ACI (American Concrete Institute) code provisions. The issue is whether designers should use cracked moment of inertia in order to estimate lateral deflection and whether the computed lateral deflection should be used to carry out subsequent second-order analysis (analysis considering the effect of first order lateral deflections on bending moment and shear stresses). On one hand, bending moments and shear forces estimated based on un-cracked moment of inertia of the sections may result in conservative designs by overestimating moments and shears. On the other hand, lateral deflections may be underestimated due to the same analyses resulting in unsafe designs.

Computational evaluation of wind loads on low- and highrise buildings

Buildings and other infrastructures located in the coastal regions of the US have a higher level of wind vulnerability. Reducing the increasing property losses and causalities associated with severe windstorms has been the central research focus of the wind engineering community. The present wind engineering toolbox consists of building codes and standards, laboratory experiments, and field measurements. The American Society of Civil Engineers (ASCE) 7 standard provides wind loads only for buildings with common shapes. For complex cases it refers to physical modeling. Although this option can be economically viable for large projects, it is not cost-effective for low-rise residential houses. To circumvent these limitations, a numerical approach based on the techniques of Computational Fluid Dynamics (CFD) has been developed. The recent advance in computing technology and significant developments in turbulence modeling is making numerical evaluation of wind effects a more affordable approach. The present study targeted those cases that are not addressed by the standards. These include wind loads on complex roofs for low-rise buildings, aerodynamics of tall buildings, and effects of complex surrounding buildings. Among all the turbulence models investigated, the large eddy simulation (LES) model performed the best in predicting wind loads. The application of a spatially evolving time-dependent wind velocity field with the relevant turbulence structures at the inlet boundaries was found to be essential. All the results were compared and validated with experimental data. The study also revealed CFD's unique flow visualization and aerodynamic data generation capabilities along with a better understanding of the complex three-dimensional aerodynamics of wind-structure interactions. With the proper modeling that realistically represents the actual turbulent atmospheric boundary layer flow, CFD can offer an economical alternative to the existing wind engineering tools. CFD's easy accessibility is expected to transform the practice of structural design for wind, resulting in more wind-resilient and sustainable systems by encouraging optimal aerodynamic and sustainable structural/building design. Thus, this method will help ensure public safety and reduce economic losses due to wind perils.

Computational Evaluation of Wind Loads on Low- and High- Rise Buildings

Buildings and other infrastructures located in the coastal regions of the US have a higher level of wind vulnerability. Reducing the increasing property losses and causalities associated with severe windstorms has been the central research focus of the wind engineering community. The present wind engineering toolbox consists of building codes and standards, laboratory experiments, and field measurements. The American Society of Civil Engineers (ASCE) 7 standard provides wind loads only for buildings with common shapes. For complex cases it refers to physical modeling. Although this option can be economically viable for large projects, it is not cost-effective for low-rise residential houses. To circumvent these limitations, a numerical approach based on the techniques of Computational Fluid Dynamics (CFD) has been developed. The recent advance in computing technology and significant developments in turbulence modeling is making numerical evaluation of wind effects a more affordable approach. The present study targeted those cases that are not addressed by the standards. These include wind loads on complex roofs for low-rise buildings, aerodynamics of tall buildings, and effects of complex surrounding buildings. Among all the turbulence models investigated, the large eddy simulation (LES) model performed the best in predicting wind loads. The application of a spatially evolving time-dependent wind velocity field with the relevant turbulence structures at the inlet boundaries was found to be essential. All the results were compared and validated with experimental data. The study also revealed CFD’s unique flow visualization and aerodynamic data generation capabilities along with a better understanding of the complex three-dimensional aerodynamics of wind-structure interactions. With the proper modeling that realistically represents the actual turbulent atmospheric boundary layer flow, CFD can offer an economical alternative to the existing wind engineering tools. CFD’s easy accessibility is expected to transform the practice of structural design for wind, resulting in more wind-resilient and sustainable systems by encouraging optimal aerodynamic and sustainable structural/building design. Thus, this method will help ensure public safety and reduce economic losses due to wind perils.

An innovative approach to teaching structural induction for computer science

Proofs by induction are central to many computer science areas such as data structures, theory of computation, programming languages, program efficiency-time complexity, and program correctness. Proofs by induction can also improve students’ understanding and performance of computer science concepts such as programming languages, algorithm design, and recursion, as well as serve as a medium for teaching them. Even though students are exposed to proofs by induction in many courses of their curricula, they still have difficulties understanding and performing them. This impacts the whole course of their studies, since proofs by induction are omnipresent in computer science. Specifically, students do not gain conceptual understanding of induction early in the curriculum and as a result, they have difficulties applying it to more advanced areas later on in their studies. The goal of my dissertation is twofold: (1) identifying sources of computer science students’ difficulties with proofs by induction, and (2) developing a new approach to teaching proofs by induction by way of an interactive and multimodal electronic book (e-book). For the first goal, I undertook a study to identify possible sources of computer science students’ difficulties with proofs by induction. Its results suggest that there is a close correlation between students’ understanding of inductive definitions and their understanding and performance of proofs by induction. For designing and developing my e-book, I took into consideration the results of my study, as well as the drawbacks of the current methodologies of teaching proofs by induction for computer science. I designed my e-book to be used as a standalone and complete educational environment. I also conducted a study on the effectiveness of my e-book in the classroom. The results of my study suggest that, unlike the current methodologies of teaching proofs by induction for computer science, my e-book helped students overcome many of their difficulties and gain conceptual understanding of proofs induction.

Study of carbon nanotube film and shape memory alloys treatment for sensing and structural vibration control

Structural vibration control is of great importance. Current active and passive vibration control strategies usually employ individual elements to fulfill this task, such as viscoelastic patches for providing damping, transducers for picking up signals and actuators for inputting actuating forces. The goal of this dissertation work is to design, manufacture, investigate and apply a new type of multifunctional composite material for structural vibration control. This new composite, which is based on multi-walled carbon nanotube (MWCNT) film, is potentially to function as free layer damping treatment and strain sensor simultaneously. That is, the new material integrates the transducer and the damping patch into one element. The multifunctional composite was prepared by sandwiching the MWCNT film between two adhesive layers. Static sensing test indicated that the MWCNT film sensor resistance changes almost linearly with the applied load. Sensor sensitivity factors were comparable to those of the foil strain gauges. Dynamic test indicated that the MWCNT film sensor can outperform the foil strain gage in high frequency ranges. Temperature test indicated the MWCNT sensor had good temperature stability over the range of 237 K-363 K. The Young’s modulus and shear modulus of the MWCNT film composite were acquired by nanoindentation test and direct shear test, respectively. A free vibration damping test indicated that the MWCNT composite sensor can also provide good damping without adding excessive weight to the base structure. A new model for sandwich structural vibration control was then proposed. In this new configuration, a cantilever beam covered with MWCNT composite on top and one layer of shape memory alloy (SMA) on the bottom was used to illustrate this concept. The MWCNT composite simultaneously serves as free layer damping and strain sensor, and the SMA acts as actuator. Simple on-off controller was designed for controlling the temperature of the SMA so as to control the SMA recovery stress as input and the system stiffness. Both free and forced vibrations were analyzed. Simulation work showed that this new configuration for sandwich structural vibration control was successful especially for low frequency system.

Structural Characterization of Metal Hydrides for Energy Applications

Hydrogen can be an unlimited source of clean energy for future because of its very high energy density compared to the conventional fuels like gasoline. An efficient and safer way of storing hydrogen is in metals and alloys as hydrides. Light metal hydrides, alanates and borohydrides have very good hydrogen storage capacity, but high operation temperatures hinder their application. Improvement of thermodynamic properties of these hydrides is important for their commercial use as a source of energy. Application of pressure on materials can have influence on their properties favoring hydrogen storage. Hydrogen desorption in many complex hydrides occurs above the transition temperature. Therefore, it is important to study the physical properties of the hydride compounds at ambient and high pressure and/or high temperature conditions, which can assist in the design of suitable storage materials with desired thermodynamic properties. ^ The high pressure-temperature phase diagram, thermal expansion and compressibility have only been evaluated for a limited number of hydrides so far. This situation serves as a main motivation for studying such properties of a number of technologically important hydrides. Focus of this dissertation was on X-ray diffraction and Raman spectroscopy studies of Mg2FeH6, Ca(BH4) 2, Mg(BH4)2, NaBH4, NaAlH4, LiAlH4, LiNH2BH3 and mixture of MgH 2 with AlH3 or Si, at different conditions of pressure and temperature, to obtain their bulk modulus and thermal expansion coefficient. These data are potential source of information regarding inter-atomic forces and also serve as a basis for developing theoretical models. Some high pressure phases were identified for the complex hydrides in this study which may have better hydrogen storage properties than the ambient phase. The results showed that the highly compressible B-H or Al-H bonds and the associated bond disordering under pressure is responsible for phase transitions observed in brorohydrides or alanates. Complex hydrides exhibited very high compressibility suggesting possibility to destabilize them with pressure. With high capacity and favorable thermodynamics, complex hydrides are suitable for reversible storage. Further studies are required to overcome the kinetic barriers in complex hydrides by catalytic addition. A comparative study of the hydride properties with that of the constituting metal, and their inter relationships were carried out with many interesting features.^

Pressure induced structural changes and gas diffusion pathways in monomeric fluorescent proteins

Fluorescent proteins (FPs) are extremely valuable biochemical markers which have found a wide range of applications in cellular and molecular biology research. The monomeric variants of red fluorescent proteins (RFPs), known as mFruits, have been especially valuable for in vivo applications in mammalian cell imaging. Fluorescent proteins consist of a chromophore caged in the beta-barrel protein scaffold. The photophysical properties of an FP is determined by its chromophore structure and its interactions with the protein barrel. Application of hydrostatic pressure on FPs results in the modification of the chromophore environment which allows a systematic study of the role of the protein-chromophore interactions on photophysical properties of FPs. Using Molecular Dynamics (MD) computer simulations, I investigated the pressure induced structural changes in the monomeric variants mCherry, mStrawberry, and Citrine. The results explain the molecular basis for experimentally observed pressure responses among FP variants. It is found that the barrel flexibility, hydrogen bonding interactions and chromophore planarity of the FPs can be correlated to their contrasting photophysical properties at vaious pressures. I also investigated the oxygen diffusion pathways in mOrange and mOrange2 which exhibit marked differences in oxygen sensitivities as well as photostability. Such computational identifications of structural changes and oxygen diffusion pathways are important in guiding mutagenesis efforts to design fluorescent proteins with improved photophysical properties.

An Innovative Approach to Teaching Structural Induction for Computer Science

Proofs by induction are central to many computer science areas such as data structures, theory of computation, programming languages, program efficiency-time complexity, and program correctness. Proofs by induction can also improve students’ understanding of and performance with computer science concepts such as programming languages, algorithm design, and recursion, as well as serve as a medium for teaching them. Even though students are exposed to proofs by induction in many courses of their curricula, they still have difficulties understanding and performing them. This impacts the whole course of their studies, since proofs by induction are omnipresent in computer science. Specifically, students do not gain conceptual understanding of induction early in the curriculum and as a result, they have difficulties applying it to more advanced areas later on in their studies. The goal of my dissertation is twofold: 1. identifying sources of computer science students’ difficulties with proofs by induction, and 2. developing a new approach to teaching proofs by induction by way of an interactive and multimodal electronic book (e-book). For the first goal, I undertook a study to identify possible sources of computer science students’ difficulties with proofs by induction. Its results suggest that there is a close correlation between students’ understanding of inductive definitions and their understanding and performance of proofs by induction. For designing and developing my e-book, I took into consideration the results of my study, as well as the drawbacks of the current methodologies of teaching proofs by induction for computer science. I designed my e-book to be used as a standalone and complete educational environment. I also conducted a study on the effectiveness of my e-book in the classroom. The results of my study suggest that, unlike the current methodologies of teaching proofs by induction for computer science, my e-book helped students overcome many of their difficulties and gain conceptual understanding of proofs induction.

Pressure Induced Structural Changes and Gas Diffusion Pathways in Monomeric Fluorescent Proteins

Fluorescent proteins (FPs) are extremely valuable biochemical markers which have found a wide range of applications in cellular and molecular biology research. The monomeric variants of red fluorescent proteins (RFPs), known as mFruits, have been especially valuable for in vivo applications in mammalian cell imaging. Fluorescent proteins consist of a chromophore caged in the beta-barrel protein scaffold. The photophysical properties of an FP is determined by its chromophore structure and its interactions with the protein barrel. Application of hydrostatic pressure on FPs results in the modification of the chromophore environment which allows a systematic study of the role of the protein-chromophore interactions on photophysical properties of FPs. Using Molecular Dynamics (MD) computer simulations, I investigated the pressure induced structural changes in the monomeric variants mCherry, mStrawberry, and Citrine. The results explain the molecular basis for experimentally observed pressure responses among FP variants. It is found that the barrel flexibility, hydrogen bonding interactions and chromophore planarity of the FPs can be correlated to their contrasting photophysical properties at vaious pressures. I also investigated the oxygen diffusion pathways in mOrange and mOrange2 which exhibit marked differences in oxygen sensitivities as well as photostability. Such computational identifications of structural changes and oxygen diffusion pathways are important in guiding mutagenesis efforts to design fluorescent proteins with improved photophysical properties.

Structural Health Monitoring Inside Concrete and Grout Using the Wireless Identification and Sensing Platform (WISP)

This research investigates the implementation of battery-less RFID sensing platforms inside lossy media, such as, concrete and grout. Both concrete and novel grouts can be used for nuclear plant decommissioning as part of the U.S. Department of Energy’s (DOE’s) cleanup projects. Our research examines the following: (1) material characterization, (2) analytical modeling of transmission and propagation losses inside lossy media, (3) maximum operational range of RFID wireless sensors embedded inside concrete and grout, and (4) best positioning of antennas for achieving longer communication range between RFID antennas and wireless sensors. Our research uses the battery-less Wireless Identification and Sensing Platform (WISP) which can be used to monitor temperature, and humidity inside complex materials. By using a commercial Agilent open-ended coaxial probe (HP8570B), the measurements of the dielectric permittivity of concrete and grout are performed. Subsequently, the measured complex permittivity is used to formulate analytical Debye models. Also, the transmission and propagation losses of a uniform plane wave inside grout are calculated. Our results show that wireless sensors will perform better in concrete than grout. In addition, the maximum axial and radial ranges for WISP are experimentally determined. Our work illustrates the feasibility of battery-less wireless sensors that are embedded inside concrete and grout. Also, our work provides information that can be used to optimize the power management, sampling rate, and antenna design of such sensors.