Caring and being cared -for: Perceptions of adolescent males at -risk for school failure

This qualitative study used grounded theory methods and purposeful sampling to explore perceptions on caring and being cared-for. Twenty-four adolescent male participants, identified as at-risk for school failure, completed a two phase interview process exploring these phenomena within three relationships; the relationship with the friend, with the most caring person they knew and with the teacher they felt cared for them. ^ Each participant was asked a predetermined set of open questions in an initial semi-structured interview. In addition each participant was encouraged to explore his own reflections on caring. A second interview allowed for member checking and for the participant to continue sharing his meaning of caring and being cared-for. ^ Line by line analysis with open, axial and selective coding was applied to interview transcripts along with a constant comparative method. Results indicated that the core category integrating all other categories was attachment bonding. Participants' stories manifested characteristics of proximity seeking, secure base, safe haven and distress upon involuntary separation from an attachment figure. ^ Strategies facilitating attachment bonding were influenced by the power positions of the relational players. Participants responded positively to the one-caring when they felt cared-for. Results further indicated that participants did not need to feel a sense of belonging in order to feel cared-for. Teacher behaviors indicating openness for authentic connections with students were specific to teacher's friendliness and professional competence. Teachers who nurtured feelings of being cared-for were uncommon in the participants' educational experience. ^ The number of adolescent males leaving high school prematurely is both a personal problem and a social problem. Despite a “mask” of indifference often exhibited by adolescent males at-risk for school failure, teachers might consider the social/emotional needs of these students when implementing the curriculum. In addition, policy makers might consider the social/emotional needs of this vulnerable population when developing programs meant to foster psychological well-being and connectedness for adolescent males at-risk for school failure. ^

A deontic analysis of inter -organizational control requirements

This research focuses on the design and verification of inter-organizational controls. Instead of looking at a documentary procedure, which is the flow of documents and data among the parties, the research examines the underlying deontic purpose of the procedure, the so-called deontic process, and identifies control requirements to secure this purpose. The vision of the research is a formal theory for streamlining bureaucracy in business and government procedures. ^ Underpinning most inter-organizational procedures are deontic relations, which are about rights and obligations of the parties. When all parties trust each other, they are willing to fulfill their obligations and honor the counter parties’ rights; thus controls may not be needed. The challenge is in cases where trust may not be assumed. In these cases, the parties need to rely on explicit controls to reduce their exposure to the risk of opportunism. However, at present there is no analytic approach or technique to determine which controls are needed for a given contracting or governance situation. ^ The research proposes a formal method for deriving inter-organizational control requirements based on static analysis of deontic relations and dynamic analysis of deontic changes. The formal method will take a deontic process model of an inter-organizational transaction and certain domain knowledge as inputs to automatically generate control requirements that a documentary procedure needs to satisfy in order to limit fraud potentials. The deliverables of the research include a formal representation namely Deontic Petri Nets that combine multiple modal logics and Petri nets for modeling deontic processes, a set of control principles that represent an initial formal theory on the relationships between deontic processes and documentary procedures, and a working prototype that uses model checking technique to identify fraud potentials in a deontic process and generate control requirements to limit them. Fourteen scenarios of two well-known international payment procedures—cash in advance and documentary credit—have been used to test the prototype. The results showed that all control requirements stipulated in these procedures could be derived automatically.^

Methods for modeling and analyzing concurrent software

Concurrent software executes multiple threads or processes to achieve high performance. However, concurrency results in a huge number of different system behaviors that are difficult to test and verify. The aim of this dissertation is to develop new methods and tools for modeling and analyzing concurrent software systems at design and code levels. This dissertation consists of several related results. First, a formal model of Mondex, an electronic purse system, is built using Petri nets from user requirements, which is formally verified using model checking. Second, Petri nets models are automatically mined from the event traces generated from scientific workflows. Third, partial order models are automatically extracted from some instrumented concurrent program execution, and potential atomicity violation bugs are automatically verified based on the partial order models using model checking. Our formal specification and verification of Mondex have contributed to the world wide effort in developing a verified software repository. Our method to mine Petri net models automatically from provenance offers a new approach to build scientific workflows. Our dynamic prediction tool, named McPatom, can predict several known bugs in real world systems including one that evades several other existing tools. McPatom is efficient and scalable as it takes advantage of the nature of atomicity violations and considers only a pair of threads and accesses to a single shared variable at one time. However, predictive tools need to consider the tradeoffs between precision and coverage. Based on McPatom, this dissertation presents two methods for improving the coverage and precision of atomicity violation predictions: 1) a post-prediction analysis method to increase coverage while ensuring precision; 2) a follow-up replaying method to further increase coverage. Both methods are implemented in a completely automatic tool.

Formal modeling and analysis techniques for high level Petri nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. ^ There are two issues in using HLPNs—modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. ^ For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. ^ For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. ^ The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.^

An Assessment of the Performances of Several Univariate Tests of Normality

The importance of checking the normality assumption in most statistical procedures especially parametric tests cannot be over emphasized as the validity of the inferences drawn from such procedures usually depend on the validity of this assumption. Numerous methods have been proposed by different authors over the years, some popular and frequently used, others, not so much. This study addresses the performance of eighteen of the available tests for different sample sizes, significance levels, and for a number of symmetric and asymmetric distributions by conducting a Monte-Carlo simulation. The results showed that considerable power is not achieved for symmetric distributions when sample size is less than one hundred and for such distributions, the kurtosis test is most powerful provided the distribution is leptokurtic or platykurtic. The Shapiro-Wilk test remains the most powerful test for asymmetric distributions. We conclude that different tests are suitable under different characteristics of alternative distributions.

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.

A Deontic Analysis of Inter-Organizational Control Requirements

This research focuses on the design and verification of inter-organizational controls. Instead of looking at a documentary procedure, which is the flow of documents and data among the parties, the research examines the underlying deontic purpose of the procedure, the so-called deontic process, and identifies control requirements to secure this purpose. The vision of the research is a formal theory for streamlining bureaucracy in business and government procedures. Underpinning most inter-organizational procedures are deontic relations, which are about rights and obligations of the parties. When all parties trust each other, they are willing to fulfill their obligations and honor the counter parties’ rights; thus controls may not be needed. The challenge is in cases where trust may not be assumed. In these cases, the parties need to rely on explicit controls to reduce their exposure to the risk of opportunism. However, at present there is no analytic approach or technique to determine which controls are needed for a given contracting or governance situation. The research proposes a formal method for deriving inter-organizational control requirements based on static analysis of deontic relations and dynamic analysis of deontic changes. The formal method will take a deontic process model of an inter-organizational transaction and certain domain knowledge as inputs to automatically generate control requirements that a documentary procedure needs to satisfy in order to limit fraud potentials. The deliverables of the research include a formal representation namely Deontic Petri Nets that combine multiple modal logics and Petri nets for modeling deontic processes, a set of control principles that represent an initial formal theory on the relationships between deontic processes and documentary procedures, and a working prototype that uses model checking technique to identify fraud potentials in a deontic process and generate control requirements to limit them. Fourteen scenarios of two well-known international payment procedures -- cash in advance and documentary credit -- have been used to test the prototype. The results showed that all control requirements stipulated in these procedures could be derived automatically.

Students' recollections of participating in a first year residential learning community experience

The purpose of this qualitative study was to gain an understanding of what participation in a first year residential learning community meant to students 2-3 years after their involvement in the program. Various theories including environmental, student involvement, psychosocial and intellectual, were used as a framework for this case study. Each of the ten participants was a junior or senior level student at the time of the study, but had previously participated in a first year residential learning community at Florida International University. The researcher held two semi-structured interviews with each participant, and collected data sheets from each. The narrative data produced from the interviews were transcribed, coded and analyzed to gain insights into the experiences and perspectives of the participants. Member checking was used after the interview process. A peer reviewer offered feedback during the data analysis. The resulting data was coded into categories, with a final selection of four themes and 15 sub-themes, which captured the essence of the participants' experiences. The four major themes included: (a) community, (b) involvement, (c) identity, and (d) academics. The community theme is used to describe how students perceived the environment to be. The involvement theme is used to describe the students' participation in campus life and their interaction with other members of the university community. The identity theme is used to describe the students' process of development, and the personal growth they underwent as a result of their experiences. The academics theme refers to the intellectual development of students and their interaction around academic issues. The results of this study showed that the participants valued greatly their involvement in the First Year Residents Succeeding Together program (FYRST) and can articulate how it helped them succeed as students. In describing their experience, they most recall the sense of community that existed, the personal growth they experienced, the academic development process they went through, and their involvement, both with other people and with activities in their community. Recommendations are provided for practice and research, including several related to enhancing the academic culture, integrating faculty, utilizing peer influence and providing further opportunities to create a seamless learning environment.

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 Modeling and Analysis Techniques for High Level Petri Nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. There are two issues in using HLPNs - modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.

Perceptions of Underprepared Community College Students regarding their Educational Achievement

The purpose of this study was to understand the perceptions of underprepared college students who had participated in learning communities and who persisted to complete developmental classes and earned at least 30 college-level credit hours to graduate and the perceptions of their peers who had dropped out of college. The theories posed by Tinto, Astin, and Freire formed the framework for this case study. The 22 participants were graduates or transfer students now attending a public university, currently-enrolled sophomores, and students no longer enrolled at the time of the study. Semi-structured individual interviews and a group interview provided narrative data which were transcribed, coded, and analyzed to gain insights into the experiences and perspectives of the participants. The group interview provided a form of member checking to increase accuracy in interpreting themes. A peer reviewer provided feedback on the researcher’s data analysis procedures. The analysis yielded four themes and 14 sub-themes which captured the essence of the participants’ experiences. The pre-college characteristics/traits theme described the students’ internal values and attributes acquired prior to college. The external college support/community influence theme described the encouragement to attend college the students received from family, friends, and high school teachers. The social involvement theme described the students’ participation in campus activities and their interactions with other members of the campus. The academic integration theme described students’ use of campus resources and their contacts with the faculty. The persisters reported strong family and peer support, a sense of responsibility, appreciation for dedicated and caring faculty, and a belief that an education can be a liberatory means to achieve their goals. The non-persisters did not report having the same sense of purpose, goal orientation, determination, obligation to meet family expectations, peer support, campus involvement, positive faculty experiences, and time management skills. The researcher offers an emerging model for understanding factors associated with persistence and three recommendations for enhancing the academic experience of underprepared college students: (a) include a critical pedagogy perspective in coursework where possible, (b) integrate co-curricular activities with the academic disciplines, and (c) increase student-faculty interaction.