Mecanismos formais e informais de regulação na decisão de cooperação : um estudo sobre seus efeitos em dilemas sociais

Ao longo dos anos, campos de estudos como os de ciência política, organizações e economia vêm se debruçando sobre a questão do papel de mecanismos regulativos no comportamento decisório do indivíduo. A partir de óticas e abordagens diferentes, cada um desses campos vem estudando o impacto de instrumentos de regulação na conformação dos atores para determinada orientação de ação. Dos instrumentos mais citados na literatura para regular a ação do ator, podemos apontar os mecanismos formais e informais de regulação. Um intenso debate entre os trabalhos dedicados ao assunto vem sendo travado, discutindo a eficiência de cada um deles na conformação do ator. Dada a relevância desse debate, o presente trabalho teve como objetivo comparar a efetividade de mecanismos formais e informais de regulação na decisão de cooperação do indivíduo em dilemas sociais, que são situações onde cada indivíduo ao buscar seu interesse próprio, leva a coletividade a resultados piores do que aqueles que seriam atingidos, caso houvesse cooperação do grupo. Para alcançarmos o objetivo do trabalho, realizou-se um experimento com alunos da graduação da EAESP-FGV para testar em ambiente laboratorial o comportamento dos agentes sob a pressão dos dois mecanismos de regulação. Os resultados do experimento mostraram que mecanismos informais de regulação têm maior influência na decisão de cooperação do ator, assim como sua presença diminui a necessidade do uso de um mecanismo formal de regulação para assegurar a cooperação dos membros de um grupo.

A decisão intuitiva nas organizações formais contemporaneas : uma analise de suas possibilidades

Jà há algum tempo o ocidente se vê questionado nos fundamentos que estruturam o saber e, consequentemente. o universo das ciências . ... A chamada razão. até então o pardigma absoluto. vem sendo contraposta a intuição como forma igualmente válida de alicerçar a ação humana na busca do conhecimento verdadeiro. Na Administração, tanto quanto em outros campos do conhecimento. a intuição vem sendo abordada por diversos estudiosos das organizações no seu ponto mais nevrálgico: a decisão gerencial. O presente trabalho discute esta questão a partir de uma análise crítica dos modelos racionais de decisão preconizados. estes fundamentados sobre uma compreensão funcionalista de organização e intenciona acrescentar às discussões já existentes a noção de intuição como método de pensamento do humano, portanto tão lógico quanto a dedução. Para tal, este estudo se vale de alguns referenciais postos por pensadores mais contemporâneos, destacando a Fenomenologia de Edmund Husserl. São abordados ainda estruturadas na direção fundamento da ação humana, à compreensão husserliana algumas configurações organizacionais da validação da intuição também como mesmo que nao necessariamente atreladas de intuição. O trabalho ainda defende a noção de supra-realidade, noção esta que traduz a síntese das diversas lógicas e não a mera agregação delas. Procura, assim. abrir espaço para reflexões na direção da necessidade da construção de novos arranjos organizacionais que reflitam essa síntese.

Representações sociais de velhice em contexto de prestação formal de cuidados

Universidade da Madeira. Centro de Ciência e Tecnologia da Madeira

Limites formais e materiais ao controle de constitucionalidade pelo Supremo Tribunal Federal

This document approaches the formal and material limits of the constitucionalidade control for the Supreme Federal Court, iniating with the study of the Constitution, detaching its evolution, nature and meanings, passing for its historical evolution, offering still a unconstitutionality concept. Is work the principles as material Constitution, making the distinction entere principles and rules, detaching the characteristics of the principles constitutional, and the basic principle of the Constituition. It analyzes metodologics the historical parameters and of the brazilian system of constitutionality control and detaches the paper of the Supreme Federal Court as positive legislator. It observes the beddings of the constitutionality control and the legitimacy of the Supreme Federal Court. Is examines the performance of the Supreme Federal Court in face of the principle of the legal security. Is offers a vision on the experience of the control of constitutionality in other constries. It still approaches the control of constitutionality in Brazil, detaching the critical points of its formal and material limits. Is verifies the application of the principles constitutional for the Supreme Federal Court in the diffuse control and the intent control of constitutionality, as well as the performance of the Supreme Federal Court ahead of the unconstitutional omissions. It brings to the debate the new perspectives how much to the formal and material limits of the control of constitutionality for the Supreme Federal Court. Objective to elaborate considerations concerning the limits of the constitutional jurisdiction from the model of Constituition, the character politican of the difficulties with respect to the definition of its formal and material limits from the performance of the Supreme Federal Court

A evolução do emprego formal industrial nas cidades médias do estado do Ceará (Juazeiro do Norte, Crato e Sobral) no período de 1990 a 2010

The work consists in a discussion of the evolution of formal employment in the industrial cities of Ceará state averages from 1990 to 2010, since this period was marked by important changes. It is emphasized that in order to achieve this aim, the present study was based on a survey of relevant literature on the subject, as well as the use of the Annual Report of Social Information (RAIS), published by the Ministry of Labour and Employment (MTE) and the Brazilian Institute of Geography and Statistics (IBGE). The central question to be considered in this study is how we evolved formal employment industry in medium-sized cities (Juazeiro do Norte, Crato and Sobral) of Ceará? The assumption that guides this work is that given the economic policies of the 1990 and 2000 these policies encouraged the relocation, thus implying significant growth in the formal manufacturing employment in these cities. Regarding the results obtained in the survey, it was found that the industrial sector of these cities, showed considerable dynamism in what refers to the expansion of establishments. When observed in percentage terms medium-sized cities (345.5%) had the highest growth in number of establishments in the 1990s with rates higher than the Northeast region (285.9%) and Brazil (167.5%). The highlight was the city of Juazeiro, with the highest concentration of micro and small footwear companies in the state. Regarding the number of formal jobs created in medium-sized cities, it went from 6.596 in 1990 to 41.660 million formal jobs in 2010, with a growth rate of 532%. The sector contributed most to employment generation was the footwear. Although the levels of minimum wages, the 1990 recorded the lowest levels. In the 2000, there were real gains in levels of minimum wages in all cities, however, it may be noted that over the decades there has been significant momentum. However, this momentum was not enough to prevent the end of the study period CMs-Ceará present low wages

Industrialização e emprego formal: uma análise para os municípios da região metropolitana do Cariri nos anos de 1990 e 2000

The Northeast has a record of fighting to reduce disparities. In late 1950, the state intervened through SUDENE, organizing and planning the promotion of development through industrialization. This study aims to identify the characteristics of the industrialization of the Northeast and evolution of formal employment in the metropolitan area of Cariri, located in the southern state of Ceará, in the case of the municipalities of Crato, Juazeiro do Norte and Barbalha (CRAJUBAR) in decades of 1990 and 2000. The assumption permeates the SUDENE with public policies to encourage the industry, causing profound changes in the cities studied. The results indicate that the Cariri since the 1960 has been benefiting the programs implemented by SUDENE. With the implementation of these programs, with in a set of circumstances based on local vocations and state policies, there was a spatial distribution industry, triggering a growth and development on the provision of formal jobs in the industrial sector

A utilização de espaços de educação não formal por professores de biologia de Natal-RN

La práctica educativa en espacios no formales es un recurso didáctico catalizador de motivación e interese, tanto para alumnos como para los profesores. El crecimiento de los espacios no formales coincide con los cambios recientes en el mundo en los campos sociales, políticos, económicos y culturales. Como una de las consecuencias de esos cambios, tenemos el crecimiento de otras instancias difusoras de conocimientos rompiendo, así, la hegemonía de la escuela. De esa forma, en este trabajo busqué investigar la frecuencia y las formas de utilización de los espacios de educación no formal por profesores de biología, de la enseñanza media, de la Ciudad de Natal (RN). Procuré también, identificar cuales son los espacios de educación no-formal que son utilizados; describir los recursos y las acciones desarrolladas en eses espacios; identificar la existencia o no de interese y la importancia que atribuyen a los espacios para la enseñanza de biología, además de divulgar los espacios utilizados como recursos didácticos. Para alcanzar estos objetivos fueron hechas observaciones de los espacios, aplicados cuestionarios y realizadas entrevistas con los profesores que realizan actividades junto a tales instituciones. Para el análisis de los datos se utilizó tanto el abordaje cuantitativo como cualitativa. Nos basamos en referenciales teóricos de autores que buscan establecer las relaciones entre diferentes modalidades de educación para mejor comprender lo que es la educación no-formal y su trayectoria histórica. Constaté que los profesores utilizan los espacios de educación no-formales, aun la cantidad de visitas al año sea reducida, en virtud de varias dificultades por ellos apuntadas, tales como el transporte, la falta de recursos financieros y de apoyo para viabilizar la visita, entre otros. Verifiqué también que los profesores demostraron un alto interese por los espacios no-formales y apuntaron como principales justificativas para considerarlos importantes para la enseñanza de la biología la posibilidad de establecer conexiones entre la teoría y la practica, además de la complementariedad

Saúde física e emocional de cuidadores da cidade de Santa Cruz-RN: perfil epidemiológico e fatores associados

Taking care for an impaired elderly is a hard and costly task that could affect directly the caregiver health. The purpose of this study was to evaluate the physical and mental health of elderly caregivers from the city of Santa Cruz-RN and analyze the potential correlated factors through an observational analytic design of a crosssectional. A multidimensional questionnaire was used to evaluation of the social demographics characteristics and those related to the care activity, as well as the caregivers´ physical and mental health. It was realized a descriptive analyze using frequency distribution and measures of the central tendency and dispersion to description of the caregivers. To verify the magnitude of the association between the variables was used the bivariate analysis through the Pearson and Spearman correlations and qui-square test. To evaluation of the association of the correlated factors to the adverse outcome with the caregivers´ physical and mental health was made a multivariate analysis by logistic binary regression and multiple linear regression models. The final sample was constituted by 304 persons, mostly women with a mean age of 50.3 ±16.8 years. The principal factors related to the physical health were age, stress and life satisfaction. Be a male caregiver, caring for a little while the elderly with cognitive deficit and not been spouse were related to worse mental health. Have worse physical health, high stress, depressive symptomatology, burden and low levels of satisfaction were also related to the mental health. After adjust through multiple linear regression was observed R2 values of R2=0,21 for Stress, R2 =0,17 for Depressive Symptomatology, R2 =0,21 for Burden and R2 =0,16 for Satisfaction. The attainment of the factors associated with caregiver´s health can help in the elaboration of specifics politics witch the goal is the integral attention to the elderly and his caregiver. The inability of continuous taking care could result in adverse outcomes such as institutionalization, impairment and death

Desenvolvimento formal de aplicações para smartcards

Smart card applications represent a growing market. Usually this kind of application manipulate and store critical information that requires some level of security, such as financial or confidential information. The quality and trustworthiness of smart card software can be improved through a rigorous development process that embraces formal techniques of software engineering. In this work we propose the BSmart method, a specialization of the B formal method dedicated to the development of smart card Java Card applications. The method describes how a Java Card application can be generated from a B refinement process of its formal abstract specification. The development is supported by a set of tools, which automates the generation of some required refinements and the translation to Java Card client (host) and server (applet) applications. With respect to verification, the method development process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of refinement, named implementation. This translation process was specified in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This specification was an important support during the translator development and contributes to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2, of Java/Java Card data types and machines that can be useful for the specifier, but are not part of the standard Java Card library. In other to validate the method, its tool support and the KitSmart, we developed an electronic passport application following the BSmart method. We believe that the results reached in this work contribute to Java Card development, allowing the generation of complete (client and server components), and less subject to errors, Java Card applications.

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

Joker: um realizador de desenhos animados para linguagens formais

Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However, there are many resistance in adopting this software development approach. The main reason is the scarcity of adequate, easy to use, and useful tools. Developers typically write code and test it. These tests usually consist of executing the program and checking its output against its requirements. This, however, is not always an exhaustive discipline. On the other side, using formal methods one might be able to investigate the system s properties further. Unfortunately, specification languages do not always have tools like animators or simulators, and sometimes there are no friendly Graphical User Interfaces. On the other hand, specification languages usually have a compiler which normally generates a Labeled Transition System (LTS). This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B, CSP, and Z. However, using a LTS in a specified XML format, it is possible to animate further languages. Additionally, the tool provides traces visualization, the choices the user did, in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it, as the developers do for programming languages, such as Java and C++.

Geração automática de hardware apartir de especificações formais: estendendo uma abordagem de tradução

A remoção de inconsistências em um projeto é menos custosa quando realizadas nas etapas iniciais da sua concepção. A utilização de Métodos Formais melhora a compreensão dos sistemas além de possuir diversas técnicas, como a especificação e verificação formal, para identificar essas inconsistências nas etapas iniciais de um projeto. Porém, a transformação de uma especificação formal para uma linguagem de programação é uma tarefa não trivial. Quando feita manualmente, é uma tarefa passível da inserção de erros. O uso de ferramentas que auxiliem esta etapa pode proporcionar grandes benefícios ao produto final a ser desenvolvido. Este trabalho propõe a extensão de uma ferramenta cujo foco é a tradução automática de especificações em CSPm para Handel-C. CSP é uma linguagem de descrição formal adequada para trabalhar com sistemas concorrentes. Handel-C é uma linguagem de programação cujo resultado pode ser compilado diretamente para FPGA's. A extensão consiste no aumento no número de operadores CSPm aceitos pela ferramenta, permitindo ao usuário definir processos locais, renomear canais e utilizar guarda booleana em escolhas externas. Além disto, propomos também a implementação de um protocolo de comunicação que elimina algumas restrições da composição paralela de processos na tradução para Handel-C, permitindo que a comunicação entre múltiplos processos possa ser mapeada de maneira consistente e que a mesma somente ocorra quando for autorizada.

Geração automática de hardware a partir de especificações formais: estendendo uma abordagem de tradução

Removing inconsistencies in a project is a less expensive activity when done in the early steps of design. The use of formal methods improves the understanding of systems. They have various techniques such as formal specification and verification to identify these problems in the initial stages of a project. However, the transformation from a formal specification into a programming language is a non-trivial task and error prone, specially when done manually. The aid of tools at this stage can bring great benefits to the final product to be developed. This paper proposes the extension of a tool whose focus is the automatic translation of specifications written in CSPM into Handel-C. CSP is a formal description language suitable for concurrent systems, and CSPM is the notation used in tools support. Handel-C is a programming language whose result can be compiled directly into FPGA s. Our extension increases the number of CSPM operators accepted by the tool, allowing the user to define local processes, to rename channels in a process and to use Boolean guards on external choices. In addition, we also propose the implementation of a communication protocol that eliminates some restrictions on parallel composition of processes in the translation into Handel-C, allowing communication in a same channel between multiple processes to be mapped in a consistent manner and that improper communication in a channel does not ocurr in the generated code, ie, communications that are not allowed in the system specification

Formal verification of PLC programs using the B Method

PLCs (acronym for Programmable Logic Controllers) perform control operations, receiving information from the environment, processing it and modifying this same environment according to the results produced. They are commonly used in industry in several applications, from mass transport to petroleum industry. As the complexity of these applications increase, and as various are safety critical, a necessity for ensuring that they are reliable arouses. Testing and simulation are the de-facto methods used in the industry to do so, but they can leave flaws undiscovered. Formal methods can provide more confidence in an application s safety, once they permit their mathematical verification. We make use of the B Method, which has been successfully applied in the formal verification of industrial systems, is supported by several tools and can handle decomposition, refinement, and verification of correctness according to the specification. The method we developed and present in this work automatically generates B models from PLC programs and verify them in terms of safety constraints, manually derived from the system requirements. The scope of our method is the PLC programming languages presented in the IEC 61131-3 standard, although we are also able to verify programs not fully compliant with the standard. Our approach aims to ease the integration of formal methods in the industry through the abbreviation of the effort to perform formal verification in PLCs