Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic.^ This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.^

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic. This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.

A framework for specification and analysis of software architectures

Software architecture is the abstract design of a software system. It plays a key role as a bridge between requirements and implementation, and is a blueprint for development. The architecture represents a set of early design decisions that are crucial to a system. Mistakes in those decisions are very costly if they remain undetected until the system is implemented and deployed. This is where formal specification and analysis fits in. Formal specification makes sure that an architecture design is represented in a rigorous and unambiguous way. Furthermore, a formally specified model allows the use of different analysis techniques for verifying the correctness of those crucial design decisions. ^ This dissertation presented a framework, called SAM, for formal specification and analysis of software architectures. In terms of specification, formalisms and mechanisms were identified and chosen to specify software architecture based on different analysis needs. Formalisms for specifying properties were also explored, especially in the case of non-functional properties. In terms of analysis, the dissertation explored both the verification of functional properties and the evaluation of non-functional properties of software architecture. For the verification of functional property, methodologies were presented on how to apply existing model checking techniques on a SAM model. For the evaluation of non-functional properties, the dissertation first showed how to incorporate stochastic information into a SAM model, and then explained how to translate the model to existing tools and conducts the analysis using those tools. ^ To alleviate the analysis work, we also provided a tool to automatically translate a SAM model for model checking. All the techniques and methods described in the dissertation were illustrated by examples or case studies, which also served a purpose of advocating the use of formal methods in practice. ^

The development and testing of a multivariate model of differentiation of self among Hispanics

Individuals of Hispanic origin are the nation's largest minority (13.4%). Therefore, there is a need for models and methods that are culturally appropriate for mental health research with this burgeoning population. This is an especially salient issue when applying family systems theories to Hispanics, who are heavily influenced by family bonds in a way that appears to be different from the more individualistic non-Hispanic White culture. Bowen asserted that his family systems' concept of differentiation of self, which values both individuality and connectedness, could be universally applied. However, there is a paucity of research systematically assessing the applicability of the differentiation of self construct in ethnic minority populations. ^ This dissertation tested a multivariate model of differentiation of self with a Hispanic sample. The manner in which the construct of differentiation of self was being assessed and how accurately it represented this particular ethnic minority group's functioning was examined. Additionally, the proposed model included key contextual variables (e.g., anxiety, relationship satisfaction, attachment and acculturation related variables) which have been shown to be related to the differentiation process. ^ The results from structural equation modeling (SEM) analyses confirmed and extended previous research, and helped to illuminate the complex relationships between key factors that need to be considered in order to better understand individuals with this cultural background. Overall results indicated that the manner in which Hispanic individuals negotiate the boundaries of interconnectedness with a sense of individual expression appears to be different from their non-Hispanic White counterparts in some important ways. These findings illustrate the need for research on Hispanic individuals that provides a more culturally sensitive framework. ^

Effects of adolescent depressive symptoms, pubertal development, and interpersonal relationship satisfaction on sexual risk behaviors in adolescent romantic couples

This study examined links between adolescent depressive symptoms, actual pubertal development, perceived pubertal timing relative to one’s peers, adolescent-maternal relationship satisfaction, and couple sexual behavior. Assessments of these variables were made on each couple member separately and then these variables were used to predict the sexual activity of the couple. Participants were drawn from the National Longitudinal Study of Adolescent Health (Add Health; Bearman et al., 1997; Udry, 1997) data set (N = 20,088; aged 12–18 years). Dimensions of adolescent romantic experiences using the total sample were described and then a subsample of romantically paired adolescents ( n = 1,252) were used to test a risk and protective model for predicting couple sexual behavior using the factors noted above. Relevant measures from the Wave 1 Add Health measures were used. Most of the items used in Add Health to assess romantic relationship experiences, adolescent depressive symptoms, pubertal development (actual and perceived), adolescent-maternal relationship satisfaction, and couple sexual behavior were drawn from other national surveys or from scales with well documented psychometric properties. Results demonstrated that romantic relationships are part of most adolescents’ lives and that adolescents’ experiences with these relationships differ markedly by age, sex, and race/ethnicity. Further, each respective couple member’s pubertal development, perceived pubertal timing, and maternal relationship satisfaction were useful in predicting sexual risk-promoting and risk-reducing behaviors in adolescent romantic couples. Findings in this dissertation represent an initial step toward evaluating explanatory models of adolescent couple sexual behavior.

Developing performance measures of mangrove wetlands using simulation models of hydrology, nutrient biogeochemistry, and community dynamics

The goal of mangrove restoration projects should be to improve community structure and ecosystem function of degraded coastal landscapes. This requires the ability to forecast how mangrove structure and function will respond to prescribed changes in site conditions including hydrology, topography, and geophysical energies. There are global, regional, and local factors that can explain gradients of regulators (e.g., salinity, sulfides), resources (nutrients, light, water), and hydroperiod (frequency, duration of flooding) that collectively account for stressors that result in diverse patterns of mangrove properties across a variety of environmental settings. Simulation models of hydrology, nutrient biogeochemistry, and vegetation dynamics have been developed to forecast patterns in mangroves in the Florida Coastal Everglades. These models provide insight to mangrove response to specific restoration alternatives, testing causal mechanisms of system degradation. We propose that these models can also assist in selecting performance measures for monitoring programs that evaluate project effectiveness. This selection process in turn improves model development and calibration for forecasting mangrove response to restoration alternatives. Hydrologic performance measures include soil regulators, particularly soil salinity, surface topography of mangrove landscape, and hydroperiod, including both the frequency and duration of flooding. Estuarine performance measures should include salinity of the bay, tidal amplitude, and conditions of fresh water discharge (included in the salinity value). The most important performance measures from the mangrove biogeochemistry model should include soil resources (bulk density, total nitrogen, and phosphorus) and soil accretion. Mangrove ecology performance measures should include forest dimension analysis (transects and/or plots), sapling recruitment, leaf area index, and faunal relationships. Estuarine ecology performance measures should include the habitat function of mangroves, which can be evaluated with growth rate of key species, habitat suitability analysis, isotope abundance of indicator species, and bird census. The list of performance measures can be modified according to the model output that is used to define the scientific goals during the restoration planning process that reflect specific goals of the project.

Ecology and distribution of diatoms in Biscayne Bay, Florida (USA): Implications for bioassessment and paleoenvironmental studies

The spatial and temporal distribution of planktonic, sediment-associated and epiphytic diatoms among 58 sites in Biscayne Bay, Florida was examined in order to identify diatom taxa indicative of different salinity and water quality conditions, geographic locations and habitat types. Assessments were made in contrasting wet and dry seasons in order to develop robust assessment models for salinity and water quality for this region. We found that diatom assemblages differed between nearshore and offshore locations, especially during the wet season when salinity and nutrient gradients were steepest. In the dry season, habitat structure was primary determinant of diatom assemblage composition. Among a suite of physicochemical variables, water depth and sediment total phosphorus (STP) were most strongly associated with diatom assemblage composition in the dry season, while salinity and water total phosphorus (TP) were more important in the wet season. We used indicator species analysis (ISA) to identify taxa that were most abundant and frequent at nearshore and offshore locations, in planktonic, epiphytic and benthic habitats and in contrasting salinity and water quality regimes. Because surface water concentrations of salts, total phosphorus, nitrogen (TN) and organic carbon (TOC) are partly controlled by water management in this region, diatom-based models were produced to infer these variables in modern and retrospective assessments of management-driven changes. Weighted averaging (WA) and weighted averaging partial least squares (WA-PLS) regressions produced reliable estimates of salinity, TP, TN and TOC from diatoms (r2 = 0.92, 0.77, 0.77 and 0.71, respectively). Because of their sensitivity to salinity, nutrient and TOC concentrations diatom assemblages should be useful in developing protective nutrient criteria for estuaries and coastal waters of Florida.

Development and verification of control and protection strategies in hybrid AC/DC power systems for smart grid applications

Modern power networks incorporate communications and information technology infrastructure into the electrical power system to create a smart grid in terms of control and operation. The smart grid enables real-time communication and control between consumers and utility companies allowing suppliers to optimize energy usage based on price preference and system technical issues. The smart grid design aims to provide overall power system monitoring, create protection and control strategies to maintain system performance, stability and security. This dissertation contributed to the development of a unique and novel smart grid test-bed laboratory with integrated monitoring, protection and control systems. This test-bed was used as a platform to test the smart grid operational ideas developed here. The implementation of this system in the real-time software creates an environment for studying, implementing and verifying novel control and protection schemes developed in this dissertation. Phasor measurement techniques were developed using the available Data Acquisition (DAQ) devices in order to monitor all points in the power system in real time. This provides a practical view of system parameter changes, system abnormal conditions and its stability and security information system. These developments provide valuable measurements for technical power system operators in the energy control centers. Phasor Measurement technology is an excellent solution for improving system planning, operation and energy trading in addition to enabling advanced applications in Wide Area Monitoring, Protection and Control (WAMPAC). Moreover, a virtual protection system was developed and implemented in the smart grid laboratory with integrated functionality for wide area applications. Experiments and procedures were developed in the system in order to detect the system abnormal conditions and apply proper remedies to heal the system. A design for DC microgrid was developed to integrate it to the AC system with appropriate control capability. This system represents realistic hybrid AC/DC microgrids connectivity to the AC side to study the use of such architecture in system operation to help remedy system abnormal conditions. In addition, this dissertation explored the challenges and feasibility of the implementation of real-time system analysis features in order to monitor the system security and stability measures. These indices are measured experimentally during the operation of the developed hybrid AC/DC microgrids. Furthermore, a real-time optimal power flow system was implemented to optimally manage the power sharing between AC generators and DC side resources. A study relating to real-time energy management algorithm in hybrid microgrids was performed to evaluate the effects of using energy storage resources and their use in mitigating heavy load impacts on system stability and operational security.

Potential for Cell-Transplant Therapy with Human Neuronal Precursors to Treat Neuropathic Pain in Models of PNS and CNS Injury: Comparison of hNT2.17 and hNT2.19 Cell Lines

Effective treatment of sensory neuropathies in peripheral neuropathies and spinal cord injury (SCI) is one of the most difficult problems in modern clinical practice. Cell therapy to release antinociceptive agents near the injured spinal cord is a logical next step in the development of treatment modalities. But few clinical trials, especially for chronic pain, have tested the potential of transplant of cells to treat chronic pain. Cell lines derived from the human neuronal NT2 cell line parentage, the hNT2.17 and hNT2.19 lines, which synthesize and release the neurotransmitters gamma-aminobutyric acid (GABA) and serotonin (5HT), respectively, have been used to evaluate the potential of cell-based release of antinociceptive agents near the lumbar dorsal (horn) spinal sensory cell centers to relieve neuropathic pain after PNS (partial nerve and diabetes-related injury) and CNS (spinal cord injury) damage in rat models. Both cell lines transplants potently and permanently reverse behavioral hypersensitivity without inducing tumors or other complications after grafting. Functioning as cellular minipumps for antinociception, human neuronal precursors, like these NT2-derived cell lines, would likely provide a useful adjuvant or replacement for current pharmacological treatments for neuropathic pain.

Chlorine contribution to quantitative structure and activity relationship models of disinfection by -products' quantum chemical descriptors and toxicities

Quantitative Structure-Activity Relationship (QSAR) has been applied extensively in predicting toxicity of Disinfection By-Products (DBPs) in drinking water. Among many toxicological properties, acute and chronic toxicities of DBPs have been widely used in health risk assessment of DBPs. These toxicities are correlated with molecular properties, which are usually correlated with molecular descriptors. The primary goals of this thesis are: (1) to investigate the effects of molecular descriptors (e.g., chlorine number) on molecular properties such as energy of the lowest unoccupied molecular orbital (E LUMO) via QSAR modelling and analysis; (2) to validate the models by using internal and external cross-validation techniques; (3) to quantify the model uncertainties through Taylor and Monte Carlo Simulation. One of the very important ways to predict molecular properties such as ELUMO is using QSAR analysis. In this study, number of chlorine (NCl ) and number of carbon (NC) as well as energy of the highest occupied molecular orbital (EHOMO) are used as molecular descriptors. There are typically three approaches used in QSAR model development: (1) Linear or Multi-linear Regression (MLR); (2) Partial Least Squares (PLS); and (3) Principle Component Regression (PCR). In QSAR analysis, a very critical step is model validation after QSAR models are established and before applying them to toxicity prediction. The DBPs to be studied include five chemical classes: chlorinated alkanes, alkenes, and aromatics. In addition, validated QSARs are developed to describe the toxicity of selected groups (i.e., chloro-alkane and aromatic compounds with a nitro- or cyano group) of DBP chemicals to three types of organisms (e.g., Fish, T. pyriformis, and P.pyosphoreum) based on experimental toxicity data from the literature. The results show that: (1) QSAR models to predict molecular property built by MLR, PLS or PCR can be used either to select valid data points or to eliminate outliers; (2) The Leave-One-Out Cross-Validation procedure by itself is not enough to give a reliable representation of the predictive ability of the QSAR models, however, Leave-Many-Out/K-fold cross-validation and external validation can be applied together to achieve more reliable results; (3) E LUMO are shown to correlate highly with the NCl for several classes of DBPs; and (4) According to uncertainty analysis using Taylor method, the uncertainty of QSAR models is contributed mostly from NCl for all DBP classes.

Effects of Adolescent Depressive Symptoms, Pubertal Development, and Interpersonal Relationship Satisfaction on Sexual Risk Behaviors in Adolescent Romantic Couples

This study examined links between adolescent depressive symptoms, actual pubertal development, perceived pubertal timing relative to one’s peers, adolescent-maternal relationship satisfaction, and couple sexual behavior. Assessments of these variables were made on each couple member separately and then these variables were used to predict the sexual activity of the couple. Participants were drawn from the National Longitudinal Study of Adolescent Health (Add Health; Bearman et al., 1997; Udry, 1997) data set (N = 20,088; aged 12-18 years). Dimensions of adolescent romantic experiences using the total sample were described and then a subsample of romantically paired adolescents (n = 1,252) were used to test a risk and protective model for predicting couple sexual behavior using the factors noted above. Relevant measures from the Wave 1 Add Health measures were used. Most of the items used in Add Health to assess romantic relationship experiences, adolescent depressive symptoms, pubertal development (actual and perceived), adolescent-maternal relationship satisfaction, and couple sexual behavior were drawn from other national surveys or from scales with well documented psychometric properties. Results demonstrated that romantic relationships are part of most adolescents’ lives and that adolescents’ experiences with these relationships differ markedly by age, sex, and race/ethnicity. Further, each respective couple member’s pubertal development, perceived pubertal timing, and maternal relationship satisfaction were useful in predicting sexual risk-promoting and risk-reducing behaviors in adolescent romantic couples. Findings in this dissertation represent an initial step toward evaluating explanatory models of adolescent couple sexual behavior.

Chlorine Contribution to Quantitative Structure and Activity Relationship Models of Disinfection By-Products' Quantum Chemical Descriptors and Toxicities

Quantitative Structure-Activity Relationship (QSAR) has been applied extensively in predicting toxicity of Disinfection By-Products (DBPs) in drinking water. Among many toxicological properties, acute and chronic toxicities of DBPs have been widely used in health risk assessment of DBPs. These toxicities are correlated with molecular properties, which are usually correlated with molecular descriptors. The primary goals of this thesis are: 1) to investigate the effects of molecular descriptors (e.g., chlorine number) on molecular properties such as energy of the lowest unoccupied molecular orbital (ELUMO) via QSAR modelling and analysis; 2) to validate the models by using internal and external cross-validation techniques; 3) to quantify the model uncertainties through Taylor and Monte Carlo Simulation. One of the very important ways to predict molecular properties such as ELUMO is using QSAR analysis. In this study, number of chlorine (NCl) and number of carbon (NC) as well as energy of the highest occupied molecular orbital (EHOMO) are used as molecular descriptors. There are typically three approaches used in QSAR model development: 1) Linear or Multi-linear Regression (MLR); 2) Partial Least Squares (PLS); and 3) Principle Component Regression (PCR). In QSAR analysis, a very critical step is model validation after QSAR models are established and before applying them to toxicity prediction. The DBPs to be studied include five chemical classes: chlorinated alkanes, alkenes, and aromatics. In addition, validated QSARs are developed to describe the toxicity of selected groups (i.e., chloro-alkane and aromatic compounds with a nitro- or cyano group) of DBP chemicals to three types of organisms (e.g., Fish, T. pyriformis, and P.pyosphoreum) based on experimental toxicity data from the literature. The results show that: 1) QSAR models to predict molecular property built by MLR, PLS or PCR can be used either to select valid data points or to eliminate outliers; 2) The Leave-One-Out Cross-Validation procedure by itself is not enough to give a reliable representation of the predictive ability of the QSAR models, however, Leave-Many-Out/K-fold cross-validation and external validation can be applied together to achieve more reliable results; 3) ELUMO are shown to correlate highly with the NCl for several classes of DBPs; and 4) According to uncertainty analysis using Taylor method, the uncertainty of QSAR models is contributed mostly from NCl for all DBP classes.

Development and Verification of Control and Protection Strategies in Hybrid AC/DC Power Systems for Smart Grid Applications

Modern power networks incorporate communications and information technology infrastructure into the electrical power system to create a smart grid in terms of control and operation. The smart grid enables real-time communication and control between consumers and utility companies allowing suppliers to optimize energy usage based on price preference and system technical issues. The smart grid design aims to provide overall power system monitoring, create protection and control strategies to maintain system performance, stability and security. This dissertation contributed to the development of a unique and novel smart grid test-bed laboratory with integrated monitoring, protection and control systems. This test-bed was used as a platform to test the smart grid operational ideas developed here. The implementation of this system in the real-time software creates an environment for studying, implementing and verifying novel control and protection schemes developed in this dissertation. Phasor measurement techniques were developed using the available Data Acquisition (DAQ) devices in order to monitor all points in the power system in real time. This provides a practical view of system parameter changes, system abnormal conditions and its stability and security information system. These developments provide valuable measurements for technical power system operators in the energy control centers. Phasor Measurement technology is an excellent solution for improving system planning, operation and energy trading in addition to enabling advanced applications in Wide Area Monitoring, Protection and Control (WAMPAC). Moreover, a virtual protection system was developed and implemented in the smart grid laboratory with integrated functionality for wide area applications. Experiments and procedures were developed in the system in order to detect the system abnormal conditions and apply proper remedies to heal the system. A design for DC microgrid was developed to integrate it to the AC system with appropriate control capability. This system represents realistic hybrid AC/DC microgrids connectivity to the AC side to study the use of such architecture in system operation to help remedy system abnormal conditions. In addition, this dissertation explored the challenges and feasibility of the implementation of real-time system analysis features in order to monitor the system security and stability measures. These indices are measured experimentally during the operation of the developed hybrid AC/DC microgrids. Furthermore, a real-time optimal power flow system was implemented to optimally manage the power sharing between AC generators and DC side resources. A study relating to real-time energy management algorithm in hybrid microgrids was performed to evaluate the effects of using energy storage resources and their use in mitigating heavy load impacts on system stability and operational security.