Seasonal fish community variation in headwater mangrove creeks in the southwestern Everglades: an examination of their role as dry-down refuges

The connectivity between the fish community of estuarine mangroves and that of freshwater habitats upstream remains poorly understood. In the Florida Everglades, mangrove-lined creeks link freshwater marshes to estuarine habitats downstream and may act as dry-season refuges for freshwater fishes. We examined seasonal dynamics in the fish community of ecotonal creeks in the southwestern region of Everglades National Park, specifically Rookery Branch and the North and watson rivers. Twelve low-order creeks were sampled via electrofishing, gill nets, and minnow traps during the wet season, transition period, and dry season in 2004-2005. Catches were greater in Rookery Branch than in the North and watson rivers, particularly during the transition period. Community composition varied seasonally in Rookery Branch, and to a greater extent for the larger species, reflecting a pulse of freshwater taxa into creeks as marshes upstream dried periodically. The pulse was short-lived, a later sample showed substantial decreases in freshwater fish numbers. No evidence of a similar influx was seen in the North and watson rivers, which drain shorter hydroperiod marshes and exhibit higher salinities. These results suggest that head-water creeks can serve as important dry-season refugia. Increased freshwater flow resulting from Everglades restoration may enhance this connectivity.

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.

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.

Evaluation of the use and management of fish resources in the pachitea river basin, Peruvian Amazon

The purpose of this study was to analyze the interrelations between the needs of local people and their usage and management of natural fisheries. Between June and August 2001, 177 households in the basin were interviewed regarding their fishing customs. The results were analyzed with parametric and nonparametric statistics considering a cultural and a geographic comparison. Results confirm that indigenous households rely more on fisheries as a resource than colonists. Fishing takes place throughout the year but is more common in the dry season. Fishing is commonly practiced using hooks and cast nets. More destructive techniques such as dynamite and "barbasco" (poisonous plant) were also used. Indigenous people use a greater array of techniques and they fish at a greater diversity of sites. Respondents also reported that fishing yields have decreased recently. Some of the most common fish genera captured are Pimelodus and Leporinus.

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.

3D navigation with six degrees-of-freedom using a multi-touch display

With the introduction of new input devices, such as multi-touch surface displays, the Nintendo WiiMote, the Microsoft Kinect, and the Leap Motion sensor, among others, the field of Human-Computer Interaction (HCI) finds itself at an important crossroads that requires solving new challenges. Given the amount of three-dimensional (3D) data available today, 3D navigation plays an important role in 3D User Interfaces (3DUI). This dissertation deals with multi-touch, 3D navigation, and how users can explore 3D virtual worlds using a multi-touch, non-stereo, desktop display. ^ The contributions of this dissertation include a feature-extraction algorithm for multi-touch displays (FETOUCH), a multi-touch and gyroscope interaction technique (GyroTouch), a theoretical model for multi-touch interaction using high-level Petri Nets (PeNTa), an algorithm to resolve ambiguities in the multi-touch gesture classification process (Yield), a proposed technique for navigational experiments (FaNS), a proposed gesture (Hold-and-Roll), and an experiment prototype for 3D navigation (3DNav). The verification experiment for 3DNav was conducted with 30 human-subjects of both genders. The experiment used the 3DNav prototype to present a pseudo-universe, where each user was required to find five objects using the multi-touch display and five objects using a game controller (GamePad). For the multi-touch display, 3DNav used a commercial library called GestureWorks in conjunction with Yield to resolve the ambiguity posed by the multiplicity of gestures reported by the initial classification. The experiment compared both devices. The task completion time with multi-touch was slightly shorter, but the difference was not statistically significant. The design of experiment also included an equation that determined the level of video game console expertise of the subjects, which was used to break down users into two groups: casual users and experienced users. The study found that experienced gamers performed significantly faster with the GamePad than casual users. When looking at the groups separately, casual gamers performed significantly better using the multi-touch display, compared to the GamePad. Additional results are found in this dissertation.^

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.

Parâmetros biológicos de Herpsilochmus pectoralis Sclater 1857 (Aves: Thamnophilidae) em fragmentos de mata atlântica do Nordeste do Brasil

The study of birds represents an important tool for the understanding of the processes involved in behavioral and morphological patterns. The species we have studied belongs to Thamnophilidae family, the third largest family restricted to the Neotropic ecozone. They are popularly known as antbirds and comprise 209 species. A large portion of the species has cryptic behavior, making the acoustic communication an important tool for maintaining contact among birds. Herpsilochmus pectoralis Sclater 1857 has evident sexual dimorphism, measured between 10 and 12 cm height and it is found in forest fragments in the Northeast and it is also categorized as vulnerable to extinction process. This study was conducted in three sandbank fragments on the east coast of the state of Rio Grande do Norte, Brazil. With the help of tape recordings between 2006 and 2012 it was possible to describe and characterize the sing of H. pectoralis. The sing from male birds has more and longer length than the female sing (16% of dimorphism). No differences were found in the dominant frequency between the sexes. We describe four types of calls from this species repertoire. Through capturing with ornithological nets between 2009 and 2012 it was possible to describe and compare the morphology of H. pectoralis. The species have shown lower corporal mass in the dry season. The young birds showed morphometric similarities in comparison to adults. The species has no accentuated dimorphism in their morphometric characteristics. The young ones with flying capabilities have morphometric characteristics of adults, even though they do not show a characteristic adult plumage. The moult pattern in the species is a characteristic of tropical birds, but it shows short reproductive period, typical of temperate species. Even being in the tropical region, the species suffers with seasonal rainfall, which influences their reproductive phenology and moult (remex and rectrix) cycle. Thus, this dissertation provides information on the biology of H. pectoralis to support the understanding of the relationship of this species to the environment and also to know the variations of morphology and vocal aspects, in order to understand patterns and general characteristics of Thamnophilidae.

Morfometria, variação anual no peso e demografia do Tico-tico-rei-cinza (Lanio pileatus: thraupidae) em dois ambientes de caatinga no nordeste do Brasil

The caatinga is considered the only exclusively Brazilian biome, with a total area of 735.000km². It is estimated that about 59% of this area has already been removed and only 2% are protected in conservations units. The region is characteristic by strong seasonality and heterogeneity in their environments. This paper sets generate information on morphological and population patterns Lanio pilatus in two areas of caatinga of Estação Ecológica do Seridó (ESEC – Seridó), Serra Negra do Norte - RN. Data collection was performed in six phases between July 2012 and December 2014, covering the end of the dry and rainy seasons in the region. The captures were performed with nets and individuals captured were marked with metal rings and measured (weight, wing length, tail, tarsus, culmen and tip of the bill to nostril). Through these measures, we observed that only males of open area range in weight during the dry and rainy season, youngs were significantly lower for all parameters measured, and males were larger than females in three characteristics (weight, wing length and tail) in open area and only one (wing length) in the closed area. The population parameters were generated from the mark-capture-recapture technique by program MARK, using the techniques of robust design and CJS. The survival probability of detection and population estimates varied with time. Only individuals of open area fluctuated in their estimates during the study. Overall, the environment was a great mediator of results which increases the need for more studies on the life history of the species in the region.

O cinema como educação do olhar

The knowledge is only possible due to we exist bodily. However, during the educational experience, the epistemic potency of the body is neglected, declining the registers of the intelligibility. The current thesis approaches that problem obliquely: from a body and image philosophy which has revealed other ways of doing those registers in the modernity – understood not as period itself, but as a qualification for the negotiations between the real and the intelligible. The referred ways are explored through Merleau- Ponty’s and Michel Foucault’s works, which offer a spectrum about that new negotiation of the real. In order to approach the studied problem, the visibility and the human body motricity in the cinema are taken as analysis object. The mentioned objects have been analyzed through a corpus of movies of which plots are centered at the formal education and they require from the characters and the spectators engagement into a visual performance. Aiming to approach the object, it is questioned how the Education phenomenon is represented by the cinema; how the body is exposed and how spectators can see it. Analyzing the corpus and articulating Merleau- Ponty’s and Michel Foucault’s theories, it has been possible to state the following thesis: the cinema as an education of the gaze. The general objective of this study is to reveal the educational potency of the filmic experience, which provides a new path of intelligibility for Education. In that sense, the body as a visual operator widens the capacity of understanding the real. The current work is divided in three chapters. The first one brings the methodological approach: it is pointed how the theoretical articulation is properly arranged; it explains the method of using the images as indirect language as part of the reality description; the filmic corpus is presented, as well the criteria for the films choices and for the construction of instrument adopted during the object analysis are described. In the second chapter, it is problematized the incapacity of the western society of formulating the real discursively by debating Merleau-Ponty’s and Foucault’s theoretical contributions about the visual performance displayed on the images while the films are watched and analyzed. In the third chapter, the implications of the education of the gaze provided by the cinema are developed, mainly concerning about the place attributed to the visibility during the formulation of the real. Finally, paths are designed for the construction of another approach for the visibility in Education. Assuming the gaze as an experience of knowledge, this study aims to present other ways of being, seeing, thinking and feeling the world. Therefore, it is a proposal to reset the epistemic and subjectification patterns at the educational context.

Os usos do território e a economia solidária no Rio Grande do Norte

The solidary economy as the organization of production, alternative to the capitalist economy provides new forms of organization and social behavior, that, in the sight of geography, it is shown by the different territory uses. The territory assume new meanings that, influenced by the Solidary Economy movement, tries to reach for new ways of acting that differ from social order already stablished. However, the different uses show themselves in a more complex and contradictory way, given that, in solidary undertakings, different corporative agents start to act, the State being a last resource on this process. Given this reality, our goal on the present paper is to analyze the different uses of the territory from the rural economic solidary undertakings and the relationship it establishes to the different agents involved on the socio-territorial dynamics on Rio Grande do Norte. Starting from a study that contemplates the territorial organization forms and contents of the analyzed phenomena, the methodology utilized for this research is based on a bibliographic review, with authors from the geography and areas related to the Solidary Economy, besides the use of secondary data, acquired from official offices such as SIES and IBGE, from the documented research, SENAES and field interviews conducted with local solidary undertakings. The results obtained in the study reveal the complexity of the agricultural use of the territory by Solidary Economy on the RN, while a resource of intensified use, from the state actions and important economical agents, and regulating the use while shelter, that marginalize solidary workers, making them subdued to the hegemonic logic. Therefore, we can infer that the solidary economy, despite its image of new form of organization between agricultural workers, given the expressivity of the rural solidary undertakings presented on RN, it hasn’t shown a full social development as an instrument of reproduction and emancipation of the associates. Nevertheless, the undertakings articulated in nets excel, even when considering its punctual and residual form. The given contradictions show that it is necessary to fortify the building of the solidary economy as being horizontal and popular based for it to have strength to surpass the regulative actions of the capitalist state and ownership created by the Capital.

Plasticidade dependente da experiência induzida por manipulação da matriz extracelular

The primary somatosensory cortex (S1) receives inputs from peripheral tactile receptors and plays a crucial role on many important behaviors. However, the plastic potential of this region is greatly reduced during adulthood, limiting functional recovery after injuries. This fact is due to the presence, in the brain parenchima, of structures and substances that have an inhibitory effect on plasticity, such as chondroitin sulfate proteoglicans (CSP) present in the perineuronal.nets (PNNs) surrounding a subset of neurons. Maturation of PNNs coincide with the closure of critical periods of plasticity in cortical areas, since CSP act to stabilize synaptic contacts. Removal of CSP is proven to be an effective therapeutic approach to restore plasticity and increase the odds of functional recovery after cortical lesion. In the present work, we removed CSP from the sensorimotor cortex of rats to restore plasticity and promote the compensatory morphofunctional regeneration of cortical circuits modified by removal of mystacial vibrissae during the critical period. Treatment with the CSP-digesting enzyme chondroitinase ABC proved efficient to restore plasticity in S1 circuits, as evidenced by morphological rearrangements and functional recovery.

Plasticidade dependente da experiência induzida por manipulação da matriz extracelular

The primary somatosensory cortex (S1) receives inputs from peripheral tactile receptors and plays a crucial role on many important behaviors. However, the plastic potential of this region is greatly reduced during adulthood, limiting functional recovery after injuries. This fact is due to the presence, in the brain parenchima, of structures and substances that have an inhibitory effect on plasticity, such as chondroitin sulfate proteoglicans (CSP) present in the perineuronal.nets (PNNs) surrounding a subset of neurons. Maturation of PNNs coincide with the closure of critical periods of plasticity in cortical areas, since CSP act to stabilize synaptic contacts. Removal of CSP is proven to be an effective therapeutic approach to restore plasticity and increase the odds of functional recovery after cortical lesion. In the present work, we removed CSP from the sensorimotor cortex of rats to restore plasticity and promote the compensatory morphofunctional regeneration of cortical circuits modified by removal of mystacial vibrissae during the critical period. Treatment with the CSP-digesting enzyme chondroitinase ABC proved efficient to restore plasticity in S1 circuits, as evidenced by morphological rearrangements and functional recovery.

Critical pegagogy in ELT: perspectives and praxis of western English teachers in Korean post-secondary education

Presently, there are numerous Native English Teacher (NETs) teaching in Korean post-secondary educational (PSE) institutions. The aim of this thesis is to explore the views held by NETs with regards to their self-perceived teaching perspectives while working in a Korean PSE setting. The thesis also aims to answer the assertion made in the literature that English as Foreign Language (EFL) teachers are "acritical and atheoretical". To this end, the thesis intends to identify the extent of the NETs’ preference for social reform as a teaching perspective, the NETs stated reasons for identifying with roles as social reformers, how these views are reflected in the NETs’ practice (praxis), what the barriers impeding the adoption and enactment of social reform are, and how the NETs’ perspectives relate to critical pedagogy. The results reveal that NETs in Korean PSE do not align themselves with social reform, yet categorizing NETS as "acritical and atheoretical" may be overly-simplistic. The results show that there are three kinds of obstacles that prevent NETs from engaging more with social reform and being less acritical and atheoretical: 1) NETs teaching in Korean EFL are conflicted and/or confused about their roles as English teachers; 2) there are significant cultural constraints to teaching in Korean EFL as a NET; 3) there are significant pedagogical constraints to teaching in Korean EFL as a NET.