Entre as principais dificuldades do desenvolvimento de software embarcado crítico e de tempo real está a especificação e o processo de verificação e validação apoiado ao projeto conceitual. Neste contexto, a modelagem de sistemas tem uma importante função, uma vez que um processo complexo possa ser analisado e validado antes de sua real implementação. Esta dissertação aborda o problema de verificação e validação de software embarcado de um satélite com configuração ACDH (Attitude Control and Data Handling) através de uma plataforma aerosuspensa com um grau de liberdade, utilizando a SysML, a ferramenta CASE TELELOGIC Rhapsody e a orientação das normas da ECSS (European Cooperation on Space Standardization). A partir do modelo obtido, são utilizadas três abordagens para análise e avaliação: (1) Especificação e gerenciamento dos requisitos, através dos conceitos determinados pela ECSS; (2) Modelagem do sistema e verificação dos requisitos, através do formalismo matemático dos autômatos utilizando a técnica de model checking através da ferramenta UPPAL; (3) Conversão do modelo em SysML, aplicando a Engenharia de Requisitos e o processo de verificação e validação do sistema, através da simulação na ferramenta CASE.

Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário. / Formal specifications are useful for describing what a system should do, without defining how, and, owing to its formal nature, it is possible to analyse them systematically. However useful formal specifications are, their usage as part of the software development process is rather rare. This is, in part, due to the scarcity of both methodologies and tools that support this development. The first goal of this work is to define a software development methodology that enables the developer to produce a Java application from a formal specification written in Z. This methodology will rely strongly on the generation of Java application skeletons and instrumentation of the generated code with means of verifying conditions (invariants, pre and post-conditions) e tracing violations of these conditions. Through this mechanisms, it is possible to mix formal and informal development in the global software development process. The second goal of this work is to develop a tool that will implement part of this methodology, producing a partial implementation that must be complemented by the developer.

Uma das principais responsabilidades da área de Engenharia de Requisitos é refinar requisitos em especificações. Em sistemas empresariais esse refinamento deve considerar o contexto empresarial no qual o sistema fará parte. Apesar de existirem algumas abordagens para refinar requisitos algumas delas até mesmo considerando o contexto empresarial essa tarefa é realizada manualmente. Baseado em conceitos de Engenharia Dirigida por Modelos, este trabalho propõe uma transformação semiautomática usando um modelo da empresa como modelo dos requisitos e um modelo de casos de uso como modelo das especificações. Para isso, considera-se que ao usar um modelo de empresa como origem dessa transformação é possível representar tanto os requisitos quanto os conhecimentos de domínio necessários para obter especificações através de uma transformação. Com isso, este trabalho apresenta os metamodelos de origem e de destino, um conjunto de regras de transformação e uma ferramenta que permite executar a transformação. Por fim, este trabalho também discute um experimento que foi executado para analisar alguns aspectos desta proposta. / One of the key responsibilities of Requirements Engineering is to refine requirements into specifications. For enterprise systems, this refinement must consider the enterprise context where the system will be deployed. Although there are some approaches for requirements refinement, some of them even considering the enterprise context, this task is executed manually. Based on Model-Driven Engineering concepts, this study proposes a semi-automatic transformation using an enterprise model as a requirements model and a use case model as a specifications model. For that, this work considers that using an enterprise model as a source it is possible to represent both the requirements and the domain knowledge that are necessary to obtain specifications through a transformation. Therefore, this study presents the source and target meta-models, a set of transformation rules, and a tool to support the transformation. Finally, this study also discusses an experiment executed to analyze some aspects of this proposal.

Uma das principais responsabilidades da área de Engenharia de Requisitos é refinar requisitos em especificações. Em sistemas empresariais esse refinamento deve considerar o contexto empresarial no qual o sistema fará parte. Apesar de existirem algumas abordagens para refinar requisitos algumas delas até mesmo considerando o contexto empresarial essa tarefa é realizada manualmente. Baseado em conceitos de Engenharia Dirigida por Modelos, este trabalho propõe uma transformação semiautomática usando um modelo da empresa como modelo dos requisitos e um modelo de casos de uso como modelo das especificações. Para isso, considera-se que ao usar um modelo de empresa como origem dessa transformação é possível representar tanto os requisitos quanto os conhecimentos de domínio necessários para obter especificações através de uma transformação. Com isso, este trabalho apresenta os metamodelos de origem e de destino, um conjunto de regras de transformação e uma ferramenta que permite executar a transformação. Por fim, este trabalho também discute um experimento que foi executado para analisar alguns aspectos desta proposta. / One of the key responsibilities of Requirements Engineering is to refine requirements into specifications. For enterprise systems, this refinement must consider the enterprise context where the system will be deployed. Although there are some approaches for requirements refinement, some of them even considering the enterprise context, this task is executed manually. Based on Model-Driven Engineering concepts, this study proposes a semi-automatic transformation using an enterprise model as a requirements model and a use case model as a specifications model. For that, this work considers that using an enterprise model as a source it is possible to represent both the requirements and the domain knowledge that are necessary to obtain specifications through a transformation. Therefore, this study presents the source and target meta-models, a set of transformation rules, and a tool to support the transformation. Finally, this study also discusses an experiment executed to analyze some aspects of this proposal.

In this work, we study the set X ̇(φ,f) of points such that the Birkhoff averages do not exist. Following Thompson, our main result here is to show that the topological pressure of X ̇(φ,f) is total. As corollary, we get the some result for the Oseledets Irregular set for Lyapunov exponent in one dimension. For higher dimensions, this question is still open. / Conselho Nacional de Desenvolvimento Científico e Tecnológico / Neste trabalho, estudamos o conjunto X ̇(φ,f) de pontos tal que as médias de Birkhoff não existe. Seguindo Thompson, nosso resultado principal aqui é mostrar que a pressão topológica de X ̇(φ,f) é total. Como corolário, damos o mesmo resultado para o conjunto Irregular de Oseledets para os expoentes de Lyapunov em dimensão um. Para dimensões maiores, esta questão está em aberto.

Grid computing has been defined as an infrastructure integrator of distributed resources. Although it is already used on a large scale in many areas, this type of computational infrastructure is still an area of active research, with many open questions. Today, new research works investigate the application of resources virtualization techniques to perform the composition of virtual grids. These grids can be defined as a high level abstraction of resources (computing and network), through which users have a view of a wide range of interconnected computers, that can be selected and virtually organized. In a virtual grid, as well in a real grid, users and middleware must have tools that allow the composition and management of the infrastructure. Among these tools, there are languages for resource description that allow the specification of components that will be used in the infrastructure. In a virtualized environment, the resources descriptions languages should offer attributes that interact with some peculiarities, such as the possibility of allocate multiple virtual resources (computing and network) on the same physical resource. In this context, this work presents VXDL, a language developed for the interconnections and resources description in virtual grids. The innovations proposed in VXDL allow the description, classification and parameter specification of all desirable components, including network topology and virtual routers. VXDL also allow the specification of a execution timeline, which can assist grid middleware in the tasks of resources sharing and scheduling. To evaluate the proposed language, this work presentes I) a comparative study between VXDL and other resources description languages and II) an analysis of results obtained with the benchmarks execution in virtual infrastructures composed using different VXDL descriptions. / Grades de computadores vêm se afirmando como uma infra-estrutura integradora de recursos distribuídos. Embora já seja utilizado em grande escala, este tipo de infraestrutura computacional ainda constitui um campo de pesquisa ativo, com muitas questões em aberto. Pesquisas atuais investigam as chamadas grades virtuais, que tiram proveito de tecnologias de virtualização de recursos em sua composição. Essas grades podem ser definidas como uma abstração de alto nível dos recursos (computacionais e de comunicação), através da qual usuários têm uma visão de um amplo conjunto de computadores interligados, que podem ser selecionados e organizados virtualmente. Em grades virtuais, assim como em grades reais, usuários e middlewares devem dispor de ferramentas que permitam a composição e o gerenciamento das infra-estruturas. Dentre essas ferramentas, encontram-se as linguagens para descrição de recursos, que permitem a definição dos componentes que deverão ser utilizados na infra-estrutura. Em ambientes virtualizados, as linguagens descritivas devem oferecer atributos que interajam com peculiaridades, como a possibilidade de alocação de múltiplos recursos virtuais (computacionais e de rede) sobre um mesmo recurso físico. Neste contexto, este trabalho apresenta VXDL, uma linguagem projetada para a descrição de interconexões e recursos computacionais em grades virtuais. As inovações propostas em VXDL permitem a descrição, classificação e parametrização de todos os componentes desejáveis, bem como a definição de uma topologia de rede, inclusive informando a localização de roteadores virtuais. Permite-se também a definição de um cronograma de execução, que pode auxiliar middlewares nas tarefas de compartilhamento e escalonamento dos recursos. Para avaliar a linguagem proposta, apresenta-se I) um estudo comparativo entre VXDL e outras linguagens de descrição existentes, e II) uma análise de resultados obtidos com a execução de benchmarks sobre infra-estruturas compostas com diferentes descrições VXDL.

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2017-02-21T16:58:53Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Dissertação_SilviaVersaoFinal.pdf: 3562807 bytes, checksum: d273ad6c061161f899cab3d232a82a79 (MD5) / Made available in DSpace on 2017-02-21T16:58:54Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Dissertação_SilviaVersaoFinal.pdf: 3562807 bytes, checksum: d273ad6c061161f899cab3d232a82a79 (MD5) Previous issue date: 2016-08-01 / FACEPE / Contexto: A fase de especificação de requisitos é fundamental no processo de desenvolvimento de software. O uso de cenários é bastante popular para especificar requisitos, por serem descritos em linguagem natural. No entanto, a linguagem natural dá margem a requisitos ambíguos, incompletos e inconsistentes, o que vai de encontro com os objetivos da fase de especificação de requisitos. Nesse sentido, uma técnica baseada em Cenário & LEL (Language Extended Lexicon), chamada de C&L, pode ser a solução adequada, pois LEL é um glossário que define um conjunto de palavras que pertencem a um domínio e que devem ser usadas para descrever os cenários. Assim, C&L é considerada uma técnica de cenários baseada em linguagem natural controlada que ajuda a minimizar os problemas previamente mencionados, além de poder ser utilizada para criar casos de teste de forma mais sistemática. Objetivo: Neste trabalho, são propostas duas abordagens: a primeira abordagem usa regras de mapeamento para derivar modelos statechart a partir de C&L visando verificar a completude e consistência desses cenários e a segunda usa heurísticas para obter sistematicamente casos de teste a partir de modelos statechart. Método: A pesquisa apresentada nessa dissertação seguiu a abordagem de Engenharia para definir as regras de mapeamento e as heurísticas que, por sua vez, foram avaliadas empiricamente. Resultados: As regras de mapeamento apoiam a derivação de statechart a partir de C&L. As heurísticas apoiam a derivação de casos de teste a partir dos modelos statechart. Foi realizado um experimento para comparar o número de erros de incompletude e inconsistência detectados pelos grupos experimental e controle e o tempo gasto pelos grupos para detectar esses erros. Também foi verificado se os statecharts gerados através da aplicação das regras de mapeamento possuem grau de corretude e semelhança. Foi realizada uma avaliação qualitativa das heurísticas utilizadas para derivar os casos de teste, com o intuito de saber se as heurísticas foram utilizadas corretamente, se estão claras e são fáceis de usar. Conclusões: Os resultados do experimento mostram que o número de erros de incompletude detectados pelo grupo experimental foi superior ao número obtido pelo grupo controle e em relação aos erros de inconsistência não houve diferença entre quantidade de erros detectados pelos dois grupos. Além disso, a média do tempo gasto para identificar erros de incompletude e inconsistência pelo grupo experimental foi ligeiramente superior a média do tempo gasto pelo grupo controle. Em relação ao grau de corretude, dentre os modelos gerados pelo grupo experimental, existe um que apresenta o maior grau de corretude com 85,7%. No entanto, o grau de semelhança entre os modelos é considerado de “baixa semelhança”. O resultado da avaliação qualitativa mostrou que os participantes concordaram que as regras de mapeamento e as heurísticas são compreensíveis e fáceis de utilizar. Também foi observado que as heurísticas foram usadas de maneira correta na derivação dos casos de teste. / Context: The requirements specification phase is fundamental in the software development process. The use of scenarios is quite popular to specify requirements because they are described in natural language. However, natural language gives rise to ambiguous, incomplete and inconsistent requirements, jeopardizes the objectives of the requirements specification phase. In this context, a technique based on Scenarios and LEL (Language Extended Lexicon), called C&L, may be an appropriate solution because LEL is a glossary that defines a set of words that belong to a domain and should be used to describe the scenarios. Thus, C&L is a scenario technique based on controlled natural language that helps to minimize the problems previously mentioned, and can be used to create test cases in a more systematic way. Objective: In this study, two approaches are proposed: the first approach uses mapping rules to derive statechart models from C & L in order to verify the completeness and consistency of these scenarios and the second uses heuristics to systematically derive test cases from statechart models. Method: The research presented in this work follows the engineering approach to define the mapping rules and heuristics that, in turn, were empirically evaluated. Results: Mapping rules support the derivation of statechart from C & L. Heuristics support the derivation of test cases from statechart models. An experiment was conducted to compare the number of incompleteness and inconsistency errors detected by the experimental and control the groups and the time spent by groups to detect these errors. Also it was verified whether the statecharts generated by the application of the mapping rules have degree of correctness and likeness. A qualitative evaluation of the heuristics used to derive the test cases was made, in order to know whether the heuristics were correctly used and if they are clear and easy to use. Conclusions: The results of the experiment show that the number of incompleteness errors detected by the experimental group was higher than the number obtained by the control group, and in relation to inconsistency errors, there was no difference among the number of errors detected by the two groups. Furthermore, the average time spent to identify incompleteness and inconsistency errors by the experimental group was slightly higher than the average time spent by the control group. In relation to the degree of correctness among the models generated by the experimental group, there is one that has the highest degree of correctness with 85.7%. However, the degree of similarity between the models is considered "low similarity”. The result of the qualitative evaluation showed that the participants agreed that the mapping rules and heuristics are comprehensible and easy to use. It was also observed that the heuristics were used correctly in the derivation of test cases.

Made available in DSpace on 2014-07-29T14:57:52Z (GMT). No. of bitstreams: 1 Diss LuNishi.pdf: 535052 bytes, checksum: 312e4f56b2249ade58df12ebfe2b4dcb (MD5) Previous issue date: 2009-09-16 / This work uses mind maps to describe requirements and investigates this not well known application through an experiment. The experiment was based on desirable features sought by requirements engineers in notations and functions offered by tools. Both provided input to small changes in mind maps before a real specification was produced for the experiment. The results show that mind maps should be considered seriously as an alternative notation to describe software requirements / Este trabalho investiga o uso de mapas mentais na engenharia de requisitos, com destaque para o registro de requisitos. Características e funcionalidades desejáveis por engenheiros de requisitos foram coletadas e motivaram adaptações nos mapas mentais para uso neste domínio. Um experimento empregou a notação alterada e forneceu indícios positivos e negativos. O experimento permite, contudo, considerar o uso de mapas mentais como uma alternativa viável para o registro de requisitos e merecedora de pesquisas posteriores

Submitted by JÚLIO HEBER SILVA (julioheber@yahoo.com.br) on 2017-04-11T19:28:47Z No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2017-04-12T14:32:03Z (GMT) No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2017-04-12T14:32:03Z (GMT). No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2017-03-07 / Fundação de Amparo à Pesquisa do Estado de Goiás - FAPEG / The process of developing computer systems takes into account many stages, in which some are more necessary than others, depending on the purpose of the application. The implementation stage is always necessary, indisputably. Sometimes the requirements analysis and testing phases are neglected. And, generally, the part of formal verification correctness is intended for few applications. The use of model checkers has been exploited in the task of validating a behavioral specification in its appropriate level of abstraction, notably specifications validation of critical systems, especially when they involve the preservation of human life, when the existence of errors entails huge financial loss or when deals with information security. Therefore, it proposes to apply formal verification techniques in the validation of the vehicular safety system Avoiding Doored System, considered as critical, in order to verify if the implemented system faithfully meets the requirements for it proposed. For that, it was used as a tool to verify its correctness the Specification and Verification System - PVS, detailing and documenting all the steps employed in the process of specification and formal verification. K / O processo de desenvolvimento de sistemas computacionais leva em conta muitas etapas, nos quais umas são tidas mais necessárias que outras, dependendo da finalidade da aplica- ção. A etapa de implementação sempre é necessária, indiscutivelmente. Por vezes as fases de análise de requisitos e de testes são negligenciadas. E, geralmente, a parte de verifica- ção formal de corretude é destinada a poucas aplicações. O uso de verificadores de modelos tem sido explorado na tarefa de validar uma especificação comportamental no seu nível adequado de abstração, sobretudo, na validação de especificações de sistemas críticos, principalmente quando estes envolvem a preservação da vida humana, quando a existência de erros acarreta enorme prejuízo financeiro ou quando tratam com a segurança da informa- ção. Diante disso, se propõe aplicar técnicas de verificação formal na validação do sistema de segurança veicular Avoiding Doored System, tido como crítico, com o intuito de atestar se o sistema implementado atende, fielmente, os requisitos para ele propostos. Para tal, foi utilizada como ferramenta para a verificação de sua corretude o Specification and Verification System - PVS, detalhando e documentando todas as etapas empregadas no processo de especificação e verificação formal. Pal

Made available in DSpace on 2016-03-15T19:40:33Z (GMT). No. of bitstreams: 1 Luciana Cristina Lourencao.pdf: 752707 bytes, checksum: 1b88457ea10e0157d6392d2f5ecea036 (MD5) Previous issue date: 2008-08-14 / Pervasive Developmental Disorders (PDD) refer to a group of persistent and long-lasting behavioral disturbances characterized by qualitative implications on communication and social interaction, restrictive patterns of interests and stereotyped behaviors. Evidences have pointed to an atypical style of visual processing in autism, which is a condition belonging to PDD. This research was carried out in order to verify the familial and not familial face processing in children with Asperger syndrome (AS) or with Not Specified PDD (PDD-NOS) and to compare it with the same processing in control-children. Pictures of holistic faces (whole face and profile) and of parts of the face (eyes, nose and mouth) were presented to the children in a computer screen. The case-group refers to seven children with AS or PDD-NOS, and the control-group included other seven children with typical development. Children were 6-12 year old. All children had minimal IQ = 70 (WISC). Diagnoses of AS and PDD-NOS was established by the application of the Autism Screening Questionnaire (ASQ) and the Screening Questionnaire for Asperger Syndrome (ASSQ). Significant differences (p = 0,018) were observed inside the case-group when compared the success frequencies of familial (100%) and not familial (42%) faces. There were no significant differences between case and control groups in relation with success frequencies and time spent for familial whole faces processing. It is supposed that individuals with AS or PDD-NOS are able to develop an holistic style for processing very close familial whole faces. / Os Transtornos Invasivos do Desenvolvimento (TID) constituem um grupo de desordens do comportamento duradouras e persistentes que se caracterizam por comprometimento qualitativo da comunicação e da interação social, padrões restritos de interesses e presença de comportamentos estereotipados e maneirismos. Evidências crescentes mostram um estilo de processamento visual atípico no autismo, que faz parte desse grupo de desordens. O objetivo deste estudo foi verificar o reconhecimento de faces familiares e não familiares em indivíduos com síndrome de Asperger (SA) e com TID Sem Outra Especificação (TID-SOE) e compará-lo com o de um grupo-controle. Para tanto, utilizaram-se figuras de faces familiares holísticas (face inteira e perfil) ou de partes da face (olho, nariz e boca). Participaram da pesquisa 14 crianças do sexo masculino com idades variando de 6 a 12 anos. As sete crianças com SA e TID-SOE formaram o grupo-caso, e outras sete com desenvolvimento típico, o grupo-controle. Foi estabelecido como critério de inclusão QI mínimo de 70, avaliado pelo WISC em toda a amostra. As crianças do grupo-caso foram avaliadas com a aplicação do Autism Screening Questionnaire (ASQ) e do Screening Questionnaire for Asperger Syndrome (ASSQ). Considerando o grupo-caso, encontrou-se diferença significativa (p = 0,018) nos acertos quando comparadas figuras de faces familiares (100%) e não familiares (42%). Não foram observadas diferenças entre os grupos em relação ao número de acertos e ao tempo necessário para o reconhecimento da prancha familiar de face inteira. Supõe-se que os indivíduos com SA e TID-SOE conseguem desenvolver uma forma holística de processamento mediante uma face inteira familiar muito íntima.