Made available in DSpace on 2014-06-12T15:51:19Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2008 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / Message Sequence Charts (MSC) é uma linguagem gráfica, usada na academia e na indústria, cujo objetivo é descrever o comportamento de componentes de sistemas e seus ambientes. A sintaxe e a semântica de um diagrama MSC padrão são definidos pelo International Telecommunication Union. A motivação para esse trabalho foi originada a partir de esforços para modelar cenários de aplicações de aparelhos móveis com o objetivo de automatizar a geração de testes, no contexto de uma colaboração entre Centro de Informática da Universidade Federal de Pernambuco (CIn- UFPE) e a Motorola, no contexto do projeto Brasil Test Center (BTC). Ao modelar algumas destas aplicações que envolvem múltipla sincronização utilizando como linguagem de modelagem, MSC padrão, constatou-se que os diagramas são de difícil entendimento ou com um comportamento diferente do desejado. É proposta neste trabalho uma extensão de MSC com o objetivo de permitir a descrição de mensagens síncronas, que permitem descrever eventos instantâneos (abstraindo-se a duração do tempo real para que a conexão seja estabelecida) e podendo envolver várias instâncias de MSC. Essa extensão é conservativa, no sentido que o comportamento das construções existentes não é afetado pela mesma; além disso, em um mesmo diagrama é possível conter mensagens síncronas e mensagens assíncronas. Foi desenvolvido um algoritmo de transformação, que a partir de um diagrama escrito na notação MSC estendido, gera um diagrama correspondente na notação de MSC padrão. Este algoritmo tem por objetivo permitir a transitividade entre as notações e demonstrar suas equivalências. Este algoritmo de transformação implementa mensagens síncronas como uma seqüência de mensagens assíncronas seguindo um algoritmo particular de handshake. A segunda contribuição desse trabalho é a definição de uma semântica para a notação padrão e estendida de MSC. Essa definição é dada em termos da álgebra de processos CSP (Communicating Sequential Processes). O formalismo introduzido na notação de Message Sequence Charts com CSP permite mostrar a equivalência entre um diagrama na notação de MSC estendido e seu correspondente descrito em MSC padrão, gerado a partir do algoritmo de transformação. Além disso, modelar MSC como um processo descrito na notação CSP permite uma análise sobre seus diagramas, usando um rico conjunto de leis algébricas de CSP, bem como o uso de ferramentas, como FDR2 e o Probe. Finalmente, para validar a estratégia proposta, desenvolveu-se um exemplo que ilustra a utilização da notação estendida de MSC, notação síncrona; a conversão desta notação para a notação padrão e a equivalência entre o MSC estendido e o padrão. Mostramos, ainda, o uso da ferramenta Power Tool Kit(PTK) para geração de casos de teste a partir de diagramas MSC

Made available in DSpace on 2014-06-12T15:52:01Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2008 / A integração de métodos formais com notações semi-formais visuais é uma tendência em engenharia de software. Métodos formais apresentam uma semântica precisa e permitem verificação de propriedades. No entanto, não são considerados intuitivos. Por outro lado, notações semi-formais visuais, como UML, são facilmente integradas no processo de desenvolvimento de software. Assim, métodos formais e semi-formais visuais são complementares. CSP e UML-RT são, respectivamente, exemplos de notação formal e diagramática usados para especificar e projetar sistemas concorrentes e distribuídos. CSP é um método formal no qual processos representam unidades comportamentais que se comunicam através de canais de comunicação, utilizando passagem de mensagem. UML-RT é uma extensão conservativa de UML na qual cápsulas são unidades comportamentais que se comunicam através de portas de comunicação. Portas realizam protocolos os quais especificam os sinais que podem ser enviados e recebidos através de uma porta, e a ordem na qual os sinais podem ser comunicados. Em um trabalho anterior, Ferreira apresentou um conjunto de regras que sistematizam o mapeamento de CSP para UML-RT, mas uma prova formal deste mapeamento não foi apresentada. Assim, para garantir consistência no desenvolvimento de sistemas concorrentes e distribuídos utilizando este mapeamento, a prova formal do mesmo é indispensável, uma vez que não faz sentido o esforço dedicado à especificação do sistema em CSP e a verificação de propriedades e refinamentos, se uma ou mais regras de mapeamento estiverem incorretas. No entanto, UMLRT não possui uma semântica formal padrão. Entre outras propostas de semântica formal, Ramos propõe uma semântica para UML-RT utilizando OhCircus (uma combinação de CSP e Z com características adicionais de orientação a objetos) como modelo semântico. Neste trabalho, é proposta uma variação da semântica de Ramos para UML-RT usando CSP como modelo semântico. Com base nesta semântica, é apresentada a prova do mapeamento de CSP para UML-RT, considerando o modelo de falhas e divergências de CSP. Assim, este trabalho consolida a integração de CSP e UML-RT proposta por Ferreira, no desenvolvimento de sistemas críticos, concorrentes e distribuídos. Um resultado interessante foi observar que, estritamente, as regras propostas por Ferreira não preservam a semântica de CSP, essencialmente com relação a aspectos de terminação dos processos

Made available in DSpace on 2014-06-12T15:57:05Z (GMT). No. of bitstreams: 2 arquivo3138_1.pdf: 1790380 bytes, checksum: 8d08d6e97caeb1942c705627bab1ddc6 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2007 / Centro de Estudos Avançados do Recife / Engenharia de software visa criar software de maneira econômica, que seja confiável e que trabalhe eficientemente em máquinas reais. Um de seus principais objetivos é obter um grau de qualidade mínimo que, em geral, significa uma baixa taxa de defeitos. Considerando que qualidade é crítico para o sucesso do software, o uso de testes vem crescendo. Testes objetivam revelar a presença de erros o mais cedo possível no ciclo de desenvolvimento. Embora teste de software seja uma atividade complexa, geralmente não é realizada sistematicamente devido a uma série de fatores como limitações de tempo, recursos e qualificação técnica dos envolvidos. Dessa forma, a automação de testes é uma tendência na área de testes. Esse trabalho está inserido no contexto de um projeto de pesquisa realizado pela Motorola em parceria com o Centro de Informática da Universidade Federal de Pernambuco denominado CInBTCRD (CIn and Brazil Test Center Research and Development Project). Na Motorola, a automação de testes faz-se por meio de um framework denominado de TAF (Test Automation Framework), o qual simula a interação de um ser humano com um aparelho celular, além de poder capturar o estado e outras informações importantes do aparelho. Testes reusam implementações já definidas no TAF para criar os scripts de teste, bem como novas implementações são criadas quando o reuso não é possível. Visto que bastante tempo é gasto para criar tais implementações, este trabalho propõe criar uma estratégia que, dado um script de teste, gere código para o TAF das funcionalidades ainda não implementadas automaticamente. Para gerar tais códigos, foi utilizada a linguagem formal CSP (Communicating Sequential Processes) como base. CSP foi criada para especificar e projetar comportamentos de sistemas concorrentes e distribuídos. CSP possui uma teoria de refinamentos associada, a qual é o alicerce de nossa proposta. O uso de refinamento em nossa proposta é relativamente simples: dado um teste em TAF descrito usando CSP e o comportamento de um celular também em CSP, a relação de refinamento só será satisfeita quando todos os elementos contidos no teste estiverem de acordo com o definido no comportamento do celular. Assim sendo, nesse trabalho usamos a ferramenta BxT (Behavior Extractor Tool) que desenvolvemos no contexto do projeto de pesquisa para extrair automaticamente um modelo CSP de um celular, bem como reusamos um outro trabalho que consegue representar casos de teste em CSP e criamos um algoritmo que usa esses elementos e a teoria da refinamento de CSP para completar certas partes do caso de teste com o auxílio do modelo do celular. Finalmente, o teste em CSP resultante é novamente escrito em TAF e dessa forma conseguimos atualizar o framework automaticamente

Made available in DSpace on 2014-06-12T15:59:36Z (GMT). No. of bitstreams: 2 arquivo5340_1.pdf: 1555764 bytes, checksum: d3735403fc535c9dd852536b0afde205 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2007 / A escrita de requisitos, dentro do processo de desenvolvimento de sistemas, está sujeita a falhas, uma vez que os requisitos são escritos em Linguagem Natural, como Inglês, que pode conter definições ambíguas ou de difícil entendimento. Por outro lado, Linguagem Natural é a opção mais simples e flexível para se especificar um sistema, e é a linguagem de entendimento comum entre clientes e contratados. Desta forma, para minimizar a existência de erros nos documentos de requisitos, técnicas de validação com inspeção ou revisão de documentos são utilizadas. Entretanto, o custo de se realizar este tipo de validação é alto e sua eficácia é questionável; erros podem persistir. Além disso, requisitos escritos usando de linguagem natural são de difícil processamento, dificultando a geração de outros artefatos a partir do mesmo. Esta dissertação define uma estratégia que utiliza templates de especificação de casos de use e uma Linguagem Natural Controlada (LNC) para descrever requisitos. Os templates de casos de uso asseguram a estruturação correta do documento de requisitos e a LNC garante a exatidão da gramática do texto que especifica o comportamento do sistema. Foram criados dois templates de casos de uso, cada um com uma visão diferente do sistema. A visão mais abstrata se chama visão do usuário e a visão mais detalhada se chama visão de componentes. A partir dessa estruturação dos requisitos torna-se, possível definir uma estratégia de geração automática de uma especificação formal da aplicação em questão. A geração automática de especificação formal de sistemas reduz custo e necessidade de mão de obra especializada em projetos de desenvolvimento de software. Ou seja, uma vez que é possível realizar a geração automática do modelo formal de sistemas podemos fazer uso do mesmo na validação de propriedades do sistema. Além disso, artefatos como casos de teste e diagramas UML podem ser gerados a partir deste. Em particular, esta dissertação define uma estratégia para gerar modelos formais na álgebra de processo CSP a partir das duas visões de caso de uso, mantendo a consistência entre os artefatos. Também foi definida uma relação de refinamento entre os modelos gerados garantindo a consistência entre as visões. Finalmente, todo o processo foi automatizado através de ferramentas. Estas foram vali- dadas através de experimentos realizados no contexto de aplicação para celulares da Motorola, empresa parceira e financiadora do projeto de pesquisa com o CIn/UFPE

Made available in DSpace on 2014-06-12T15:59:48Z (GMT). No. of bitstreams: 1 license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2007 / A especificação formal de um sistema ou seu modelo formal é uma forma abstrata de representar suas propriedades (características). Métodos formais é um ramo da Engenharia de Software com foco no desenvolvimento de sistemas tendo uma especificação formal do mesmo como ponto de partida. Inicialmente, as vantagens de usar notações abstratas antes da implementação do sistema estavam apenas relacionadas a um melhor entendimento do problema. Depois, tornou-se evidente que o uso de notações formais abstratas combinadas com técnicas de refinamentos de modelos reduzem o tempo de desenvolvimento e aumentam a qualidade do produto de sistema. A fase de testes é positivamente influenciada pelo uso de métodos formais. Pesquisas têm sido desenvolvidas para melhorar a qualidade do sistema usando modelos formais e casos de teste. Uma vez verificadas as propriedades do sistema através de uma investigação dos modelos formais, é possível gerar casos de testes confiáveis do sistema que serão colocados em ação para verificar a implementação do sistema posteriormente. O campo de pesquisa que explora métodos formais aplicados com testes de software é chamada de Testes Baseados em Modelos, ou simplesmente MBT, do inglês Model-Based Testing. Porém, há situações onde não é possível possuir o modelo abstrato definido a priori. Para superar tal restrição outras técnicas surgiram para sintetizar um modelo abstrato seguindo apenas execuções do sistema. As execuções de um sistema contêm comportamentos necessários para construir um modelo abstrato desse sistema. Na literatura atual, tais técnicas usadas para construir representações abstratas seguindo execuções do sistema são chamadas de Anti-Model- Based Testing ou simplesmented Anti-MBT. Então, depois de construir um modelo abstrato, técnicas de verificação de modelos e geração de casos de teste seguindo modelos formais podem ser aplicadas normalmente. O propósito desse trabalho é dar suporte a algumas técnicas de MBT usadas no contexto da Motorola (CIn/BTC). Em tais técnicas, as especificações usadas para gerar casos de testes são geralmente incompletas, inconsistentes, e às vezes não existem. Portanto, usando casos de testes reais do sistema é possível criar novas especificações e atualizar especificações originais do sistema, e posteriormente gerar novos casos de teste usando comportamentos válidos do sistema. Um outro problema detectado em nosso contexto é a distância existente entre as representações abstratas e reais. Um caso de teste abstrato, por exemplo, é útil em técnicas formais, mas não é possível executar um caso de teste diretamente no sistema. Dessa forma, para executar (manualmente ou automaticamente) os casos de teste gerados pelas técnicas de MBT é necessário primeiro traduzi-los em uma representação real. Como resultado desse trabalho nós desenvolvemos técnicas formais de modelagem do comportamento do sistema usando casos de teste. Os resultados das técnicas de modelagem são modelos formais especificados nos formalismos de LTS ou CSP. Além disso, nós definimos uma técnica de unificação que une modelos formais gerados a partir de diferentes artefatos do sistema (requisitos e casos de teste). O resultado da técnica de unificação é um completo e unificado modelo do sistema, que contém informações providas de diferentes artefatos. Nós também definimos uma técnica para traduzir casos de teste abstratos em representações reais. Os casos de teste reais gerados por nossa técnica de tradução são usados no contexto do time de automação de testes da Motorola, onde esse trabalho está inserido. Finalmente, nós automatizamos as técnicas desenvolvidas usando linguagens de programação e especificações formais. O resultado é a ferramenta TCRev que é capaz de modelar, unificar e traduzir modelos do sistema. A ferramenta TCRev interage com o outras ferramentas externas, tais como FDR e FDR Explorer. Todos os resultados foram validados em estudos de casos reais executados no contexto da Motorola. Nessa dissertação nós apresentamos um destes estudo de casos

Submitted by Renata Lopes (renatasil82@gmail.com) on 2017-09-27T12:20:13Z No. of bitstreams: 1 felipedefreitasfonseca.pdf: 1431342 bytes, checksum: b363be3713c64bee0af77b9414f7632f (MD5) / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2017-09-27T13:43:20Z (GMT) No. of bitstreams: 1 felipedefreitasfonseca.pdf: 1431342 bytes, checksum: b363be3713c64bee0af77b9414f7632f (MD5) / Made available in DSpace on 2017-09-27T13:43:20Z (GMT). No. of bitstreams: 1 felipedefreitasfonseca.pdf: 1431342 bytes, checksum: b363be3713c64bee0af77b9414f7632f (MD5) Previous issue date: 2017 / A conjuntura nacional pós anos 2000 se apresenta como momento de reorganização e rearticulação das organizações dos trabalhadores, notadamente no campo sindical. A CUT, que surge com o “novo sindicalismo” no final dos 1970 e que cumpriu importante papel na mobilização e organização trabalhadores numa perspectiva sindical crítica, classista e autônoma passa a evidenciar, já na década de 1990, transformações em suas práticas, concepções e políticas na direção da conciliação de classes e de um sindicalismo cidadão. Os grupos internos contrários a este descenso político e ideológico posto pela direção majoritária da Central concluem o processo de ruptura interna no primeiro governo petista, no qual o se evidencia, com força, os elementos conciliatórios e governistas nas ações da CUT. É neste contexto que surge, em 2004, uma Coordenação Nacional de Lutas que resultou, posteriormente, na consolidação da Central Sindical e Popular - CSP-Conlutas, cujo um dos principais objetivos é apresentar uma nova concepção de organização e atuação de Central, de modo a atuar, também, junto aos movimentos sociais dos trabalhadores para além do campo sindical. É esta concepção de Central que será o foco da nossa análise neste trabalho. Nosso objetivo é apreender a dinâmica de incorporação dos movimentos populares (urbanos e rurais) e de luta contra as opressões, inédita em uma Central Sindical nacional, avaliando suas características, suas agendas de lutas e seus rebatimentos na construção das ações político-interventivas da CSP-Conlutas. / The national conjuncture after the years 2000 presents itself as a moment of reorganization and rearticulation of workers' organizations, especially in the trade union field. The CUT, which emerged with the "new syndicalism" in the late 1970s and which fulfilled an important role in the mobilization and organization of workers in a critical, classist and autonomous trade union perspective began to show, as early as the 1990s, transformations in their practices, conceptions and Policies in the direction of class reconciliation and citizen unionism. The internal groups opposed to this political and ideological descent by the majority direction of the Central conclude the process of internal rupture in the first PT government, in which the conciliatory and governmental elements in the actions of the CUT are strongly evidenced. It is in this context that a National Coordination of Struggles emerged in 2004 that resulted in the consolidation of the CSP-Conlutas, one of the main objectives of which is to present a new conception of Central organization and To act, also, with the social movements of the workers beyond the trade union field. It is this conception of Central that will be the focus of our analysis in this work. Our aim is to understand the dynamics of incorporation of popular movements (urban and rural) and struggle against oppression, unprecedented in a national trade union center, evaluating its characteristics, its agendas of struggles and its refutations in the construction of political-intervention actions of CSP -Conlutas.

La modélisation et la résolution de problèmes sous contraintes constituent un domaine majeur enIA. Par la nature diverse des contraintes, différents formalismes de représentation ont été proposés pour les exprimer de manière simple et compacte tout en garantissant une efficacité des outils de résolutions associés. Les formules propositionnelles, les réseaux de contraintes discrets (RCD) et qualitatives (RCQ) sont des cadres de modélisation répondant à ces critères. Pour les informations temporelles ou spatiales, les RCQ constituent un modèle de choix avec de nombreuses applications comme l’ordonnancement de tâches, la planification temporelle ou spatiale, les systèmes d’informations géographiques. Nos contributions visent à étudier les liens des RCQ vers les RCD et les formules propositionnelles, afin d’adapter les outils issus des divers domaines et de proposer de nouvelles approches. Tout d’abord, nous nous concentrons sur l’aspect structurel des RCQ, en adaptant la méthode de la composition faible dans les différents cadres. Nous exploitons ensuite les propriétés des classes traitables de certains formalismes qualitatifs, afin de définir une transformation vers la logique propositionnelle. En exploitant la transformation vers les RCD, nous proposons une méthode incomplète facilitant la preuve de l’incohérence des RCQ par la relaxation de la propriété de composition faible, puis nous complétons l’approche en exploitant les classes traitables. Enfin, ces études nous conduisent à proposer une nouvelle forme de substituabilité locale, dont les détections statique et dynamique permettent d’obtenir une amélioration algorithmique dans le cadre des RCD. / Modelling and solving constraints problems is a major domain in Artificial Intelligence. By the various natures of the constraints, different formalisms were proposed to express them in a simple andcompact way while guaranteeing the effectiveness of the associated solution tools. Propositional formulae, discrete constraint networks (DCNs), and qualitative constraint networks (QCNs) are the well known frameworks that guaranty these requirements. For temporal or space information, QCNs constitute a model of choice with many real world applications such as scheduling, temporal or spatial planning and geographic information systems. Our contributions aim at studying the links between QCNs, DCNs and propositional formulas, in order to adapt the tools developed in these fields and to propose new approaches. First of all, we focus on the structural aspects of QCNs, by transforming weak composition within the various frameworks. In order to define a transformation towards propositional logic we then exploit the properties of tractable classes of some qualitative formalism. Exploiting the transformation towards DCNs, we propose an incomplete method simplifying the proof of the inconsistency for QCNs by relaxing the weak composition property. Then, we propose a complete approach thanks to tractable classes. Finally, these studies lead us to propose a new form of local substitutability, whose static and dynamic detections significantly improve search algorithms for DCNs.

In recent years power generation from renewable energy has grown substantially both in South Africa and around the world. This growth is set to continue as there is more pressure to reduce the burning of fossil fuels. However, renewable energy power generation suffers from unpredictability, which causes problems when it comes to managing power grids. Concentrated Solar Power (CSP) plants offer a practical solution to store power in the form of thermal energy storage (TES). Thus, the plant can run when there is no solar energy available, leading to a more stable power supply. Unfortunately, CSP plants cost more than other renewables such as photovoltaic and wind power. Thus, there is a need for research into how to bring down the cost of CSP plants. One of the most proven types of CSP is the parabolic trough plant. The most recent innovation is to try and use molten salt as the heat transfer fluid which would reduce the cost of the plant. However, this new technology has not been implemented on a full scale CSP plant and little testing has been done to prove the technology. The HPS2 is a test facility aimed at testing the use of molten salt as a heat transfer fluid (HTF). This test facility, located in Evora Portugal, is being developed by an international consortium led by the German DLR institute of Solar Research. It is one of the first test facilities of its kind where experiments will be conducted to demonstrate the validity of using molten salt as a HTF and a storage medium in a parabolic trough CSP plant. The HPS2 test facility is not yet operational and there is a need for a dynamic thermofluid process model to better understand and predict both its steady state and transient operational behaviour. This dissertation reports on the development of such a dynamic thermofluid process model and the results obtained from it. The process model developed primarily focuses on the steam cycle with the TES incorporated into the model. The physical geometry of each of the components are employed to construct discretized elements for which the conservation of mass, energy, and momentum are applied in a one-dimensional network approach. The economizer and evaporator combined has a helical coil geometry and uses molten salt as a heat transfer fluid, which is unique. Thus, correlations had to be adjusted for the flow characteristics found in the economizer/evaporator. Results from the steady state simulations of the steam cycle show that the molten salt mass flowrate through the steam generation system will have to be reduced from the initially expected value to meet operational requirements. Results of the dynamic simulations show that the test facility will be able to produce a constant power supply despite transient solar conditions and highlights key dynamic responses for operators to be aware of.

This project consists of three parts. The first part is aimed to summarize list of actual packaging systems and especially systems using 3D construction. Project continues in the second part, which is more practical and contains design and production of organic and inorganic testing substrates for lead-free soldered 3D structures. Last experimental part is about tests performed on soldered substrates and evaluation of results of these practical tests.

The aim of this work was the evaluation of some statistic indicators from the data obtained from the Health Informatic System Clinicom. The data used in this informatic system are administrated by the database system Caché. The data from the database which is administrated by Departement of Biomedical Engineering in Brno, have been also used. Data mentioned in this work were mined from the database by SQL queries. The statistic indicators obtained this way were needed to be presented on internet. The user interface for this presentation was designed and realized in programming language CSP. The resulting statistic indicators were split up into 3 basic groups: Hospitalization, Mandatory reporting and Medicament requirement. Besides the statistic indicators some pacients‘ data and the graphs of results are shown in the user interface. The part which has also been used in this work is the concept of the online form for reporting of cancers.