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.

Imunidade recíproca e livre concorrência: considerações acerca de sua fruição por empresas estatais

This study begins with a brief overview of tax immu nities in general, dealing with the concept, legal, doctrinal ratings and limits. Then enters into the reciprocal immunity, since its birth in the United States, its justifica tions, until her current developments in the Brazilian Supreme Court, which has expanded it quite considerably. That Court has extended to state owned enterprises, even if pa id by public prices or rates, or if acts somewhat away from its essential functions, es pecially if they are public services provider. Given this linkage, these are also treate d in own topic, grounded in newer doctrinal proposals and less attached to historical formalisms (see such Supremacy of Public Interest over Private one). Public services are approached in its diversity, oblivious to traditional monolithic nature and accu stomed to the modern doctrine of fundamental human rights. It deals also the princip les of free enterprise and free competition, given that the public service provider s have lived intensely in this environment, be they public or private agents. In d ialectical topic, these institutes are placed in joint discussion, all in an attempt to in vestigate their interactions and propose criteria less generic and removed from real ity, to assess the legitimacy of the mutual enjoyment of immunity by certain agents. Sev eral cases of the Court are analyzed individually, checking in each one the app lication of the proposed criteria, such logical-deductive activity and theory of pract ice approach. At the end, the conclusions refer to a reciprocal immunity less rhe torical and ideological and more pragmatic and consequentialist. It is proposed the end to the general rules or abstract formulas of subsumption, with concerns on the one h and the actual maintenance of the federal pact, and on the other by a solid econo mic order without inapt advantages to certain players, which flatly contradicts the co nstitutional premises.

A interpretação constitucional dos princípios da afetividade e solidariedade familiar pelos tribunais superiores brasileiros

The Brazilian juridical ordain has suffered several transformations on Family Law as of the 1988 Federal Constitution, which incorporated the changes in socio-cultural values and behaviors that appeared in the post-modern Brazilian society, with the repersonalization of the family, beginning with the principles of human dignity, affectivity and familiar solidarity; occurring an enlargement of the concept of family, increasing the relevance of socioaffectivity and eudaimonia. The general purpose of this dissertation is to analyze the constitutional interpretations of paradigmatic cases of the Brazilian Superior Courts checking the conditions and behaviors required to achieve the principles of affectivity and familiar solidarity. To do so, uses an exploratory and descriptive research trough books, scientific papers, jurisprudence, monographs and consult to specialized magazines to identify the reasons and specific purposes of the principles of affectivity and family solidarity within the constitutional norms, systematizing the primary meaning of these principles, then to observe the trial of patriotic courts, the criteria and standards of behavior used in their application. The analysis of recent decisions of the Supreme Federal Court and the Superior Court of Justice on the topic of the familiar relations, utilizing the new interpretative approach to the law that considers man as an ontological being of language, demonstrate that the affectivity and familiar solidarity are constitutional principles concretized in decisions, that don’t affect the principle of protection of the juridical security, that is, don’t cause uncertainty despite the incipient specification of criteria to its use

Conselho estadual de meio ambiente do Rio Grande do Norte: paradigmas, proposições e atores sociais

The environmental movement rises up strongly in the year 1972 with the Stocolmus Conference, in the middle of pressions concerning the environmental preservation, in consequence of the environmental catastrophes. In spite of the fact that, in Brazil, the environmental movement has is institutionalization with the 1988 Constitution, in a way that the councils became democratic spaces, and provided the society’s participation in the management of public policies. In this way, we propose a discussion about the participation and the exercise of the citizenship in the State Council of Environment of Rio Grande do Norte (CONEMA), focusing the glance about the decisory process, as from the expression of the social actors. For that, our research compilate documents of the meetings of the referring council, transcribing the main discussions about the environmental necessities which were important in the potiguar society, and checking how these agents defend their interest during the meetings. We understand, with these informations, the role of CONEMA/RN as a communicative mechanism between State and Society. With the analysis of the informations of the extraordinary meetings from 2007 to 2014, we concluded that the CONEMA is a council where the civil organized society takes part on the decisory process, despite the great influence of the representative actors of public power over the representative actors of civil society. The results of this research confirm the discrepancy between the participation of representative councilors of civil society in CONEMA/RN. The conclusion point out that the civil society representative don’t, yet, assimilate the citizen duty, the responsibility of it1s action, producing, in this way, damages for the legal structure of the potiguar environmental legislation, with serious consequences on the public policy implementation

Aplicação de tecnologias eletroquímicas (oxidação via radicais hidroxila, oxidação mediada via cloro ativo e eletrocoagulação) para o tratamento de efluentes reais ou sintéticos

In this work the degradation of real and synthetic wastewater was studied using electrochemical processes such as oxidation via hydroxyl radicals, mediated oxidation via active chlorine and electrocoagulation. The real effluent used was collected in the decanter tank of the Federal University of Rio Grande do Norte (ETE-UFRN) of Effluent Treatment Plant and the other a textile effluent dye Ácido Blue 113 (AB 113) was synthesized in the laboratory. In the electrochemical process, the effects of anode material, current density, the presence and concentration of chloride as well as the active chlorine species on site generated were evaluated. Electrodes of different compositions, Ti/Pt, Ti/Ru0,3Ti0,7O2, BDD, Pb/PbO2 and Ti/TiO2-nanotubes/PbO2 were used as anodes. These electrodes were subjected to electroanalytical analysis with the goal of checking how happen the anodic and cathodic processes across the concentrations of NaCl and supporting electrolyte used. The potential of oxygen evolution reaction were also checked. The effect of active chlorine species formed under the process efficiency was evaluated by removing the organic matter in the effluent-ETE UFRN. The wastewater treatment ETE-UFRN using Ti/Pt, DDB and Ti/Ru0,3Ti0,7O2 electrodes was evaluated, obtaining good performances. The electrochemical degradation of effluent-UFRN was able to promote the reduction of the concentration of TOC and COD in all tested anodes. However, Ti/Ru0,3Ti0,7O2 showed a considerable degradation due to active chlorine species generated on site. The results obtained from the electrochemical process in the presence of chloride were more satisfactory than those obtained in the absence. The addition of 0.021 M NaCl resulted in a faster removal of organic matter. Secondly, was prepared and characterized the electrode Ti/TiO2-nanotubes/PbO2 according to what the literature reports, however their preparation was to disk (10 cm diameter) with surface area and higher than that described by the same authors, aiming at application to textile effluent AB 113 dye. SEM images were taken to observe the growth of TiO2 nanotubes and confirm the electrodeposition of PbO2. Atomic Force Microscope was also used to confirm the formation of these nanotubes. Furthermore, was tested and found a high electrochemical stability of the electrode Ti/TiO2-nanotubes/PbO2 for applications such as long-term indicating a good electrocatalytic material. The electrochemical oxidation of AB 113 using Ti/Pt, Pb/PbO2 and Ti/TiO2-nanotubes/PbO2 and Al/Al (electrocoagulation) was also studied. However, the best color removal and COD decay were obtained when Ti/TiO2-nanotubes/PbO2 was used as the anode, removing up to 98% of color and 92,5% of COD decay. Analysis of GC/MS were performed in order to identify possible intermediates formed in the degradation of AB 113.

Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.

Aprendizagem musical na Orquestra Sinfônica da UFRN

Music and music education are present in the daily lives of people in different ways and in multiple contexts. In this study, we highlight the musical training in the orchestral context aiming to understand how learning music happens in the Symphony Orches tra of the Universidade Federal do Ri o Grande do Norte – OSUFRN. To achieve this goal, we identified all the activities, structure and functioning in OSUFRN; we have observed the development of activities of the group by checking the interactions among the participants of the orchestra and the different ways to learn music in that orchestral context. The research is based on discussions about collective musical practice, instrumen tal training in music education, the process of learning and the relationship between young people and music in the context of collective musical practice learning. Qualitative approach and case study were used as methodological procedures. Data collection was established by means of on - site observations, accompanying of the activities, rehearsals and performances of group and semi - structured interviews with the conductor and some participants with more time in the orchestra. We have also used photographs a nd footage that helped us in the procedure collection and construction of data. The analysis and interpretation of these data were enforced by Content Analysis featuring. It reveals the musical learning, through learning instances perceived in rehearsals, concerts, in living with the conductor and between musicians, teachers, employees and guest musicians, individually in travel and exchanges with other orchestral groups. In this way the activities developed by the group enable a comprehensive musical educa tion that guides to acquire autonomy in their learning and preparing them for future careers.