Search

O tomateiro é uma das hortaliças mais importantes, no entanto o ataque de pragas, como o tripes, Frankliniella schultzei, pode causar prejuízos a essa cultura, principalmente por transmitir o complexo de vírus denominados de vira-cabeça do tomateiro. Contudo, os extratos de plantas podem ser uma alternativa no manejo de pragas. Assim, o objetivo foi avaliar o potencial inseticida de extratos hexânicos de fumo, alho e pimenta-roxa sobre F. schultzei. Esses extratos na concentração de 500 µg mL-1 foram testadas sobre ninfas de segundo ínstar de F. schultzei. O extrato hexânico de fumo foi o que causa maior mortalidade (28,1%). Assim, nenhum dos extratos hexânicos avaliados neste trabalho causa mortalidade satisfatória sobre ninfas de F. schultzei, na concentração de 500 µg mL-1.

In previous work we have presented a CSP based approach for developing component-based asynchronous systems, \(\mathcal {B}\mathcal {R}\mathcal {I}\mathcal {C}\), which guarantees deadlock freedom by construction. It uses CSP to specify the constraints and interactions between the components to allow a formal verification of the composition’s behaviour. Following this work, we also proposed an efficient approach for ensuring livelock analysis by construction. In this work we present a tool that automates the verification of component composition by automatically generating and checking the side conditions imposed by both approaches. The tool also includes a support to \(\mathcal {B}\mathcal {R}\mathcal {I}\mathcal {C}\mathcal {K}\), an optimisation of \(\mathcal {B}\mathcal {R}\mathcal {I}\mathcal {C}\), that enriches the components with metadata containing additional useful information, which considerably reduces the costs of the composition verifications.

The increasing interest in the combination of different computational paradigms is well represented by Hoare and He in the Unifying Theories of Programming (UTP). In this paper, we present a mechanisation of part of that work in a theorem prover, ProofPower-Z; the theories of alphabetised relations, designs, reactive and CSP processes are in the scope of this paper. Furthermore, the mechanisation of Circus , a language that combines Z, CSP, specification statements and Dijkstra’s guarded command language, is also presented here. We also present an account of how this mechanisation is achieved, and more interestingly, of what issues were raised, and of our decisions. We aim at providing tool support not only for CSP and Circus , but also for further explorations of Hoare and He’s unification, and for the mechanisation of languages whose semantics is based on the UTP.

In previous work we presented a CSP-based systematic approach that fosters the rigorous design of component-based development. Our approach is strictly defined in terms of composition rules, which are the only permitted way to compose components. These rules guarantee the preservation of properties (particularly deadlock freedom) by construction in component composition. Nevertheless, their application is allowed only under certain conditions whose verification via model checking turned out impracticable even for some simple designs, and particularly those involving cyclic topologies. In this paper, we address the performance of the analysis and present a significantly more efficient alternative to the verification of the rule side conditions, which are improved by carrying out partial verification on component metadata throughout component compositions and by using behavioural patterns. The use of metadata, together with behavioural patterns, demands new composition rules, which allow previous exponential time verifications to be carried out now in linear time. Two case studies (the classical dining philosophers, also used as a running example, and an industrial version of a leadership election algorithm) are presented to illustrate and validate the overall approach.

In previous work we have proposed a correct-by-construction approach for building deadlock-free CSP models. It contains a comprehensive set of composition rules that capture safe steps in the development of concurrent systems. In this paper, we extend that work by proposing and implementing a strategy for establishing livelock freedom based on constructive rules similar to those that ensure the absence of deadlock. Our method is based solely on the local analysis of the minimum sequences that lead the CSP model back to its initial state. The effectiveness of our livelock-analysis technique is demonstrated via three case studies. We compare the performance of our approach with that of two other techniques for livelock freedom verification: FDR2 and SLAP.

Circus specifications define both data and behavioural aspects of systems using a combination of Z and CSP constructs. Previously, a denotational semantics has been given to Circus; however, a shallow embedding of Circus in Z, in which the mapping from Circus constructs to their semantic representation as a Z specification, with yet another language being used as a meta-language, was not useful for proving properties like the refinement laws that justify the distinguishing development technique associated with Circus. This work presents a final reference for the Circus denotational semantics based on Hoare and He’s Unifying Theories of Programming (UTP); as such, it allows the proof of meta-theorems about Circus including the refinement laws in which we are interested. Its correspondence with the CSP semantics is illustrated with some examples. We also discuss the library of lemmas and theorems used in the proofs of the refinement laws. Finally, we give an account of the mechanisation of the Circus semantics and of the mechanical proofs of the refinement laws.

Circus is a refinement language, in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but refinements may be long and repetitive, and using this technique can be hard. Some useful strategies have already been identified, described, and used. By documenting and using them as tactics, a lot can be gained since they can be repeatedly used as single transformation rules. Here, we present ArcAngelC, a language for defining such refinement tactics; we present the language and its application in the formalisation of an existing informal strategy for verification of Ada implementations of control systems.

This article presents an analysis of the selection process of students from both private and public high schools in the state of Rio Grande do Norte (Northeast of Brazil), in order to form the first group of the Information Technology technical course of the Metropole Digital project at the Federal University of Rio Grande do Norte (UFRN). The selection instrument consists of a written exam built on the basis of a set of matrices that depict relevant competences and abilities expected from the students. Data concerning the profile of distribution of performance per exam question are presented, together with empirical evidences of the effectiveness of the proposed competence matrices in the selection process. The correlation very fied among the matrices compounding the instrument and scores in courses, and the instrument as a wholeand scores in courses is moderate to strong (rS = 0.6 and rS = 0.7; p < 0,05). The association between the criterion variables (Average of Performance in the Basic Moduleof courses) and the explicative variables (Total score in the selection instrument (QTot) and each of the five compounding matrices) is moderate (rS=0.51, p = 0.001), and the matrices and QTot are jointly responsible for 25% of the variance of the performance in the basic module. The regression coefficient for matrix 1 is 1.38 (CI of 95% = 1.07-1.68); for matrix 2 it was 0.65 (CI of 95% = 036-0.95); for matrix 3, 1.2 (CI of 95% = 0.92 - 1,55); matrix 4 0,76 (CI of 95% = 0.45-1.06); matrix 5 1.08 (CI of 95% = 0.78-1.39). The effects of student-descriptive independent variables on performance in the exam are also presented and discussed, and predictive relationships between performance in the exam and performance in the disciplines of the course are verified. Data collected allow concluding that the instrument of selection proposed fits well the aim of forming a group of students to undertake a technical course in the area of information technology.

In this paper we propose inheritance relations for a CSP-based component model (BRIC), which supports a constructive design based on composition rules that preserves desired properties such as deadlock freedom. We enhance this component model with support for extensibility via inheritance. The proposed relations allow extension of functionality, whilst preserving service conformance, which we define by means of a substitutability test. We also establish an algebraic connection between component extensibility and refinement. We illustrate our results by presenting a case study that consists of a bank system incrementally improved by inheritance.

This study examines the determinants of the outcome of bids for procurement of public works in the State of Ceará, once submitted to dispute with the presumption of equality among those interested in contracting with the Administration. Econometric models were developed to analyze if the amount of participants, the amount and bidding modality or type of department government can influence the final value and the corresponding discount on each event. The sample was extracted from transparency tools considering data from 2013, a period in which the Executive Power of State of Ceará bid more than R$ 5.6 billions in construction or engineering services. Robust estimates allow us to infer that the discount obtained through a bidding is directly affected by the number of participants and inversely by the value of the intended object, regardless of the modality and the kind of secretary of government. Together these results suggest that the bidding process practiced in every department of the State of Ceará is homogeneous, does not depend on the modality and the strategy to be considered by public managers in the State is reducing the bargaining power of the participants. Este estudo avalia possíveis determinantes do resultado das licitações para contratação de obras públicas no estado do Ceará, outrora submetidas à disputa com a presunção de igualdade entre os interessados em contratar com a Administração. Modelos econométricos foram desenvolvidos para analisar se a quantidade de participantes, o valor e a modalidade de licitação ou o tipo de secretaria de governo podem influenciar o valor final e o respectivo desconto de cada certame. A amostra foi extraída de instrumentos de transparência considerando dados de 2013, período em que o Poder Executivo cearense licitou mais de 5,6 bilhões de reais em obras ou serviços de engenharia. Estimativas robustas permitem inferir que o desconto obtido por meio de um certame licitatório é afetado diretamente pelo número de participantes e inversamente pelo valor do objeto licitado, independente da modalidade e do tipo de secretaria de governo. Em conjunto, estes resultados sugerem que o processo licitatório praticado em cada secretaria do estado do Ceará é homogêneo, independe da modalidade e a redução do poder de barganha dos participantes é a estratégia a ser considerada pelos gestores públicos do estado.

Morgan's refinement calculus is a successful technique for developing software in a precise and consistent way. This technique, however, can be hard to use, as developments may be long and repetitive. Many authors have pointed out that a lot can be gained by identifying commonly used development strategies, documenting them as tactics, and using them as single transformation rules. Also, it is useful to have a notation for describing derivations, so that they can be analysed and modified. In this paper, we present ArcAngel, a language for defining such refinement tactics; we present the language, its semantics, and some of its algebraic laws. Apart from Angel, a general-purpose tactic language that we are extending, no other tactic language has a denotational semantics and proof theory of its own.

Throughout the past decades two schools have been developing formal techniques for correct software development, taking complementary approaches: the model-based approach and the behavioural approach. Combinations of languages from both approaches have also been proposed. The lack of support for refinement of state-rich reactive systems in a calculational style has motivated the creation of Circus, a combination of Z, CSP, and Djikstra’s commmand language. In this paper, we foster the reuse of theoretical results underpinned on CSP to Circus by providing a sound mapping for processes and refinement from Circus to CSP. This mapping is proved sound from an existing link between these languages, established in the Unifying Theories of Programming (UTP). Our results allow analysing Circus specifications with techniques and tools, like FDR2 and PAT, originally developed for CSP. We illustrate the overall approach with a running example.

The complexity of concurrent systems can turn their development into a very complex and error-prone task. The use of formal methods like CSP considerably simplifies this task. Development, however, usually aims at reaching an executable program:i¾?a translation into a programming language is still needed and can be challenging. In previous work, we presented a tool, csp2hc, that translates a subset of CSP into Handel-C source code, which can itself be converted to produce files to program FPGAs. This subset restricts parallel composition:i¾?multi-synchronisation and interleaving on shared channels are not allowed. In this paper, we present an extension to csp2hc that removes these restrictions. We provide a performance analysis of our code.

Resumo: A partir de reflexoes acerca do recorte temporal e do sentido com que se deve compreender o termo Pre-modernismo, o presente estudo analisa a situacao de disputas e enfrentamentos por posicoes no campo artistico brasileiro, identificando agentes e suas praticas discursivas evidenciando, atraves da analise de textos da autoria desses agentes, propostas esteticas em conflito, segundo as quais grupos e individuos buscavam garantir legitimidade no referido campo. Palavras-chave: Pre-modernismo. Campo artistico. Agentes. Praticas discursivas. Propostas esteticas. Abstract: By means of reflections about this time frame, and the ways in which the term Pre-modernism should be understood, the current study analyzes the situation of quarrels and confrontations for positions in the Brazilian artistic field, identifying actors and their discursive practices, demonstrating through the analysis of texts written by these agents, aesthetic issues in conflict, according to which groups and individuals were trying to ensure legitimacy in the related field. Keywords: Pre-modernism. Artistic field. Actors. Discursive practices. Aesthetic issues.

Objetivo: Comparar os efeitos do polimento imediato e tardio (após sete dias) sobre a rugosidade superficial de quatro resinas compostas diretas: Suprafill, Opallis, Filtek Z250 e Filtek Z350. Materiais e Métodos: Quarenta espécimes (n=10) foram confeccionados a partir de uma matriz metálica de alumínio (5 mm Ø e 2mm de espessura). Cada grupo de resina composta foi submetido a dois tipos de polimento de forma aleatória. 5 amostras de cada grupo teve seu polimento realizado imediatamente e os outros 5 corpos de prova aguardaram sete dias para a realização do polimento com discos de óxido de alumínio Sof-Lex em todas as suas granulometrias diferentes. A rugosidade foi avaliada por meio de rugosímetro Surftest 211, série 178 (velocidade de 0,5 mm/s; distância de 0,25mm; ajuste em Ra µm). Os dados foram submetidos à análise estatística com o Teste paramétrico t de student pareado. Resultados: Os valores de p foram para G1=1 (0,58/0,58mm); G2=0,44 (0,59/0,51mm); G3=0,012 (0,6/0,95mm); e G4=0,33 (0,56/0,48mm), ou seja, houve diferença estatisticamente significativa apenas o G3, sendo pior o seu desempenho de lisura superficial após sete dias. Conclusão: não houve melhoria estatística dos resultados de rugosidade superficial após polimento tardio em relação ao polimento imediato (p>0,05).

Circus is a formal language that combines Z and CSP, providing support for specification of both data and behavioural aspects of concurrent systems. Furthermore, Circus has an associated refinement calculus, which can be used to develop software in a precise and stepwise fashion. Each step is justified by the application of a refinement law (possibly with the discharge of proof obligations). Sometimes, the same laws can be applied in the same manner in different developments or even in different parts of a single development. A strategy to optimize this calculus is to formalise this application as a refinement tactic, which can then be used as a single transformation rule. CRefine was developed to automate the Circus refinement calculus. However, before the work presented here, it did not provide support for refinement tactics. In this paper, we present an extension to CRefine: a new module that automates the process of defining and applying refinement tactics formalised in the tactic language ArcAngel C. Finally, we illustrate the usefulness of the extension in the development of an industrial case study.

This paper presents a new generation scheme for small hydroelectric power plants feeding weak grids. The configuration in use is a squirrel cage asynchronous machine as a generator, rather than the synchronous machine, which is most commonly used for this purpose. Besides the lower costs of acquisition and maintenance of the squirrel cage asynchronous machine, this paper presents a control based on a back-to-back converters arrangement. This control makes the rotor speed be adjusted online according to the water flow through the turbine. This way the potential power generated is significantly increased in addition to turbine operation damages prevention.

This paper presents a formal development of a cardiac pacing system based on a Boston Scientific's model, a pilot case study from the Grand Challenge in Software Verification. We present a summary of our Z model of the system, its translation into Perfect Developer, and the code generation and execution. Further practical result and analysis are also in the context of this paper.

This paper presents a migration approach from a class of hierarchical B models to CSP. The B models follow a so-called polling pattern, suitable for reactive systems, and are automatically translated into a set of communicating CSP processes with the same behaviour. The structure of the CSP model matches that of the B model and may be formally analysed using model checking. Selected CSP processes may then be further refined and synthesised to hardware, while the remaining modules would be mapped to software using B refinements. The translation proposed here paves the way for a model-based approach to hardware and software co-design employing complementary formal methods.

An important frequent task in both Z and B is the proof of verification conditions (VCs). In Z and B, VCs can be predicates to be discharged as a result of refinement steps, some proof about initialization properties or domain checking. Ideally, a tool that supports any Z and B technique should automatically discharge as many VCs as possible. Here, we present ZB2SMT, a Java package designed to clearly and directly integrate both Z and B tools to the satisfiability module theory (SMT) solvers such as veriT [1], a first-order logic (FOL) theorem prover that accepts the SMT syntax [4] as input. By having the SMT syntax as target we are able to easily integrate with further eleven automatic theorem provers. ZB2SMT is currently used by Batcave [2], an open source tool that generates VCs for the B method and CRefine [3], a tool that supports the Circus refinement calculus. Much of the VCs generated to validate the refinement law applications, are based on FOL predicates. Hence, CRefine uses the ZB2SMT package to automatically prove such predicates. The package integrates elements of Z and B predicates in a common language and transforms these predicates into SMT syntax. In this process, a SMT file is generated containing the predicate and some definitions. It is sent to a chosen SMT solver which yields a Boolean value for the predicate or it can be sent to several SMT solvers in a parallel approach. In order to improve the performance of the proof system, ZB2SMT has a module that can call different instances of solvers at different computers, according to a configuration file. It improves the proof process by allowing different strategies to be performed in parallel, reducing the verification time.

System-on-Chip is a solution that integrates several components of a computer into a single chip substrate. Those systems are generally targeted for embedded applications and can increase their processing power by using multiple processors and an on-chip interconnection. STORM is a Multi-Processor System-on-Chip virtual platform which uses a basic implementation of the MPI standard to provide communication among their applications. STORM implements a small set of MPI routines for essential point-to-point and collective communication in order to provide more programmability and portability for the applications of the platform. In this work, we make use of CSP to build a formal model of those MPI routines and eliminate imprecision and ambiguities that may arise from their informal descriptions on the MPI standard. Also, we use the FDR model checker to ensure that the implemented routines have no errors introduced during the development process.

We describe how to use a timeband architecture to model real-time requirements. The architecture separates requirements that use different time units, producing a family of models. Each model is characterised by its granularity and precision. These models are then linked using superposition, a kind of event refinement, and a loose synchronisation of their time units, with respect to their precision. Our models are written using CSP and checked using the FDR model checker. More complicated models use Circus, the state-rich process algebra. We show how to implement such a timeband architecture using the JCSP Java class library.

Considerando a magnitude global da tuberculose, destaca-se que os elementos da dimensão organizacional e de desempenho dos serviços de saúde que integram a Atenção Primária em Saúde (APS), são preponderantes para o controle da doença, quer seja em relação ao acesso, elenco de serviços, vínculo, coordenação da atenção, enfoque familiar, orientação na comunidade ou formação profissional. Nesta perspectiva, o presente estudo objetivou analisar a operacionalização do acesso e do vínculo, aos quais se integrou à adesão ao tratamento, dado que esta se refere, diretamente, as primeiras, além da sua importância para o controle da enfermidade. Trata-se de pesquisa quantitativa, ramo de um Projeto Matriz intitulado Avaliação das Dimensões Organizacionais e de Desempenho dos Serviços de Atenção Básica no Controle da Tuberculose em Municípios do Estado de São Paulo, tendo como referencial a teoria da determinação social do processo saúde-doença e o marco da APS. O projeto foi submetido e aprovado por Comitê de Ética em Pesquisa, e os dados foram coletados, de Julho a Setembro de 2008, por meio de instrumentos específicos, com questões fechadas, destinados a dois grupos de sujeitos: usuários portadores de tuberculose e profissionais de saúde que atuavam no controle da enfermidade, no âmbito de cinco Unidades Básicas de Saúde da Supervisão Técnica de Saúde da Subprefeitura Sé, no Município de São Paulo. Foram entrevistados 53 usuários e 40 profissionais de saúde. Apresentam-se os principais resultados: 79,2% dos usuários eram homens, em idade economicamente ativa (69,9%), com baixa escolaridade (77,3%) e que viviam sós (45,3%); 17,0% eram imigrantes provenientes da Bolívia e 90,5% viviam em áreas vulneráveis, que predispunham à ocorrência da tuberculose, como cortiços (39,6%), ocupações (7,5%) ou em situação de rua (43,4%); 62,2% tinham renda familiar mensal menor que um salário mínimo; 37,8% não tinham ocupação e importante parcela desenvolvia trabalhos esporádicos, com baixa qualificação; ressalta-se que 26,6% deixaram de trabalhar, após o início dos sintomas. Quanto aos profissionais entrevistados, 30,0% eram agentes comunitários de saúde, 30,0% eram auxiliares de enfermagem, 5,0% eram técnicos de enfermagem, 22,5% eram enfermeiros e 12,5% eram médicos. Quanto ao acesso, os principais pontos de estrangulamento foram: a restrição de benefícios; o número diminuído de visitas domiciliarias; dificuldade no encaminhamento para outros serviços, quando necessário; e oferecimento reduzido de informações acerca de outros problemas de saúde. Quanto ao vínculo, de modo geral, os entrevistados apontaram que se efetiva, destacando-se que, quanto menor a qualificação do trabalhador, mais importante é sua relação com os usuários. Quanto à adesão, os usuários apontaram que ocorre em função da motivação para a melhoria das condições de vida, para a recuperação da auto-estima e que os incentivos (cesta básica, vale-transporte e lanche) são importantes neste processo. Conclusão: ainda que o acesso e o vínculo se operacionalizem na região estudada, os resultados deste estudo apontam para a necessidade de aprimoramento da organização e do desempenho dos serviços de saúde da região, com o sentido de contribuir para a adesão ao tratamento e para o controle da tuberculose Considering the global magnitude of tuberculosis, it is emphasized that the elements of the organizational and effectiveness dimensions of health services that integrate the Primary Health Care (PHC), are fundamental to the control of the disease, whether in relation to accessibility, continuity (bonding), comprehensiveness, coordination, interpersonal and technical accountability. Therefore, this study aimed to analyze the operation of the access and the bonding, to which was integrated the treatment adherence, as it refers directly to them and because of its importance to the control of the disease. It is quantitative research, a branch of a major project entitled Organizational and effectiveness dimensions of Primary Care Services in the Control of Tuberculosis in counties in the State of Sao Paulo\", adopting the theory of social determination of health-illness process and in the mark of PHC. The project was approved by a Committee of Ethics in Research, and the data were collected from July to September of 2008, through specific instruments, with closed questions, aimed at two groups of subjects: patients with tuberculosis and health professionals who worked with them in five Primary Care Units from the Technical Supervision of Health of the Sub-prefecture Sé, in the City of São Paulo. 53 users and 40 professionals were interviewed. The main results: 79.2% of the patients were men, in the economically active age (69.9%), with low education (77.3%) and living alone (45.3%); 17.0 % were immigrants from Bolivia and 90.5% were living in vulnerable areas, that predisposed the occurrence of tuberculosis, as tenements (39.6%), occupations (7.5%) or homeless (43, 4%); 62.2% had family income less than a minimum wage, 37.8% had no job and a important part had sporadic work, with low qualifications, emphasizing that 26.6% stopped working after the beginning of the symptoms. As for the professionals, 30.0% were community health workers, 30.0% were nursing assistants, 5.0% were nursing technicians, 22.5% were nurses and 12.5% were physicians. Regarding the accessibility, the main problems were the restriction of the treatment incentives; the decreased number of home visits; difficulty in being referral to other services, when in need; and limited offering of information about other health problems. Regarding the bonding, in general, the respondents indicated that was effective, pointing out that as lower is the qualification of the professionals, the better was its relationship with users. As for adherence, users indicated that it occurs according the motivation to improve living conditions, for the recovery of self-esteem and, also, the incentives (food basket, bus-tickets and snacks) are important in this process. Conclusion: Although the access and the bond occurred within the study area, the results of this study points to the necessity to improve the organization and effectiveness of health services in the area, in order to contribute to treatment adherence and the control of tuberculosis

The lack of architecturally-significant mechanisms for aspectual composition might artificially hinder the specification of stable and reusable design aspects. Current aspect-oriented approaches at the architecture-level tend to mimic programming language join point models while overlooking mainstream architectural concepts such as styles and their semantics. Syntax-based pointcuts are typically used to select join points based on the names of architectural elements, exposing architecture descriptions to pointcut fragility and reusability problems. This paper presents style-based composition, a new flavor of aspect composition at the architectural level based on architectural styles. We propose style-based join point models and provide a pointcut language that supports the selection of join points based on style-constrained architectural models. Stability and reusability assessments of the proposed style-based composition model were carried out through three case studies involving different styles. The interplay of style-based pointcuts and some style composition techniques is also discussed.

The International Grand Challenge project on Verified Software is a long-term research program involving people from all over the world and is aimed to stimulate the creation of new theories and tools to be applied on industrial-scale problems. One of the challenges proposed is to make a formal development of a cardiac pacemaker. In this paper, we present a formal specification of this system using the Z notation and also discuss our experience in building this formal model and the decisions made during the process.

Circus specifications combine both data and behavioral aspects of concurrent systems using a combination of CSP, Z, and Dijkstrapsilas command language. Its associated refinement theory and calculus distinguishes itself from other such combinations. Recently, tools for Circus like a parser, a type-checker, a model-checker, and a translator to Java have been developed. Nevertheless, tool support for the circus refinement calculus has only been prototyped. In this paper, we present CRefine, a tool that can be used throughout the refinement of concurrent systems in a calculational approach. Its functionalities are described using a simple case study. Furthermore, we also describe CRefinepsilas architecture and its integration to the CZT framework.

Circus combine both data and behavioural aspects of concurrent systems using a combination of CSP, Z, and Dijkstra's command language. Its associated refinement theory and calculus distinguishes itself from other such combinations. Using a refinement calculus, we can correctly construct programs in a stepwise fashion. Each step is justified by the application of a refinement law, possibly with the discharge of proof obligations (hereafter called POs). The manual application of the refinement calculus, however, is an error-prone and hard task.

Partindo do pressuposto de que as respostas às necessidades de saúde oferecidas pelos serviços de saúde sofreram impacto com a regulamentação do Sistema Nacional de Saúde - SUS, o objetivo deste estudo foi apreender as tendências dessa reorganização em publicações científicas sobre o tema. Dentre 73 publicações selecionadas na base de dados on-line LILACS, 66 (90,4%) não abordavam o conceito de necessidades, utilizando o termo no senso comum; as que o abordavam tinham caráter de reflexão, sendo praticamente inexistentes as publicações que tomavam a perspectiva da Saúde Coletiva. Os artigos tomavam/definiam necessidades comuns a todos os indivíduos, considerando-os um agrupamento homogêneo de sujeitos abstratos, sem pertencimento de classe - que é o que determina e diferencia as necessidades de saúde. É preocupante o que os artigos revelam, pois a atenção à saúde vem privilegiando um recorte fragmentado que enfatiza a doença e pode reforçar práticas amparadas na visão funcionalista e classificatória, em detrimento de uma práxis emancipatória. This paper assumes that the health services' responses to health needs were affected by the regulation of the Brazilian public health system. Its objective is to capture the health-service trends found in scientific publications. Among the 73 publications selected from on-line databases, 66 (90.4%) did not mention the concept of health needs. Those that did had a reflective stance toward the subject. Health needs as defined in those articles were similar for all individuals, not considering them as members of a social class, a circumstance that defines health-needs characteristics. The results of this study are worrisome because health care delivery has been emphasizing sickness and reinforcing classification practices, rather than enabling emancipating praxis. Partiendo del presupuesto de que las respuestas a las necesidades de salud ofrecidas por los servicios de salud brasileños sufrieron un impacto con la regulación del Sistema Único de Salud (SUS), este estudio trata de aprehender las tendencias de tal reorganización en publicaciones científicas sobre el tema. Entre las 73 publicaciones seleccionadas en la base de datos on-line LILACS, 66 de ellas (90, 4%) no afrontaban el concepto de necesidades, usando el término en el sentido común; las que lo afrontaban tenían carácter de reflexión, siendo prácticamente inexistentes las publicaciones que encaraban la perspectiva de Salud Colectiva. Los artículos tomaban/definían necesidades comunes a todos los individuos, considerándoles una agrupación homogénea de sujetos abstractos sin alusión a clase que es lo que determina y distingue las necesidades de salud. Resulta objeto de preocupación lo que tales artículos revelan ya que la atención a la salud viene privilegiando un recorte que enfatiza la enfermedad y puede reforzar prácticas amparadas en la visión funcionalista y clasificadora, en detrimento de una praxis emancipadora.

280f. Submitted by Suelen Reis (suziy.ellen@gmail.com) on 2013-04-11T18:12:28Z No. of bitstreams: 1 Dissertacao Jean Araujoseg.pdf: 3152859 bytes, checksum: 3ef45787638eccde5ba291aa36d1b9c1 (MD5) Approved for entry into archive by Oliveira Santos Dilzaná(dilznana@yahoo.com.br) on 2013-05-09T14:12:09Z (GMT) No. of bitstreams: 1 Dissertacao Jean Araujoseg.pdf: 3152859 bytes, checksum: 3ef45787638eccde5ba291aa36d1b9c1 (MD5) Made available in DSpace on 2013-05-09T14:12:09Z (GMT). No. of bitstreams: 1 Dissertacao Jean Araujoseg.pdf: 3152859 bytes, checksum: 3ef45787638eccde5ba291aa36d1b9c1 (MD5) Previous issue date: 2006 FAPESB Este estudo tem por finalidade investigar o processo de desenvolvimento urbano implementado pelos grupos de elite da cidade da Bahia durante a segunda metade do século XIX e a primeira metade do século XX, permitindo compreender a configuração da cidade no início do século XXI. Tal processo foi impulsionado por um discurso modernizador que procurou efetivar, mediante uma política de controle social, a prevenção de enfermidades, a intervenção na estrutura física da cidade e a implantação da campanha de normatização para o uso pelos habitantes da cidade tanto do espaço público quanto privado, em especial, pelas camadas populares. Tem início, então, a produção do espaço capitalista que acontecia por intermédio de novas relações sociais, no movimento da vida, da natureza e da artificialidade, principalmente, no processo de construção de representações sobre os domínios do espaço citadino, constituindo, portanto, uma ferramenta essencial para os pensamentos e as ações voltados à produção e reprodução do capitalismo. Além de meio de produção, o espaço também constitui meio de controle, dominação e poder. A produção do espaço urbano na cidade da Bahia, a exemplo de outras cidades brasileiras e européias, seguia cada vez mais um parâmetro de segregação social, em que os grupos de elite, impulsionados pelo discurso de modernização, determinavam sua conformação, excluindo abertamente as camadas populares. Salvador

Circus specifications define both data and behavioural aspects of systems using a combination of Z and CSP. Previously, a denotational semantics has been given to Circus; however, as a shallow embedding of Circus in Z, it was not possible to use it to prove properties like the refinement laws that justify the distinguishing development technique associated with Circus. This work presents a final reference for the Circus denotational semantics based on Hoare and He's Unifying Theories of Programming (UTP). Finally, it discusses the library of theorems on the UTP that was created and used in the proofs of the refinement laws.

Circus is a refinement language in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but since refinements may be long and repetitive, the practical application of this technique can be hard. Useful strategies have been identified, described, and used, and by documenting them as tactics, they can be expressed and repeatedly applied as single transformation rules. Here, we present ArcAngelC, a language for defining such tactics; we present the language, its semantics, and its application in the formalisation of an existing strategy for verification of Ada implementations of control systems specified by Simulink diagrams. We also discuss its mechanisation in a theorem prover, ProofPower-Z.

ArcAngel is a specialised tactic language devised to facilitate and automate program developments using Morgan's refinement calculus. It is especially well-suited for the specification of high-level strategies to derive programs by construction, and equipped with a formal semantics that enables reasoning about tactics. In this paper, we present an implementation of ArcAngel for the ProofPower theorem prover. We discuss the underlying design, explain how it implements the semantics of ArcAngel, and examine differences in expressiveness and flexibility in comparison to ProofPower's in-built tactic language. ArcAngel supports backtracking through angelic choice; this is beyond the basic capabilities of ProofPower and many other main-stream theorem provers. The implementation is demonstrated with a non-trivial tactic example.

Na administração de Fábio da Silva Prado frente à Prefeitura de São Paulo, a municipalidade criou, em 1935, o Departamento de Cultura, sendo este o primeiro órgão municipal destinado à difusão, pesquisa e incentivo no campo das artes e da cultura. Participando efetivamente da elaboração do anteprojeto de criação do Departamento, Mário de Andrade assumiu a diretoria da instituição e, conforme determinava o regulamento, acumulou o cargo de Chefia da Divisão de Expansão Cultural. Pela abrangência do projeto e pelo ineditismo de suas iniciativas, o Departamento chamou a atenção de artistas, políticos e intelectuais interessados no estabelecimento de políticas públicas para a cultura no Brasil, tornando-se um centro de referência na capital paulista para assuntos relacionados às artes, aos divertimentos públicos, ao patrimônio cultural e à pesquisa sociológica, histórica e etnográfica. No âmbito da Divisão de Expansão Cultural, o projeto, aprovado em 1935, previa a criação de uma Rádio Escola, que seria o principal canal de comunicação do Departamento de Cultura com o público da cidade. Nesta Rádio, os ouvintes poderiam acompanhar concertos transmitidos do Teatro Municipal, programas de música ao vivo em estúdio, programas de discos selecionados do acervo da Discoteca Pública Municipal, e também conferências e cursos com intelectuais convidados. Apesar dos esforços da Diretoria do Departamento, a iniciativa nunca pôde ser implantada integralmente, isto é, a emissora, propriamente dita, nunca fora ao ar, o que não implica em dizer que tenha fracassado por completo. Para garantir a manutenção de uma programação com a qualidade pretendida, o Departamento necessitou criar uma estrutura institucional antes mesmo de dar início às irradiações. Primeiramente, foi criada uma seção burocrática, e, posteriormente, criou-se a Discoteca e os corpos musicais estáveis. Essa estrutura chegou a funcionar mesmo com a ausência de condições de levar ao ar a emissora, colocando em prática parte dos objetivos que o Departamento planejara para a Rádio Escola, sobretudo, no que se referia à formação do gosto musical do público paulistano. A Discoteca abriu seu acervo para consulentes e realizou gravações de música brasileira para o selo do Departamento de Cultura. Os corpos estáveis, por sua vez, realizaram, periodicamente, concertos públicos gratuitos de caráter educativo no Teatro Municipal. No contexto da década de 1930, período em que a expansão da atividade radiofônica já era perceptível no Brasil, e o projeto de criação de uma emissora do Departamento de Cultura estava relacionado às convicções intrínsecas aos intelectuais daquela época no potencial educativo da radiodifusão. During the administration of Fabio da Silva Prato in the City of São Paulo, the Municipality created in 1935 the Department of Culture, the first municipal institution for the dissemination, research, encouragement in the field of arts and culture. For having participated in the formulation of the outline in the Department creation, Mário de Andrade took over the management of the institution, as determined the regulation, he racked up the position of Head of the Cultural Expansion Division. Through the scope of the project and the originality of their initiatives, the Department drew the attention of artists, politicians and intellectuals interested in establishing public policies for culture in Brazil, becoming a reference center of the state capital for related matters to arts, public amusements, cultural heritage and sociological, historical and ethnographic research. As part of the Cultural Expansion Division the approved project in 1935 provided for the creation of a Radio School, which is the main communication channel of the Department of Culture with the public city. Listeners could follow broadcast concerts of the Municipal Theater, live music in studio programs, selected disks programs of collection of the Municipal Public Record Collection, aswell as conferences and courses with intellectual guests. In spite of the efforts of the Management of Department, the initiative cannot be implemented in full, that is, the station itself never aired. But that does not mean that have failed completely. To ensure maintenance of a schedule with the desired quality, the Department had to create an institutional structure before you even start the radiations. First created a bureaucratic section and from there created the Record Collection and stable musical groups. This structure came to work even without still had conditions to air the network, putting into practice the objectives of the planned Department for Radio School, especially as regards the formation of the musical taste of the São Paulo public. The Record Collection opened its heap to consultees and made of Brasilians music recordings for the stamp of the Department of Culture. Musical groups, in turn, periodically did free Public Concerts of educational nature at the Municipal Theater. In the context of the 1930s, when the expansion of radio activity was already noticeable in Brazil, the project to create a station of the Department of Culture is related to the belief that intellectuals of that time had about the educational potential of broadcasting.