Verification Of The Standard Vector Data Model For Interoperability Of River-Geospatial Information

Recently, two international standard organizations, ISO and OGC, have done the work of standardization for GIS. Current standardization work for providing interoperability among GIS DB focuses on the design of open interfaces. But, this work has not considered procedures and methods for designing river geospatial data. Eventually, river geospatial data has its own model. When we share the data by open interface among heterogeneous GIS DB, differences between models result in the loss of information. In this study a plan was suggested both to respond to these changes in the information envirnment and to provide a future Smart River-based river information service by understanding the current state of river geospatial data model, improving, redesigning the database. Therefore, primary and foreign key, which can distinguish attribute information and entity linkages, were redefined to increase the usability. Database construction of attribute information and entity relationship diagram have been newly redefined to redesign linkages among tables from the perspective of a river standard database. In addition, this study was undertaken to expand the current supplier-oriented operating system to a demand-oriented operating system by establishing an efficient management of river-related information and a utilization system, capable of adapting to the changes of a river management paradigm.

Uma Proposta de especificação formal e fundamentação teórica para simulated annealing

Os algoritmos baseados no paradigma Simulated Annealing e suas variações são atualmente usados de forma ampla na resolução de problemas de otimização de larga escala. Esta popularidade é resultado da estrutura extremamente simples e aparentemente universal dos algoritmos, da aplicabilidade geral e da habilidade de fornecer soluções bastante próximas da ótima. No início da década de 80, Kirkpatrick e outros apresentaram uma proposta de utilização dos conceitos de annealing (resfriamento lento e controlado de sólidos) em otimização combinatória. Esta proposta considera a forte analogia entre o processo físico de annealing e a resolução de problemas grandes de otimização combinatória. Simulated Annealing (SA) é um denominação genérica para os algoritmos desenvolvidos com base nesta proposta. Estes algoritmos combinam técnicas de busca local e de randomização. O objetivo do presente trabalho é proporcionar um entendimento das características do Simulated Annealing e facilitar o desenvolvimento de algoritmos com estas características. Assim, é apresentado como Simulated Annealing e suas variações estão sendo utilizados na resolução de problemas de otimização combinatória, proposta uma formalização através de um método de desenvolvimento de algoritmos e analisados aspectos de complexidade. O método de desenvolvimento especifica um programa abstrato para um algoritmo Simulated Annealing seqüencial, identifica funções e predicados que constituem os procedimentos deste programa abstrato e estabelece axiomas que permitem a visualização das propriedades que estes procedimentos devem satisfazer. A complexidade do Simulated Annealing é analisada a partir do programa abstrato desenvolvido e de seus principais procedimentos, permitindo o estabelecimento de uma equação genérica para a complexidade. Esta equação genérica é aplicável aos algoritmos desenvolvidos com base no método proposto. Uma prova de correção é apresentada para o programa abstrato e um código exemplo é analisado com relação aos axiomas estabelecidos. O estabelecimento de axiomas tem como propósito definir uma semântica para o algoritmo, o que permite a um desenvolvedor analisar a correção do código especificado para um algoritmo levando em consideração estes axiomas. O trabalho foi realizado a partir de um estudo introdutório de otimização combinatória, de técnicas de resolução de problemas, de um levantamento histórico do uso do Simulated Annealing, das variações em torno do modelo e de embasamentos matemáticos documentados. Isto permitiu identificar as características essenciais dos algoritmos baseados no paradigma, analisar os aspectos relacionados com estas características, como as diferentes formas de realizar uma prescrição de resfriamento e percorrer um espaço de soluções, e construir a fundamentação teórica genérica proposta.

OZJ : uma ferramenta para geração de óraculos para teste de software a partir de especificação formal

A literatura sobre Teste de Software apresenta diversas estratégias e metodologias que definem critérios eficazes e automatizáveis para selecionar casos de teste capazes de detectar erros em softwares. Embora eficientes na descoberta de erros, as técnicas de seleção de casos de teste exigem que uma quantidade relativamente grande de testes seja realizada para satisfazer os seus critérios. Essa característica acarreta, em parte, um alto custo na atividade de teste, uma vez que, ao fim de cada teste deve-se verificar se o comportamento do software está ou não de acordo com os seus requisitos. Oráculo para teste de software é um mecanismo capaz de determinar se o resultado de um teste está ou não de acordo com os valores esperados. Freqüentemente, assume-se que o próprio projetista de teste é o responsável por esta tarefa. A automatização da atividade dos oráculos deu origem a oráculos automáticos, os quais são capazes de determinar o bom ou mau funcionamento do software a partir de uma fonte de informação confiável. Ao longo dos anos, a especificação formal vêm sendo largamente utilizada como fonte de informação para oráculos automáticos. Diversas estratégias vêm propondo geradores de oráculos baseados em especificações formais. Dentre as características marcantes dessas estratégias, cita-se aquelas que são aplicáveis a implementações derivadas a partir da estrutura da especificação e aquelas que geram oráculos a partir de técnicas específicas de seleção de casos. Essas características, entretanto, limitam a aplicação abrangente dos oráculos por restringi-los tanto a implementações derivadas diretamente de especificações como ao uso de técnicas específicas de seleção de casos de teste. Este trabalho apresenta um estudo sobre os geradores de oráculos para teste de software, identifica aspectos fundamentais que regem seu processo de construção e propõe uma estratégia que permite a geração de oráculos semi-automaticamente, mesmo para implementações não derivadas diretamente da estrutura da especificação. A estratégia proposta é, também, aplicável aos casos de teste derivados de qualquer técnica de seleção de casos de teste.

Análise da gestão do líder formal em relação à implementação da mudança organizacional : estudo de caso na Universidade Federal do Rio Grande do Sul

Esta pesquisa analisa a gestão do líder formal em relação às mudanças acontecidas em sete Unidades de Ensino da Universidade Federal do Rio Grande do Sul (UFRGS), as quais decidiram unir seus ambientes de trabalho, pela falta de recursos humanos, para serem mais eficientes e dar um melhor atendimento à comunidade universitária. Segundo a Pró-Reitoria de Recursos Humanos da UFRGS, um dos principais fatores que fizeram com que a implementação das Secretarias Unificadas apresentasse situações de resistência e de conflito foram os problemas de liderança das pessoas que possuem autoridade formal e que dirigem as Unidades (líderes formais). Os resultados indicam que eles desconsideraram os elementos comportamentais e de planejamento da mudança no inicio e durante a implementação das Secretarias Unificadas. Foram entrevistados os líderes formais (Diretores e Assessores Administrativos) do Instituto de Geociências, do Instituto de Matemática, da Escola de Administração, da Escola de Educação Física, da Escola de Enfermagem, da Faculdade de Biblioteconomia e Comunicação e da Faculdade de Veterinária, e aplicaram-se questionários na totalidade dos funcionários das Secretarias Unificadas, para obter dados sobre estratégias implementadas, tipo de mudança, fatores facilitadores e fatores inibidores da mudança, características da liderança e gestão atual nas Secretarias Unificadas. A partir da análise dos dados coletados, chegou-se à afirmação de que o sucesso na gestão do líder formal nas Secretarias Unificadas de penderá da sua capacidade de criar boas condições de trabalho e desenvolver os fatores motivacionais, profissionais e pessoais, considerando que muitas das necessidades de mudança nas Unidades são compartilhadas e outras são específicas, devido aos seus interesses.

Extensão de um modelo OO formal com aspectos temporais

Na área de Engenharia de Software, há vários modelos formais de especificação orientado a objetos (OO). Um destes é o OO-Method / OASIS. OO-Method se baseia nos seguintes princípios: - dar suporte às noções do modelo conceitual orientado a objetos; - integrar os modelos formais com metodologias de aceitação industrial; - possibilitar a produção de software avançado que inclua a geração completa de código (estática e dinâmica) do desenvolvimento comercial. O processo de desenvolvimento consiste em levantar as propriedades principais do sistema em desenvolvimento (modelo conceitual) por parte do engenheiro de software, e construir de forma automática, em qualquer momento (por um processo de conversão gráfico-textual) a especificação formal orientada a objetos em OASIS (Open and Active Specifications of Information System) que constituirá um repositório de alto nível do sistema. O objetivo de OASIS é expressar os requisitos funcionais de um sistema de informação, em um marco formal, que facilite sua validação e geração automática de programas. OASIS não inclui a especificação de aspectos temporais. A modelagem de aspectos temporais é um importante tópico da modelagem de sistemas de informação, porque através destes são representadas as características dinâmicas das aplicações e a interação temporal entre diferentes processos. A especificação de requisitos de aplicações através de modelos orientados a objetos permite representar não só os seus estados, mas também, seu comportamento. Modelos temporais representam também a evolução de objetos com o tempo. Como o estado de um objeto pode ser alterado devido à ocorrência de um evento (fato ocorrido em um determinado instante no tempo), é importante que o modelo utilizado permita apresentar a história destes eventos. O presente trabalho tem por finalidade propor uma extensão temporal a um modelo formal de especificação OO. Esta extensão inclui tanto aspectos estáticos quanto dinâmicos. A extensão de aspectos estáticos estende OASIS com atributos temporais. A extensão dos aspectos dinâmicos, contribuição central do trabalho, estende OASIS com eventos temporais.

Um Modelo formal e executável de agentes BDI

Modelos BDI (ou seja, modelos Beliefs-Desires-Intentions models) de agentes têm sido utilizados já há algum tempo. O objetivo destes modelos é permitir a caracterização de agentes utilizando noções antropomórficas, tais como estados mentais e ações. Usualmente, estas noções e suas propriedades são formalmente definidas utilizandos formalismos lógicos que permitem aos teóricos analisar, especificar e verificar agentes racionais. No entanto, apesar de diversos sistemas já terem sido desenvolvidos baseados nestes modelos, é geralmente aceito que existe uma distância significativa entre esta lógicas BDI poderosas e sistemas reais. Este trabalho defende que a principal razão para a existência desta distância é que os formalismos lógicos utilizados para definir os modelos de agentes não possuem uma semântica operacional que os suporte. Por “semântica operacional” entende-se tanto procedimentos de prova que sejam corretos e completos em relação à semântica da lógica, bem como mecanismos que realizem os diferentes tipos de raciocínio necessários para se modelar agentes. Há, pelo menos, duas abordagens que podem ser utilizadas para superar esta limitação dos modelos BDI. Uma é estender as lógicas BDI existentes com a semântica operacional apropriada de maneira que as teorias de agentes se tornem computacionais. Isto pode ser alcançado através da definição daqueles procedimentos de prova para as lógicas usadas na definição dos estados mentais. A outra abordagem é definir os modelos BDI utilizando formalismos lógicos apropriados que sejam, ao mesmo tempo, suficientemente poderosos para representar estados mentais e que possuam procedimentos operacionais que permitam a utilizaçao da lógica como um formalismo para representação do conhecimento, ao se construir os agentes. Esta é a abordagem seguida neste trabalho. Assim, o propósito deste trabalho é apresentar um modelo BDI que, além de ser um modelo formal de agente, seja também adequado para ser utilizado para implementar agentes. Ao invés de definir um novo formalismo lógico, ou de estender um formalismo existente com uma semântica operacional, define-se as noções de crenças, desejos e intenções utilizando um formalismo lógico que seja, ao mesmo tempo, formalmente bem-definido e computacional. O formalismo escolhido é a Programação em Lógica Estendida com Negação Explícita (ELP) com a semântica dada pelaWFSX (Well-Founded Semantics with Explicit Negation - Semântica Bem-Fundada com Negação Explícita). ELP com a WFSX (referida apenas por ELP daqui para frente) estende programas em lógica ditos normais com uma segunda negação, a negação explícita1. Esta extensão permite que informação negativa seja explicitamente representada (como uma crença que uma propriedade P não se verifica, que uma intenção I não deva se verificar) e aumenta a expressividade da linguagem. No entanto, quando se introduz informação negativa, pode ser necessário ter que se lidar com programas contraditórios. A ELP, além de fornecer os procedimentos de prova necessários para as teorias expressas na sua linguagem, também fornece um mecanismo para determinar como alterar minimamente o programa em lógica de forma a remover as possíveis contradições. O modelo aqui proposto se beneficia destas características fornecidas pelo formalismo lógico. Como é usual neste tipo de contexto, este trabalho foca na definição formal dos estados mentais em como o agente se comporta, dados tais estados mentais. Mas, constrastando com as abordagens até hoje utilizadas, o modelo apresentanto não é apenas uma especificação de agente, mas pode tanto ser executado de forma a verificar o comportamento de um agente real, como ser utilizado como mecanismo de raciocínio pelo agente durante sua execução. Para construir este modelo, parte-se da análise tradicional realizada na psicologia de senso comum, onde além de crenças e desejos, intenções também é considerada como um estado mental fundamental. Assim, inicialmente define-se estes três estados mentais e as relações estáticas entre eles, notadamente restrições sobre a consistência entre estes estados mentais. Em seguida, parte-se para a definição de aspectos dinâmicos dos estados mentais, especificamente como um agente escolhe estas intenções, e quando e como ele revisa estas intenções. Em resumo, o modelo resultante possui duas características fundamentais:(1) ele pode ser usado como um ambiente para a especificação de agentes, onde é possível definir formalmente agentes utilizando estados mentais, definir formalmente propriedades para os agentes e verificar se estas propriedades são satifeitas pelos agentes; e (2) também como ambientes para implementar agentes.

Educação musical não-formal e atuação profissional : um survey em oficinas de música de Porto Alegre - RS

O presente trabalho teve como objetivo caracterizar o ensino de música inserido em projetos sociais. Os objetivos específicos foram analisar as dimensões presentes nas práticas educativo-musicais das oficinas de música, identificar os profissionais que ali ensinam música e qual a sua formação, e examinar as concepções sobre educação musical desses profissionais e do coordenador. O referencial teórico do trabalho está fundamentado em conceitos de educação não-formal, de autores da pedagogia e da educação musical. Foi realizado um survey de pequeno porte em 19 oficinas de música do projeto de Descentralização, da Secretaria Municipal de Cultura, da Prefeitura de Porto Alegre. Os participantes foram 14 oficineiros (profissionais que ensinam música) e o ativista de música (coordenador das oficinas). A técnica de pesquisa utilizada foi a da entrevista semi-estruturada, e os dados foram analisados qualitativamente. A partir da análise, considerei que as oficinas de música se configuram como espaços de educação musical não-formal. Os resultados sinalizam a necessidade de reconhecimento desses espaços como contextos de atuação profissional que, como tais, demandam uma formação também profissional.

Entre o Controle social formal e o (des) controle fragmentado

A presente dissertação discute a participação cidadã na gestão pública, em três áreas do governo municipal de São Gonçalo: saúde , educação e a implantação do orçamento participativo. São apresentados os fundamentos teóricos para se tentar o fenômeno: a noção de participação, os limites da democracia representativa e as potencialidades de uma maior participação política na gestão local. Confrontam-se a teoria com os casos empíricos e conclui-se que mais que uma participação na gestão o que se observa é construção de formas de gestão desta participação. Ainda que haja algum nível de interferência de ação dos representantes da sociedade civil nas ações do governo local, e sempre há, esta é crescentemente gerida pelo próprio governo.

Visões das gerências da auditoriainterna da Petrobras sobre a sua estratégia de atuação em facedas práticas de mercado e da nova modelagem organizacional da companhia

The purpose of this study is to identify the strategic vision of the Internal Audit Department of Petrel Brasileiro S.A. PETROBRAS, in comparison with the audit function's proposals and practices in competitive organizations and their reality. It also aims at the verification of the possible solutions, within Petrobras itself, so as to constantly add value to the business and to the shareholders. With this in mind, a research was carried out, contemplating the conceptual proposals and market practices related to auditing and to the current diagnosis and the organizational model of Petrobras, so as to choose elements for comparison and analysis of such vision. The results of this research pointed in the direction of questioning the organizational value of the internal audit action, concluding that it will only be possible to continuously attain such value by means of a permanent coordination with the organization's strategic level. This is especially true if the audit action participates effectively in the process of Corporate Governance, in defining the risks, the internal control system and the measurement of corporate performance, as related to the development of the strategic plan. However, any action along these lines is still heavily impacted and limited by several aspects of culture and relationship of the organizational power as well as by the beliefs of the organization and of the body of auditors. The involvement of the auditors as employees was also considered relevant in the auditing process, by means of the participation of the audited entities in self assessment2. This procedure is still not sufficiently guaranteed by successful experiments in major organizations, considering that there is not a clear demonstration of the effective benefits of adopting this practice, as ompared to the central control, seldom shared but strongly monitored by integrated information systems. Finally, this research points to the need to renew the concept of the formation and role of the auditors in modern competitive organizations, in the face of information technology and of automation of the instrument controls of the business. Therefore, one may conclude that the trend will be toward an action aiming at the revision of formal internal control matrixes, as they are established in such systems. On the other hand, the majority of audit human resources will be increasingly deployed to the evaluation of risk and control, as related to relevant events of a more abstract nature, as in the case of those connected with the uncontrollable factors of the external environment.

Poder normativo da Justiça do Trabalho : direito formal da classe trabalhadora brasileira

Resumo não disponível.

A flexibilização do processo de formulação de estratégias empresarias. O caso da transportadora brasileira Bolivia-Brasil

Com a maIOr interação entre povos, culturas e nações e a conseqüente abertura dos mercados, a concorrência entre as organizações tem aumentado consideravelmente, forçando-as a buscarem diferenciais que lhes garantam a criação e a manutenção de altos níveis de competitividade. A presença de algumas das técnicas de flexibilização do processo formal de formulação de estratégias pode ser um indicativo de maior preocupação das empresas com a instabilidade externa, porém, sem necessariamente, dar à organização o poder de adaptar-se continuamente às possíveis alterações. o presente estudo pretende analisar o caso da Transportadora Brasileira Gasoduto BolíviaBrasil sob o prisma das teorias de Motta, Mintzberg e Grant verificando se o processo de formulação de estratégias da citada organização se caracteriza pela criação de estratégias emergentes ou deliberadas e se demonstra flexibilidade diante do ambiente externo.

Autogestão, participação e estrutura organizacional: uma análise crítica da evolução formal da empresa média atual

Analisa a evolução histórica da estrutura formal da empresa, avaliando a questão da participação e da autogestão. Procura discutir, a partir de uma perspectiva metodológica definida, a possibilidade da paticipação real dos trabalhadores na ação produtiva, considerando a autogestão enquanto a formação discursiva de uma vontade coletiva e propõe um modelo organizacional teoricamente mais adequado a esta prática

Do formal para o informal: executivos em trabalhos flexíveis

Quando observamos o mundo do trabalho atual, percebemos que, há um movimento em direção à maior flexibilidade, tanto em relação aos empregados formais quanto aos trabalhadores que passam a atuar por meio de formas flexíveis de contrato de trabalho. O contrato de emprego flexível refere-se àquele que não segue o modelo formal de contrato de trabalho, regido por CLT (Consolidação das Leis do Trabalho), e, vem sendo estudado ultimamente como um resultado das mudanças na organização do trabalho, em geral, associado à busca por trabalhadores mais produtivos e de menor custo. Devido à amplitude dos fenômenos envolvidos nestas transformações, delimitamos o tema e o público a ser estudado: adotando a idéia de construção social da realidade, de Berger e Luckmann (1966/2002), analisamos os processos de “migração” de 30 executivos, residentes no município de São Paulo, ex-empregados de grandes corporações, que tiveram experiências em cargos de gerência média e alta em organizações nacionais e multinacionais, e, que atualmente, trabalham no mercado sob regime de contratos flexíveis. Para nosso estudo, entendemos os executivos como trabalhadores formais que ocupam posições de alta e média gerência na hierarquia organizacional e detêm posições de poder e prestígio. Assim, o objetivo deste estudo é descrever o sentido atribuído por executivos, ao processo de “migração” para formas mais flexíveis de trabalho e à nova realidade vivida no trabalho. A pesquisa segue uma abordagem qualitativa, utilizando-se de entrevista em profundidade semi-estruturada, para a coleta de dados; para a análise das entrevistas realizadas, usamos, como base, as idéias de práticas discursivas e produção de sentidos, de Spink e Medrado (1999/2004). A abordagem construcionista permitiu verificar que os executivos em trabalhos flexíveis possuem alto nível de autoconfiança, uma visão missionária sobre o seu trabalho, e diversos motivos diferentes para a “migração”. Por meio de seus relatos, pode-se observar as estratégias para a sobrevivência e obtenção de sucesso como um trabalhador flexível; a percepções dos entrevistados sobre o mercado brasileiro; a mudança de relacionamento com os clientes, a família e a rede de contatos. Apesar dos problemas enfrentados para se estabilizar, a maioria demonstra a vontade de permanecer no trabalho flexível, contrariando grande número de estudo que enxergam a flexibilização de contratos de trabalho como precarização para os trabalhadores. Para os executivos em regime flexível, a vida como trabalhador CLT parece fazer parte do passado: agora, eles precisam se mostrar competentes a qualquer custo, planejar-se para as “entressafras”, buscar melhorar a rede de contatos, aumentar o conhecimento e passar um tempo com a sua família. Os motivos de permanência são diversos, mas possuem um ponto de conversão: a sensação de deter o domínio sobre a sua vida, seu tempo, seu dinheiro, seu conhecimento, seu futuro. Talvez, o cotidiano apresente muitas situações de submissão à vontade do cliente e de dedicação maior do que na época de empregado formal; mas, na “realidade cotidiana”, a sensação é de ser o “dono” da sua vida.

Semântica formal para TVQL

Modelos de bancos de dados têm sido progressivamente estendidos a fim de melhor capturar necessidades específicas de aplicações. Bancos de dados versionados, por exemplo, provêm suporte a versões alternativas de objetos. Bancos de dados temporais, por sua vez, permitem armazenar todos os estados de uma aplicação, registrando sua evolução com o passar do tempo. Tais extensões sobre os modelos de dados se refletem nas respectivas linguagens de consulta, normalmente sob a forma de extensões a linguagens conhecidas, tais como SQL ou OQL. O modelo de banco de dados TVM (Temporal Versions Model ), definido sobre o modelo de banco de dados orientado a objetos, suporta simultaneamente versões alternativas e o registro de alterações de objetos ao longo do tempo. A linguagem de consulta TVQL (Temporal Versioned Query Language), definida a partir da linguagem de consulta SQL, permite recuperar informações do modelo de dados TVM. As construções introduzidas em TVQL têm como objetivo tornar simples a consulta do banco de dados em diversos pontos da linha temporal. Apesar das vantagens da utilização da linguagem TVQL para resgatar dados temporais do modelo TVM, existem algumas limitações importantes para seu aprimoramento. Uma delas é a alta complexidade do modelo TVM, proveniente da integração de conceitos variados como estados alternativos e rótulos temporais. Outro ponto é que, até o presente momento, não existe um interpretador para TVQL, impedindo uma experiência prática de programação de consultas. O objetivo principal deste trabalho é o desenvolvimento de uma especificação formal para a linguagem TVQL, tornando possível um estudo consistente de suas construções. Adicionalmente, uma especificação formal serve como documentação para futuras implementações de interpretadores. Neste trabalho foi desenvolvido um protótipo de avaliador de consultas e verificador de tipos para um núcleo funcional da linguagem TVQL, possibilitando também uma experimentação prática sobre os modelos propostos.