O crescimento da complexidade e do tamanho dos sistemas computacionais atuais suscitou um aumento na dificuldade de extração e especificação de modelos formais desses sistemas, tornando essa atividade cada vez mais dispendiosa, tanto em tempo quanto em custo. Modelos são utilizados em diversas técnicas da Engenharia de Software, com o intuito de auxiliar em processos que compreendem desde o desenvolvimento de novos softwares, até reconstrução de um sistema a partir de software legado, passando pela realização de manutenção de um software em operação. Portanto, é necessário que essas abstrações sejam confiáveis e representem fielmente o software real. Nesse sentido, a adoção de métodos formais para a construção e análise de modelos computacionais é crescente e motivada, principalmente, pela confiabilidade que os formalismos matemáticos agregam aos modelos. No entanto, a utilização de métodos formais geralmente demanda um alto investimento de recursos humanos e, consequentemente, financeiros, uma vez que a utilização de tais formalismos é condicionada ao estudo profundo de sua fundamentação matemática. Considerando-se a extensa aplicabilidade de modelos em diversas subáreas da Ciência da Computação e as vantagens advindas da utilização de métodos formais para especificar sistemas, é interessante identificar métodos e ferramentas existentes para automatizar os processos de extração e análises de modelos, em conjunto com a adoção de formalismos que possam ser utilizados por profissionais da computação que atuam na indústria de software. Dessa forma, é estimulada nesse trabalho a utilização do formalismo de Gramática de Grafos, um método formal que diferencia-se dos demais por ser intuitivo e possuir uma representação visual gráfica, o que facilita a sua compreensão e não exige um conhecimento avançado sobre o formalismo. Primeiramente, é proposta uma abordagem para a extração de modelos em Gramática de Grafos a partir de código-fonte, extraindo informações de execuções de código Java anotado. Em seguida, é apresentada uma metodologia existente para extração e análise de Gramática de Grafos a partir de Casos de Uso, juntamente com um estudo empírico realizado a fim de validar a metodologia. Por fim, são propostas possíveis verificações adicionais, a fim de extender as análises dessa metodologia. Com isso, busca-se a obtenção de modelos, descritos através do formalismo de grafos, a partir de artefatos criados nos dois pólos do processo de desenvolvimento de software, antes e depois da implementação, no sentido de viabilizar futuras comparações, no contexto de verificação de software. / The growing size and complexity of current computer systems leading to an increase in the difficulty of extraction and specification of formal models of such systems, making it increasingly expensive activity, both in time and in cost. Models are used in various techniques of software engineering in order to assist in processes that range from the development of new software, to rebuild a system from legacy software, passing for performing maintenance of software in operation. Therefore, it is necessary that these abstractions are reliable and faithfully represent the actual software. In this sense, the adoption of formal methods for the construction and analysis of models is growing and motivated mainly by the reliability that the mathematical formalism add to models. However, the use of formal methods generally demands a high investment in human resources and hence financial, since the use of such formalism is conditioned to the deep study of its mathematical foundation. Considering the extensive applicability of models in various subfields of computer science and the benefits arising from the use of formal methods for specifying systems, it is interesting to identify existing methods and tools to automate the process of extracting models, in addition to the adoption of formalism that can be used by computer professionals working in the software industry. Thus, we encourage the use of the Graph Grammar formalism, a formal method that differs from others because it is intuitive and has a graphical visual representation, making it easy to understand and does not require an advanced knowledge of the formalism. First, we propose an approach for extracting models from source code in Graph Grammar, getting information of executions of annotated Java code. Then an existing methodology for extraction and analysis of Graph Grammar from Use Cases is presented, along with an empirical study to validate the methodology. Finally, we propose possible additional checks in order to extend the analysis of this methodology. Thus, this work aims to extract models, described by the formalism of graphs, from artifacts created in the two poles of the software development process, before and after implementation, in order to allow future comparisons, in the context of software verification.

Conselho Nacional de Desenvolvimento CientÃfico e TecnolÃgico / A aplicaÃÃo de nuvens computacionais para oferecer serviÃos de ComputaÃÃo de Alto Desempenho (CAD) à um assunto bastante discutido no meio acadÃmico e industrial. Esta dissertaÃÃo està inserida no contexto do projeto de uma nuvem computacional para o desenvolvimento e execuÃÃo de aplicaÃÃes de CAD baseadas em componentes paralelos, doravante denominada nuvem de componentes. Um dos principais desafios na sua utilizaÃÃo consiste no suporte à programaÃÃo paralela, tarefa bastante suscetÃvel à erros, pois tais erros podem levar, ao longo do desenvolvimento, a problemas de sincronizaÃÃo de processos, que podem causar abortamento da execuÃÃo e a produÃÃo de dados incorretos, bem como a problemas relacionados ao uso ineficiente dos recursos computacionais. à importante que tais problemas sejam tratados no caso de aplicaÃÃes de longa duraÃÃo cujo respeito a um cronograma para obtenÃÃo de resultados à crÃtico, aplicaÃÃes estas bastante comuns no contexto de CAD. Uma possÃvel soluÃÃo para tais problemas consiste na verificaÃÃo do comportamento e das propriedades dos componentes na nuvem, antes que seja feita a sua execuÃÃo, tornando possÃvel que os usuÃrios dos componentes da nuvem saibam se um componente pode ser utilizado com seguranÃa em sua aplicaÃÃo. Nesse cenÃrio, o uso de mÃtodos formais surge como uma alternativa atraente. A contribuiÃÃo desta dissertaÃÃo consiste em um processo de derivaÃÃo e verificaÃÃo de propriedades de componentes na nuvem. Tal processo envolve a especificaÃÃo formal do comportamento dos componentes por meio de contratos descritos pela linguagem Circus. EntÃo, atravÃs de um processo de refinamento e traduÃÃo tendo como ponto de partida o contrato, chega-se à implementaÃÃo de um componente para execuÃÃo sobre uma plataforma de computaÃÃo paralela. AtravÃs desse processo, torna-se possÃvel oferecer garantias aos desenvolvedores em relaÃÃo ao comportamento dos componentes no contexto de suas aplicaÃÃes. Para a prova de conceito, o processo à aplicado sobre a especificaÃÃo "papel-e-caneta" de dois benchmarks do NAS Parallel Benchmarks, IS e CG, bastante difundidos na Ãrea de CAD. / The use of cloud computing to offer High Performance Computing (HPC) services has been widely discussed in the academia and industry. In this respect, this dissertation is included in the context of designing a cloud computing platform for the development of component-based parallel computing applications, referred as cloud of components. Many important challenges about using the cloud of components relate to parallel programming, an error-prone task due to synchronization issues, which may lead to abortion and production of incorrect data during execution of applications, and the inefficient use of computational resources. These problems may be very relevant in the case of long running applications with tight timelines to obtain critical results, quite common in the context of HPC. One possible solution to these problems is the formal analysis of the behavior of the components of an application through the cloud services, before their execution. Thus, the users of the components may know if a component can be safely used in their application. In this scenario, formal methods becomes useful. In this dissertation, it is proposed a process for specification and derivation of parallel components implementation for the cloud of components. This process involves the formal specification of the components behavior through contracts described using the Circus formal specification language. Then, through a refinement and translation process, which takes the contract as a start point, one may produce an implementation of a component that may execute on a parallel computing platform. Through this process, it becomes possible to offer guarantees to developers about the components behavior in their applications. To validate the proposed idea, the process is applied to contracts that have been described based on two benchmarks belonging to the NAS Parallel Benchmarks, widely adopted in HPC for evaluate the performance of parallel programming and computing platforms.

É possível rir da ciência? Qual seria a relação entre o cômico e a ciência? Onde está o humor na ciência? No âmbito do ensino, os alunos riem das piadas com física? É preciso entender ou saber conceitos de física para entender a piada? É pensando nestas questões que articulamos a presente pesquisa, que visa estudar a relação entre o humor e a ciência e suas implicações didáticas. Para tanto, iniciamos nossa pesquisa a partir de um estudo das teorias sobre o humor e sua evolução ao longo da história, seguida de um levantamento de obras, tais como: O Guia do Mochileiro das Galáxias de Douglas Adams, As cosmicômicas de Italo Calvino, tiras e charges, entre outras, nas quais enxergamos uma aproximação entre ciência e humor. Com a base teórica, investigamos os resultados de intervenções didáticas nas quais foram utilizados materiais midiáticos pesquisados. Para a elaboração e realização das atividades e da pesquisa, nós nos apoiamos em uma metodologia que engloba três etapas: análise, formulação e aplicação/intervenção. Em que na primeira, o material é estudado, em seguida é realizada a produção de uma proposta de atividades, que, por fim, é realizada em um espaço educacional, seja ele formal ou não. No presente trabalho, a investigação foi realizada em dois momentos distintos. O primeiro envolvendo estudantes do ensino superior, tanto da Escola de Artes Ciências e Humanidades da Universidade de São Paulo, quanto da Universidade Júlio de Mesquita Filho - UNESP, Campus Rio Claro, e no segundo com alunos do ensino fundamental II, no âmbito do projeto Banca da Ciência na Escola. Como resultado, concluímos que, no geral, a relação entre humor e ciência se encontra fora da ciência, e relacionada com outros conteúdos. Pudemos observar que, de fato, há uma estreita relação entre o riso e a compreensão de um conteúdo científico, e, que o humor, devido a sua aproximação com o lúdico, possibilita, e necessita, um espaço dinâmico para a sua utilização. Portanto, o humor apresenta um papel importante tanto no processo de ensino-aprendizagem quanto no engajamento à ciência. / Is it possible to laugh from Science? What would it be the relationship between something funny and science? Where is the humor on science? On the scope of teaching, do the students laugh from physics puns? Is it necessary to understand or to know physics concepts to \"get\" the joke? It is thinking on these questions that we have articulated this current research, that aims to study the relationship between humor and science, and its didactical implications. To do so, we started this research studying the humors theories and its evolution trough history, followed by a study of media works, such as Douglas Adams\' Hitchhiker\'s Guide to the Galaxy, Italo Calvino\'s Cosmicomics, comic stripes, among others, on which we saw an approximation of science and humor. With this theoretical background, we have investigated the outcomes of didactical interventions on which the works researched were used. For the elaboration and realization of the activities and the research, we supported a methodology that can be divided in three steps, analysis, elaboration and intervention. On the first step, the work its studied, on the second step one intervention its elaborated, and, on the third step, the intervention takes place on an education environment, be it formal or nonformal. On the current work, the investigation was performed on two different moments. The first involving students from undergraduate courses, such as Escola de Artes, Ciências e Humanidades da Universidade de São Paulo, and, Universidade Júlio de Mesquita Filho - UNESP, Campus Rio Claro, and on the second moment, with students from secondary education on the project Science stand at school. As results, we have concluded that, in general, the relation between humor and science can be found outside the science, and related with others subjects. We could also observe that, indeed, there is a strait relationship among laugh and the comprehension of a scientific content, and, that the humor, due its proximity with ludic activities, allows, and requires, a dynamical space for its use. Therefore, the humor has an important role in teaching and learning process an in the engagement of science

A integração estruturada e consistente de diversas especificações (ou visões) de um sistema é hoje uma questão essencial na moderna abordagem para especificação e desenvolvimento de software. Neste contexto, precisamos de uma teoria que fale sobre formalismos de especificação e que ao mesmo tempo nos ofereça conceitos e construções para estabelecer-mos relações entre eles. Com este trabalho temos o objetivo de discutir noções rigorosas para idéia de lógica, técnicas fundamentais para relacioná-Ias e mostrar a utilização destes concei¬tos para abordar a questão da interoperabilidade formal, especialmente de provas. Como formalização para idéia de lógica utilizaremos as Instituições de Goguen & Burstall e a extensão de Meseguer para General Logics. Como técnica para rela¬cionar lógicas trabalharemos com os mapeamentos Plain e Simples de Meseguer. Atenção especial é dada à discussão das propriedades destes mapeamentos com vis¬ta à reutilização de componentes lógicos, especialmente da relação de consequência entre fórmulas. Contribuições desta dissertação incluem um tratamento acessível para os con¬ceitos fundamentais necessários para estudar lógicas e sua integração, uma expo¬sição uniforme e detalhada de uma família de sistemas lógicos e uma apresentação categórica desta integração via mapeamentos. / The integration in a sound and structured way of several specifications (or views) of a system is a key research area in (modern) software specification and development. In this context, we need a theory to speak not only about specification logics, but also one that can offer us concepts and constructions to establish relations between these formalisms. In this work we have the purpose of discussing rigorous notions for the idea of logic, presenting fundamental techniques to relate them, and introducing important constructions to approach the problem of formal interoperability, most notably of proofs. As a formalization of the informal idea of a logical system, we use Goguen & Burstall's concept of Institutions and Meseguer's further extension to General Logics. Meseguer's Plain and Simple Maps of Institutions are the tools we use to relate and map logics. Besides, special attention is given for the discussion of the essential properties of these maps concerning the borrowing of logical components, specially of consequence relations. Contributions of this thesis include a smooth presentation of fundamental techniques to study and relate logics, an uniform and detailed exposition of a num¬ber of logical systems, and a categorical formalization of relations between these formalisms by way of maps between institutions.

Made available in DSpace on 2014-06-12T15:52:29Z (GMT). No. of bitstreams: 2 arquivo5034_1.pdf: 809628 bytes, checksum: 2ff554a299db1e14396d8f0d82fa4d3d (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2007 / O processo de formalização da ciência política, ocorrido principalmente na segunda metade do século XX, ainda encontra resistência de largas parcelas da comunidade científica dessa área de estudos. O objetivo deste trabalho é expor a utilização da teoria dos jogos (TJ), principal ferramenta metodológica de formalização da ciência política, na produção recente em diversas áreas da ciência política. O período analisado é 2000-2006, com análises sobre nove artigos coletados de periódicos de grande circulação internacional na área da ciência política, como o American Political Science Review, o Journal of Conflict Resolution, British Journal of Political Science e o American Journal of Politics. Os artigos foram concentrados em três áreas principais: Relações Internacionais, Análise Institucional e Estudos Legislativos. Neste trabalho não apenas exponho a multiplicidade de aplicações da TJ na ciência política como também teço considerações acerca dos seus limites explicativos e possibilidades de novas percepções acerca dos eventos estudados. As bases do meu argumento sobre vantagens e desvantagens no uso da TJ estão na sua versatilidade, na interdisciplinaridade crescente da ciência política e no individualismo metodológico

Made available in DSpace on 2014-06-12T15:56:13Z (GMT). No. of bitstreams: 2 arquivo2770_1.pdf: 3435334 bytes, checksum: c4ebc011cd6476e268421539acd59c8c (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Associação para Promoção da Excelência do Software Brasileiro / O gerenciamento e o projeto de sistemas de engenharia complexos é um desafio interessante. A engenharia de sistemas é um campo interdisciplinar da engenharia focado na melhoria da qualidade de projetos de sistemas. Ela encoraja o uso de métodos e ferramentas como simulação, otimização, análise de confiabilidade e análise estatística para aumentar o conhecimento do sistema, frequentemente representado como um conjunto de modelos. Uma enorme variedade de sistemas dinâmicos precisa ser controlada e pode ser modelada usando os princípios da Teoria de Controle, a base da disciplina de engenharia de controle. Em particular, a engenharia de controle objetiva criar leis de controle para o sistema, que são modeladas usando diagramas de bloco (também chamados de diagramas de leis de controle) e validadas/verificadas usando simulação. Entretanto, a maior parte das validações de leis de controle realizadas na indústria é feita usando ferramentas de simulação como o Simulink, e simulações não cobrem todos os comportamentos do modelo. Além disso, não é fácil modelar uma arquitetura complexa na qual redundância e monitoramento são comumente usados para se obter segurança. Neste trabalho, nós apresentamos três principais contribuições: (1) um conjunto de regras de tradução de modelos Simulink para a algebra de processos CSP (Communicating Sequential Processes), incluindo uma infraestrutura para suportar vários blocos discretos de Simulink; (2) uma estratégia para validar a integração de uma proposta de arquitetura com as leis de controle; e (3) a validação de um sistema de controle de voo dos profundores de um avião produzido pela Embraer. Os resultados mostram que a estratégia pode ser aplicada a modelos complexos através do uso das técnicas formais de abstração de dados e verificação de modelos. Ademais, a estratégia proposta aprimora o processo de desenvolvimento padrão (modelo V) seguido pela indústria por encontrar potenciais defeitos em fases de especificação do projeto, reduzindo tempo de desenvolvimento e custos

Made available in DSpace on 2014-06-12T15:59:33Z (GMT). No. of bitstreams: 2 arquivo5175_1.pdf: 1994160 bytes, checksum: 29002a3ad03ec142019fe6f3747721fb (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2004 / O desenvolvimento de aplica¸c oes baseado em frameworks tem sido apontado como o pr´oximo passo em dire¸c ao a um maior reuso de software. O reuso atrav´es da composi¸c ao de dois frameworks, e n ao apenas atrav´es de extens oes de classes de um ´unico framework, tornou-se uma necessidade gerada pelo aumento da complexidade de desenvolvimento de sistemas computacionais. Neste sentido, tornam-se necess´arias novas t´ecnicas de documenta¸c ao ou especifica¸c ao de frameworks que eliminem imprecis oes e ambig¨uidades nas descri¸c oes dos seus comportamentos. Este trabalho apresenta uma estrat´egia de composi¸c ao de frameworks que utiliza linguagens de especifica¸c ao formal para descrever seus comportamentos e estruturas de dados. As linguagens utilizadas s ao CSP, Z e CSP-Z. Por tratar da composi¸c ao no n´ıvel das especifica¸c oes formais, a estrat´egia consegue abstrair detalhes de implementa¸c ao e eliminar restri¸c oes ligadas a estes detalhes. Al´em disso, a abordagem formal permite a verifica¸c ao, atrav´es do verificador de modelos de CSP, FDR, da manuten¸c ao das propriedades dos frameworks originais. O objetivo principal da estrat´egia ´e a composi¸c ao de fluxos de controle, que ´e um dos problemas mais comuns da composi¸c ao de frameworks. N´os apresentamos as causas e poss´ıveis solu¸c oes deste e dos demais problemas da composi¸c ao de frameworks. Por fim, mostramos que a estrat´egia aborda todos os problemas listados em menor ou maior grau. A estrat´egia pretende realizar a comunica¸c ao entre os frameworks atrav´es de um casamento entre os eventos e tipos de dados correspondentes dos dois frameworks. A composi¸c ao ´e realizada atrav´es de um terceiro componente, o componente de sincroniza¸c ao e comunica¸c ao (CSC). A ado¸c ao deste componente possibilita maior flexibilidade `a composi¸c ao e, entre outros benef´ıcios, permite que os frameworks se comuniquem de forma an onima e elimina efeitos colaterais nos seus comportamentos. A estrat´egia tem todos os seus pontos especificados num n´ıvel de detalhe que facilitar´a uma futura mecaniza¸c ao. Neste sentido, s ao apresentados modelos para a especifica¸c ao do CSC e uma abordagem construtiva para a sua gera¸c ao

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

Orientador: Arnaldo Vieira Moura / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-16T20:14:05Z (GMT). No. of bitstreams: 1 Cabral_GlauberModolo_M.pdf: 1025512 bytes, checksum: 7aaf4d32142384e7200596499be77cca (MD5) Previous issue date: 2010 / Resumo: Métodos formais são ferramentas da Engenharia de Software que empregam formalismos matemáticos na construção de programas. Em geral, são compostos por uma ou mais linguagens de especificação e algumas ferramentas auxiliares. A linguagem de especificação algébrica Common Algebraic Specification Language (Casl) foi concebida para ser a linguagem padrão na área de especificação algébrica. A linguagem HasCasl é a extensão da linguagem Casl responsável por suportar lógica de segunda ordem e possui um subconjunto de sua sintaxe que se assemelha à linguagem de programação Haskell e que pode ser executado. O uso prático de uma linguagem de especificação depende da disponibilidade de uma biblioteca padrão de especificações pré-definidas. Embora Casl possua tal biblioteca, esta não disponibiliza propriedades e tipos de dados de segunda ordem. Esta dissertação descreve a especificação de uma biblioteca para a linguagem HasCasl com funções e tipos de dados de segunda ordem, tendo como referência a biblioteca Prelude da linguagem Haskell. Os tipos de dados especificados incluem o tipo booleano, listas, caracteres e cadeias de caracteres, além de classes e funções presentes na biblioteca Prelude. Uma primeira versão da biblioteca faz uso de tipos de dados com avaliação estrita, devido à complexidade de iniciar o processo de especificação com o uso de tipos com avaliação preguiçosa. Um refinamento posterior da biblioteca incluiu o suporte a tipos de dados com avaliação preguiçosa. A verificação de ambas as versões da biblioteca foi realizada com o uso da ferramenta Hets, responsável por traduzir as especificações escritas na linguagem HasCasl para a linguagem HOL e gerar necessidades de prova verificadas com o auxílio do provador de teoremas Isabelle. Para ilustrar o uso dos tipos de dados especificados foram incluídas algumas especificações de exemplo envolvendo listas e tipos booleanos. Algumas sugestões de extensão à biblioteca são propostas, tais como o suporte à recursão e às estruturas infinitas, além do aperfeiçoamento do suporte a provas relacionadas a especificações importadas da biblioteca da linguagem Casl / Abstract: Formal methods can be used as software engineering tools that employ mathematical formalisms for building and verifying programs. They are usually composed of one or more specification languages and some auxiliary tools. The Common Algebraic Specification Language (Casl) is designed to be the standard language in the area of algebraic specification, taking tecnical elements from other specification languages. The HasCasl language is the extention of the Casl language that is responsible for supporting secondorder logic, which has a subset of its syntax resembling the Haskell programming language. The practical use of a specification language depends on the availability of a standard library of pre-defined specifications. CASL has such a library and its specifications can be imported by specifications developed in HasCasl. However, the library of the Casl language does not provide higer order properties and data types. This dissertation describes the specification of a library for the language HasCasl based on the Prelude library from the Haskell programming language. The library created her provides second-order functions and data types. It does so by specifying data types and functions existing in Haskell language, such as boolean, list, character and string types. The first version of our library uses types with strict evaluation. The second version of the library has been refined to support types with lazy evaluation. Verification of both libraries was performed using the Hets tool, which translates specifications to the HOL language, producing proof needs that were discharged with the help of the Isabelle theorem prover. To illustrate the use of our library, some example specifications using lists and boolean types are included. Some suggestions for extension of the library are proposed, dealing with support for infinite structures and numeric data types / Mestrado / Linguagens de Programação / Mestre em Ciência da Computação