Made available in DSpace on 2014-06-12T15:52:59Z (GMT). No. of bitstreams: 2 arquivo4837_1.pdf: 1490840 bytes, checksum: 1e2239b5952d87633b8a93c565229e3e (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2004 / A reestruturação de programas no contexto da orientação a objeto é também conhecida como refactoring e consiste em mudanças na estrutura interna de um software, sem modificar seu com portamento externo, a ¯m de melhorar sua legibilidade e torn¶a-lo mais f¶acil de passar por futuras mudan»cas. Na pr¶atica, refactoring baseia-se em compila»c~ao e testes para assegurar a preserva»c~ao do comportamento. Trabalhos como os de Opdyke e Roberts foram realizados com vistas µa formaliza»c~ao de refac- torings por meio da identi¯ca»c~ao de condi»c~oes que devem ser satisfeitas para assegurar que uma mudan»ca num programa preserva o comportamento do mesmo. As condi»c~oes, geralmente escritas na linguagem do c¶alculo de predicados, s~ao introduzidas como pr¶e e p¶os-condi»c~oes dos refactor- ings. Outras abordagens para a prova de preserva»c~ao do comportamento de refactorings usam formalismos como an¶alise conceitual e reescritura de grafos. Contudo, n~ao h¶a t¶ecnica alg¶ebrica que apresente refactorings como transforma»c~oes que preservam o comportamento, com prova deste fato. Nossa principal contribui»c~ao constitui-se na apresenta»c~ao de refactorings como transforma»c~oes de programas escritos em rool (Re¯nement object-oriented Language), uma linguagem baseada em Java, com classes, controle de visibilidade, liga»c~ao din^amica, e recurs~ao. A linguagem rool permite que raciocinemos sobre programas orientados a objetos e especi¯ca»c~oes, pois a mesma une estas constru»c~oes como no c¶alculo de re¯namentos de Morgan. A sem^antica de rool ¶e baseada em weakest preconditions. Um conjunto de leis de programa»c~ao est¶a dispon¶³vel tanto para os comandos imperativos de rool quanto para construtores relacionados µa orienta»c~ao a objetos. A prova, na sem^antica de rool, de que tais leis s~ao corretas, ¶e tamb¶em uma contribui»c~ao do presente trabalho. Apresentamos refactorings como regras alg¶ebricas de re¯namento envolvendo programas. A prova da preserva»c~ao do comportamento ¶e realizada pela aplica»c~ao de leis de programa»c~ao a um lado da regra a ¯m de obtermos o lado oposto. N¶os generalizamos a t¶ecnica padr~ao de re¯namento de dados a ¯m de lidar com hierarquia de classes. Neste trabalho tamb¶em apresentamos como obter um sistema estruturado segundo um padr~ao de projeto, por meio da aplica»c~ao de regras de refactoring. Padr~oes de projeto constituem-se num objetivo natural para a realiza»c~ao de transforma»c~oes por meio da aplica»c~ao de refactorings. Trabalhos presentes na literatura sobre padr~oes de projeto que prop~oem a formaliza»c~ao dos mesmos, em geral, concentram-se em suas descri»c~oes formais, n~ao na transforma»c~ao de um sistema com vistas a estrutur¶a-lo de acordo com padr~oes de projeto. Tamb¶em apresentamos a transforma»c~ao de uma aplica»c~ao monol¶³tica para uma aplica»c~ao estruturada segundo um padr~ao arquitetural.

Made available in DSpace on 2014-06-12T15:57:28Z (GMT). No. of bitstreams: 2 arquivo3199_1.pdf: 729356 bytes, checksum: 6c269a282f3e408a30566d12c64fac0e (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / Os contratos (modelos que descrevem mais detalhadamente a arquitetura e os componentes) podem ser utilizados para a construção de softwares corretos. Esta construção pode ser realizada através do (1) cálculo de refinamento, (2) refinamento da estratégia e (3) fazendo a geração automática de código. Embora (1) e (2) são soluções corretamente comprovadas, eles requerem bastante esforço. Por outro lado, (3) é uma solução mais simples para derivação do código. No entanto, esta solução não pode fornecer um código confiável em relação aos seus contratos (ao menos que se comprove que o gerador de código é correto). Este trabalho propõe uma estratégia de testes baseados em modelos para verificar se determinado gerador de código é correto. A estratégia inicia-se com JML (linguagem baseada em contrato utilizada no Java) usando como estudo de caso o JavaCard, JMLe (um gerador de código baseado em JML) e o Jartege (gerador de testes baseados em modelos). Além disso, através deste trabalho é realizado um experimento onde é investigado o número de erros encontrados no jmle variando os valores do parâmetros do Jartege no nosso estudo de caso

Made available in DSpace on 2014-06-12T15:59:18Z (GMT). No. of bitstreams: 2 arquivo5011_1.pdf: 1099518 bytes, checksum: 29a36710d81ec239b320f6d900a43fc5 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2004 / Leis de programação são importantes tanto para definir a semântica axiomática de linguagens de programação quanto para auxiliar o processo de desenvolvimento de software. De fato, estas leis podem ser utilizadas como base para práticas informais de desenvolvimento como refactoring, que vem sendo popularizada por metodologias modernas, em especial por Extreme Programming. Embora não tenham sido suficientemente exploradas ainda, as leis de modelagem provavelmente podem trazer benefícios similares, mas com um impacto positivo maior em confiabilidade e produtividade, devido ao melhor suporte antecipado no processo de desenvolvimento de software. Em geral, transformação de modelos que preservam semântica são propostas de maneira ad hoc tendo em vista que são difíceis de serem provadas que são consistentes com respeito a semântica formal. Como consequência, pequenos equívocos podem levar a transformações que deixem o modelo inconsistente. Por estes motivos, este trabalho propõe um conjunto de leis de modelagem (que podem ser vistas como transformações de modelos bidirecionais que preservam semântica) que podem ser utilizas com segurança para se derivar leis mais complexas. Estas leis descrevem transformações de modelos em Alloy, uma linguagem formal para modelagem orientada a objetos. Além disso, será mostrada como estas leis podem ser utilizadas para refatorar especificações em Alloy. Com o intuito de se verificar a consistência das leis, foi proposta uma semântica denotacional para Alloy, utilizando a própria linguagem e uma noção de equivalência indicando quando dois modelos em Alloy possuem a mesma semântica. Por fim, o Alloy Analyzer, ferramenta utilizada para fazer análises em modelos em Alloy, foi estendida com algumas das leis básicas propostas. Como resultado, algumas diretrizes para a implementação de sistemas de transformação foram propostas

Made available in DSpace on 2014-06-12T15:59:45Z (GMT). No. of bitstreams: 2 arquivo5533_1.pdf: 1386556 bytes, checksum: dd140b25c88f8bcdd90de267c9e23d34 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2006 / O processo de avaliação de desempenho pode ser implementado através de diversos métodos: medição que é processo de coleta de informações de um sistema real; simulação computacional e modelos analíticos que capturam o comportamento temporal de um sistema através de uma representação matemática. A avaliação baseada em modelos possibilita a análise de desempenho de sistemas, antes mesmo de sua implementação, o que possibilita ajustes ainda na fase de desenvolvimento. O uso de modelos como mecanismo de avaliação também torna possível a avaliação de cenários complexos, possibilitando, portanto, a análise de desempenho em função de restrições temporais e de recursos. O interesse na avaliação de desempenho do sistema do middleware está aumentando. O CORBA é um padrão de middleware orientado a objetos definido pela OMG que permite aplicações distribuídas em uma rede (local ou mesmo na Internet) se comuniquem. O serviço de controle de concorrência (SCC) faz parte do conjunto de serviços conhecidos como serviços comuns do CORBA e são usados por várias aplicações de diversos domínios. O SCC do CORBA foi definido para coordenar o acesso a recursos compartilhados, através do uso de locks, garantindo a consistência quando o recurso é acessado concorrentemente. Este trabalho propõe modelos redes de Petri estocástica para avaliar o desempenho do SCC do CORBA. Com a finalidade de validar os modelos propostos, os resultados da avaliação das redes de Petri são comparados com as medidas obtidas no OpenORB (núcleo do CORBA). Também são apresentados cenários de desempenho que auxiliam a tomada de decisões para melhoria do desempenho do SCC do CORBA

Orientador: Arnaldo Vieira Moura / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Computação Cientifica / Made available in DSpace on 2018-08-03T17:41:22Z (GMT). No. of bitstreams: 1 Pinto_GuilhermeAlbuquerque_D.pdf: 4219537 bytes, checksum: acd92f5d71678809ad0e63efea423560 (MD5) Previous issue date: 2003 / Doutorado

Tese (livre-docencia) - Universidade Estadual de Campinas, Instituto de Matematica, Estatistica e Ciencia da Computação / Made available in DSpace on 2018-07-17T18:51:34Z (GMT). No. of bitstreams: 1 Sette_AntonioMarioAntunes_LD.pdf: 1761459 bytes, checksum: 62b3e9a87a15d8cd1cf6b2ba968fc4ac (MD5) Previous issue date: 1983 / Resumo: Não informado. / Abstract: Not informed. / Tese (livre-docencia) - Univer / Livre-Docente em Matematica

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

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2017-08-08T13:40:24Z No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) Dissertação-Transformando-modelos-xscade-em-SCR-Kamila-Serafim.pdf: 1127362 bytes, checksum: cb72514ffcaf617a6573ea197ab446c1 (MD5) / Made available in DSpace on 2017-08-08T13:40:24Z (GMT). No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) Dissertação-Transformando-modelos-xscade-em-SCR-Kamila-Serafim.pdf: 1127362 bytes, checksum: cb72514ffcaf617a6573ea197ab446c1 (MD5) Previous issue date: 2016-09-08 / A construção de um software para domínios particulares tem de atender normas específicasque impõem o atendimento a fatores como rastreabilidade de requisitos e certificação. Por exemplo, a indústria aeronáutica deve atender à norma DO-178B que estabelece restrições para uso de software de aeronaves, que são considerados sistemas críticos. Para um sistema estar de acordo com essa certificação é necessário ter requisitos formais e código certificado; nesta direção, Andrade (ANDRADE, 2013) usou a notação SCR (Software Cost Reduction) para definição de requisitos e a ferramenta SCADE para modelagem de sistemas críticos, com desenvolvimento de um tradutor de SCR para artefatos xscade. A prática de desenvolvimento de sistema, porém, não está restrita à transição entre requisitos e artefatos de projeto. Modificações realizadas nestes últimos devem também ser refletidas nos requisitos. Neste trabalho desenvolvemos um tradutor de artefatos de modelagem da ferramenta SCADE para SCR. Desta forma podemos gerar especificação de requisitos a partir do código (Engenharia Reversa) e complementamos o trabalho anterior desenvolvido por Andrade (ANDRADE, 2013). Para o desenvolvimento do tradutor, utilizamos a plataforma Spoofax por meio da qual descrevemos a sintaxe do esquema XML utilizado em SCADE e também as regras de tradução tendo como alvo SCR. A validação da tradução teve como ponto de partida o resultado do uso do tradutor desenvolvido por Andrade (ANDRADE, 2013), tendo de gerar como saída a mesma entrada do tradutor desenvolvido por Andrade (ANDRADE, 2013). Além disso, desenvolvemos exemplos para demonstrar que a modificação estrutural, com preservação de semântica, em projetos SCADE, é verificável por meio do uso de testes gerados por meio da ferramenta TTM-TVEC / Building a software for particular domains must attend specific standards that impose attendance to factors such as traceability requirements and the certification issue. For example, the airline industry should meet the DO-178B standard that establishes restrictions on the use of aircraft software, which is considered a critical system. For a system to be in accordance with this certification, one must have formal requirements and certified code. In this direction, Andrade (ANDRADE, 2013) used SCR (Software Cost Reduction) for requirements definition and SCADE for modeling critical systems with development of an artifacts a translator from SCR. However the practice of developing is not restricted to the transition from requirements to design artifacts. Changes made on design should be reflected in the requirements. In this work we developed a translator from SCADE to SCR. In this way we can generate requirements specification from the code (reverse engineering) and complement the previous Andrade (ANDRADE, 2013) thesis. For the translator development, we use the Spoofax platform through which we describe the XML schema syntax used in SCADE and also the translation rules having SCR as the target language. The translation validation had as its starting point the result of the translator developed by Andrade (ANDRADE, 2013), where the output is the same input developed by Andrade(ANDRADE, 2013). Furthermore, examples developed to demonstrate that the structural modification that preserves semantics in SCADE, is verifiable through the use of tests generated by the TTM-TVEC tool.

Submitted by DHARA CARLESSO ZAMPIVA (dhara.zampiva@univates.br) on 2018-08-07T17:52:31Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) 2018KatianeVargensdeOliveira.pdf: 3874079 bytes, checksum: 330944a2a62ef5ee20b39bc547f749b9 (MD5) / Rejected by Ana Paula Lisboa Monteiro (monteiro@univates.br), reason: Inserir o Lattes do autor. on 2018-09-11T18:20:51Z (GMT) / Submitted by DHARA CARLESSO ZAMPIVA (dhara.zampiva@univates.br) on 2018-09-17T17:08:07Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) 2018KatianeVargensdeOliveira.pdf: 3874079 bytes, checksum: 330944a2a62ef5ee20b39bc547f749b9 (MD5) / Approved for entry into archive by Ana Paula Lisboa Monteiro (monteiro@univates.br) on 2018-10-02T18:43:51Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) 2018KatianeVargensdeOliveira.pdf: 3874079 bytes, checksum: 330944a2a62ef5ee20b39bc547f749b9 (MD5) / Made available in DSpace on 2018-10-02T18:43:51Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) 2018KatianeVargensdeOliveira.pdf: 3874079 bytes, checksum: 330944a2a62ef5ee20b39bc547f749b9 (MD5) Previous issue date: 2018-08-07 / O objetivo deste estudo foi compreender como as vivências possibilitadas pela Associação de Mulheres “Cantinho da Amazônia” (AMCA) contribuem para o empoderamento das mulheres pertencentes ao projeto. Trata-se de uma investigação que revela a importância dos espaços não formais de aprendizagem para a formação humana, especialmente no que concerne ao empoderamento feminino. A investigação ocorreu na AMCA com base na pesquisa qualitativa (BOGDAN; BIKLEN 1994). Os instrumentos de coleta de dados utilizados foram dois grupos focais com nove associadas e a análise de documentos da associação como: atas, reportagens, fotografias e livretos. A revisão teórica acerca das aprendizagens em espaços não formais, sob a perspectiva do empoderamento feminino, foi determinante para o estabelecimento do contraponto entre essas teorias e o fazer concreto. Por fim, apresenta-se algumas (in) compreensões do que foi possível vivenciar no decorrer da pesquisa. Serão encontradas nesse estudo razões significativas que apontam para a necessidade de se promover cada vez mais espaços como este pesquisado, a fim de alavancar o empoderamento feminino e, assim, efetivar uma sociedade com equidade de gênero e social, uma vez que a AMCA é um espaço onde há interlocução de vozes femininas que se aproximam, solidarizam-se, compartilham alegrias e problemas cotidianos em um processo de fortalecimento mútuo. As ações da AMCA por si só não levam ao empoderamento, contudo, elas possibilitam momentos que podem ser pontes para que os sujeitos desenvolvam habilidades para adquirirem o empoderamento. Os processos de aprendizagem encadeados nesse espaço possibilitam avanços progressivos político-psicológicos que impulsionaram mudanças na vida social das associadas. Os processos educativos desenvolvidos na AMCA não se desenvolvem apenas nas vivências diárias, mas também na participação de encontros, feiras, oficinas, projetos sociais, capacitações. São oportunizados conhecimentos às mulheres para se qualificarem profissionalmente, tanto no aperfeiçoamento como na aquisição de novas técnicas e aptidões. A AMCA é a uma das poucas opções de trabalho remunerado para as mulheres do assentamento “Vale do Amanhecer”, tampouco há políticas públicas na região que qualifiquem especificamente as mulheres para o mundo do trabalho. Nessa direção, importante se faz refletir sobre a necessidade de constituir novas práticas e ampliar a reflexão sobre os caminhos das políticas públicas com o objetivo de qualificar as mulheres profissionalmente. / The objective of this study was to understand how the experiences made possible by the Association of Women "Cantinho da Amazônia" (AMCA) contribute to the empowerment of women belonging to the project. It is an investigation that reveals the importance of non-formal learning spaces for human formation, especially with regard to female empowerment. The data collection instruments used were: two focal groups with nine associates and the analysis of association documents such as minutes, reports, photographs. The research was carried out at the AMCA based on qualitative research (BOGDAN; BIKLEN 1994). The theoretical review of learning in non-formal spaces from the perspective of female empowerment was decisive for the establishment of the counterpoint between these theories and the concrete and thinking. Finally, I present some (in) understandings of what was possible to experience in the course of the research. We will find in this study, significant reasons that point to the need to promote more and more spaces like this one, in order to leverage female empowerment and thus effect a society with gender and social equity, since AMCA is a space where there is interlocution of female voices that approach, solidarity, share joys and daily problems in a process of mutual strengthening. AMCA actions alone do not lead to empowerment, however, they do provide opportunities that can be bridges for individuals to develop skills to gain empowerment. The learning processes chained in the AMCA allow for progressive political-psychological advances that have led to changes in the social life of the members. The educational processes developed in the AMCA are not only developed in daily life, but also in the participation of meetings, fairs, workshops, social projects, courses of short duration. Knowledge is given to women to qualify professionally, both in terms of improvement and acquisition of new skills and techniques. AMCA is one of the few paid employment options for women in the Valley of the Dawn settlement, nor is there any public policy in the region that specifically qualifies women for the world of work. In this direction, it is important to reflect on the need to establish new practices and broaden the reflection on the paths of public policies in order to qualify women professionally.

Submitted by Kleber Silva (kleberbs@ufba.br) on 2017-02-06T17:13:39Z No. of bitstreams: 1 Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Approved for entry into archive by Vanessa Reis (vanessa.jamile@ufba.br) on 2017-02-07T12:02:49Z (GMT) No. of bitstreams: 1 Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Made available in DSpace on 2017-02-07T12:02:49Z (GMT). No. of bitstreams: 1 Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Os Agentes Autônomos – AA e os Sistemas Multiagentes – SMA realizam suas tarefas baseados num planejamento e a sua complexidade vai depender de qual ambiente esteja envolvido, principalmente quando este ambiente é dinâmico e não determinista. A verificação de modelos tem sido aplicada para a verificação de propriedades do planejamento de modo a checar a correção de aplicações baseadas em AAs e SMA’s e tal verificação apresenta muitos desafios para contornar situações potenciais de explosão de estados. O futebol de robôs simulados é uma aplicação que apresenta muitas das características e problemas inerentes aos AA’s e SMA’s como um ambiente não determinista e dinâmico, fato este que vem tornando esta aplicação um relevante estudo de caso para a verificação de modelos de SMA’s. O presente trabalho considera a especificação e verificação de planos de um time de futebol de robôs simulado, o qual é baseado na arquitetura multicamada de Agentes Concorrentes(camada cognitiva, camada instintiva, e camada reativa), utilizando o verificador de modelos UPPAAL. Para atingir os objetivos do trabalho foi proposta uma abordagem incremental e evolutiva para modelar e verificar os planos, a qual inclui abstrações e técnicas baseadas em verificação composicional de modelos (Compositional Model Checking), com o objetivo de contornar situações de explosão de estados. O método proposto também pode ser utilizado em aplicações similares, o qual poderia ser suportado por um ambiente computacional interativo para guiar os analistas no processo de verificação de planos de SMA’s com arquitetura multicamada, usando a verificação de modelos.