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. ^

Multiple predator effects and native prey responses to two non-native Everglades cichlids

Non-native predators may have negative impacts on native communities, and these effects may be dependent on interactions among multiple non-native predators. Sequential invasions by predators can enhance risk for native prey. Prey have a limited ability to respond to multiple threats since appropriate responses may conflict, and interactions with recent invaders may be novel. We examined predator–prey interactions among two non-native predators, a recent invader, the African jewelfish, and the longer-established Mayan cichlid, and a native Florida Everglades prey assemblage. Using field enclosures and laboratory aquaria, we compared predatory effects and antipredator responses across five prey taxa. Total predation rates were higher for Mayan cichlids, which also targeted more prey types. The cichlid invaders had similar microhabitat use, but varied in foraging styles, with African jewelfish being more active. The three prey species that experienced predation were those that overlapped in habitat use with predators. Flagfish were consumed by both predators, while riverine grass shrimp and bluefin killifish were eaten only by Mayan cichlids. In mixed predator treatments, we saw no evidence of emergent effects, since interactions between the two cichlid predators were low. Prey responded to predator threats by altering activity but not vertical distribution. Results suggest that prey vulnerability is affected by activity and habitat domain overlap with predators and may be lower to newly invading predators, perhaps due to novelty in the interaction.

Functional near infrared spectroscopy study of language, joint attention and motor skills

Near infrared spectroscopy (NIRS) is an emerging non-invasive optical neuro imaging technique that monitors the hemodynamic response to brain activation with ms-scale temporal resolution and sub-cm spatial resolution. The overall goal of my dissertation was to develop and apply NIRS towards investigation of neurological response to language, joint attention and planning and execution of motor skills in healthy adults. Language studies were performed to investigate the hemodynamic response, synchrony and dominance feature of the frontal and fronto-temporal cortex of healthy adults in response to language reception and expression. The mathematical model developed based on granger causality explicated the directional flow of information during the processing of language stimuli by the fronto-temporal cortex. Joint attention and planning/ execution of motor skill studies were performed to investigate the hemodynamic response, synchrony and dominance feature of the frontal cortex of healthy adults and in children (5-8 years old) with autism (for joint attention studies) and individuals with cerebral palsy (for planning/execution of motor skills studies). The joint attention studies on healthy adults showed differences in activation as well as intensity and phase dependent connectivity in the frontal cortex during joint attention in comparison to rest. The joint attention studies on typically developing children showed differences in frontal cortical activation in comparison to that in children with autism. The planning and execution of motor skills studies on healthy adults and individuals with cerebral palsy (CP) showed difference in the frontal cortical dominance, that is, bilateral and ipsilateral dominance, respectively. The planning and execution of motor skills studies also demonstrated the plastic and learning behavior of brain wherein correlation was found between the relative change in total hemoglobin in the frontal cortex and the kinematics of the activity performed by the participants. Thus, during my dissertation the NIRS neuroimaging technique was successfully implemented to investigate the neurological response of language, joint attention and planning and execution of motor skills in healthy adults as well as preliminarily on children with autism and individuals with cerebral palsy. These NIRS studies have long-term potential for the design of early stage interventions in children with autism and customized rehabilitation in individuals with cerebral palsy.

Intracranial Volume Estimation and Graph Theoretical Analysis of Brain Functional Connectivity Networks

Understanding pathways of neurological disorders requires extensive research on both functional and structural characteristics of the brain. This dissertation introduced two interrelated research endeavors, describing (1) a novel integrated approach for constructing functional connectivity networks (FCNs) of brain using non-invasive scalp EEG recordings; and (2) a decision aid for estimating intracranial volume (ICV). The approach in (1) was developed to study the alterations of networks in patients with pediatric epilepsy. Results demonstrated the existence of statistically significant (p

Evoking non-repertory verbal behavior across operant classes : the effects of motor echoic sign language training within the context of a motivating operation

The individual effects that echoic, mand, and sign language training procedures have on the acquisition of verbal behavior have been widely demonstrated, but more efficient strategies are still needed. This study combined all three treatment strategies into one treatment intervention in order to investigate the joint effects they may have on verbal behavior. Six participants took part in the study. Intervention totaled 1 hour/day for 5 days/week until mastery criterion for motor echoic behavior was achieved. Although motor echoic behavior were solely targeted for acquisition, significant increases in spontaneous motor mands were noted in all treatment participants. Additionally, 4 treatment participants also demonstrated significant gains in vocal echoics and spontaneous vocal mands. No significant increases were noted for the control participant. Results suggest that the aforementioned procedure may provide more efficient results as a first-step to teaching a functional repertoire of verbal behavior to developmentally delayed children.

Design for placement of modified optodes to non-invasively map cerebral function

By using near infrared spectroscopy (NIRS) and by modifying the current Somanetics® optodes being used with the INVOS oximeter, the modified optodes are made to be fairly functional not only across the forehead, but across the hairy regions of the scalp as well. A major problem arises in the positioning of these optodes on the patients scalp and holding them in place while recording data. Another problem arises in the inconsistent repeatability of the trends displayed in the recorded data. A method was developed to facilitate the easy placement of these optodes on the patients scalp keeping in mind thepatient's comfort. The sensitivity of the optodes, too, was improved by incorporating better refined techniques for manufacturing the fiber optic brushes and fixing the same to the optode transmitting and receiving windows. The modified and improved optodes, in the single as well as in the multiplexed modes, were subjected to various tests on different areas of the brain to determine their efficiency and functionality.