A framework for transforming, analyzing, and realizing software designs in unified modeling language

Unified Modeling Language (UML) is the most comprehensive and widely accepted object-oriented modeling language due to its multi-paradigm modeling capabilities and easy to use graphical notations, with strong international organizational support and industrial production quality tool support. However, there is a lack of precise definition of the semantics of individual UML notations as well as the relationships among multiple UML models, which often introduces incomplete and inconsistent problems for software designs in UML, especially for complex systems. Furthermore, there is a lack of methodologies to ensure a correct implementation from a given UML design. The purpose of this investigation is to verify and validate software designs in UML, and to provide dependability assurance for the realization of a UML design.^ In my research, an approach is proposed to transform UML diagrams into a semantic domain, which is a formal component-based framework. The framework I proposed consists of components and interactions through message passing, which are modeled by two-layer algebraic high-level nets and transformation rules respectively. In the transformation approach, class diagrams, state machine diagrams and activity diagrams are transformed into component models, and transformation rules are extracted from interaction diagrams. By applying transformation rules to component models, a (sub)system model of one or more scenarios can be constructed. Various techniques such as model checking, Petri net analysis techniques can be adopted to check if UML designs are complete or consistent. A new component called property parser was developed and merged into the tool SAM Parser, which realize (sub)system models automatically. The property parser generates and weaves runtime monitoring code into system implementations automatically for dependability assurance. The framework in the investigation is creative and flexible since it not only can be explored to verify and validate UML designs, but also provides an approach to build models for various scenarios. As a result of my research, several kinds of previous ignored behavioral inconsistencies can be detected.^

The use of computer graphic organizers for narrative writing by elementary school students with Specific Learning Disabilities

Writing is an academic skill critical to students in today's schools as it serves as a predominant means for demonstrating knowledge during school years (Graham, 2008). However, for many students with Specific Learning Disabilities (SLD), learning to write is a challenging, complex process (Lane, Graham, Harris, & Weisenbach, 2006). Students SLD have substantial writing challenges related to the nature of their disability (Mayes & Calhoun, 2005). ^ This study investigated the effects of computer graphic organizer software on the narrative writing compositions of four, fourth- and fifth-grade, elementary-level boys with SLD. A multiple baseline design across subjects was used to explore the effects of the computer graphic organizer software on four dependent variables: total number of words, total planning time, number of common story elements, and overall organization. ^ Prior to baseline, participants were taught the fundamentals of narrative writing. Throughout baseline and intervention, participants were read a narrative writing prompt and were allowed up to 10 minutes to plan their writing, followed by 15 minutes for writing, and 5 minutes of editing. During baseline, all planning was done using paper and pencil. During intervention, planning was done on the computer using a graphic organizer developed from the software program Kidspiration 3.0 (2011). All compositions were written and editing was done using paper and pencil during baseline and intervention. ^ The results of this study indicated that to varying degrees computer graphic organizers had a positive effect on the narrative writing abilities of elementary aged students with SLD. Participants wrote more words (from 54.74 to 96.60 more), planned for longer periods of time (from 4.50 to 9.50 more minutes), and included more story elements in their compositions (from 2.00 to 5.10 more out of a possible 6). There were nominal to no improvements in overall organization across the 4 participants. ^ The results suggest that teachers of students with SLD should considering use computer graphic organizers in their narrative writing instruction, perhaps in conjunction with remedial writing strategies. Future investigations can include other types of writing genres, other stages of writing, participants with varied demographics and their use combined with remedial writing instruction. ^

A software tool that generates symbolic model verifier (SMV) input language from a predicate transition net

The purpose of this research was to apply model checking by using a symbolic model checker on Predicate Transition Nets (PrT Nets). A PrT Net is a formal model of information flow which allows system properties to be modeled and analyzed. The aim of this thesis was to use the modeling and analysis power of PrT nets to provide a mechanism for the system model to be verified. Symbolic Model Verifier (SMV) was the model checker chosen in this thesis, and in order to verify the PrT net model of a system, it was translated to SMV input language. A software tool was implemented which translates the PrT Net into SMV language, hence enabling the process of model checking. The system includes two parts: the PrT net editor where the representation of a system can be edited, and the translator which converts the PrT net into an SMV program.

Network Construction and Graph Theoretical Analysis of Functional Language Networks in Pediatric Epilepsy

This dissertation introduces a new approach for assessing the effects of pediatric epilepsy on the language connectome. Two novel data-driven network construction approaches are presented. These methods rely on connecting different brain regions using either extent or intensity of language related activations as identified by independent component analysis of fMRI data. An auditory description decision task (ADDT) paradigm was used to activate the language network for 29 patients and 30 controls recruited from three major pediatric hospitals. Empirical evaluations illustrated that pediatric epilepsy can cause, or is associated with, a network efficiency reduction. Patients showed a propensity to inefficiently employ the whole brain network to perform the ADDT language task; on the contrary, controls seemed to efficiently use smaller segregated network components to achieve the same task. To explain the causes of the decreased efficiency, graph theoretical analysis was carried out. The analysis revealed no substantial global network feature differences between the patient and control groups. It also showed that for both subject groups the language network exhibited small-world characteristics; however, the patient’s extent of activation network showed a tendency towards more random networks. It was also shown that the intensity of activation network displayed ipsilateral hub reorganization on the local level. The left hemispheric hubs displayed greater centrality values for patients, whereas the right hemispheric hubs displayed greater centrality values for controls. This hub hemispheric disparity was not correlated with a right atypical language laterality found in six patients. Finally it was shown that a multi-level unsupervised clustering scheme based on self-organizing maps, a type of artificial neural network, and k-means was able to fairly and blindly separate the subjects into their respective patient or control groups. The clustering was initiated using the local nodal centrality measurements only. Compared to the extent of activation network, the intensity of activation network clustering demonstrated better precision. This outcome supports the assertion that the local centrality differences presented by the intensity of activation network can be associated with focal epilepsy.