Navegando por Autor "Oliveira, Marcel Vinícius Medeiros"

Agora exibindo 1 - 7 de 7

Beta: a B based testing approach
(2016-04-14) Matos, Ernesto Cid Brasil de; Moreira, Anamaria Martins; Leuschel, Michael; ; ; http://lattes.cnpq.br/2363575151206774; ; http://lattes.cnpq.br/4276245931614707; Oliveira, Marcel Vinícius Medeiros; ; http://lattes.cnpq.br/1756952696097255; Mota, Alexandre Cabral; ; http://lattes.cnpq.br/2794026545404598; Machado, Patricia Duarte de Lima; ; http://lattes.cnpq.br/2495918356675019
Sistemas de software estão presentes em grande parte das nossas vidas atualmente e, mais do que nunca, eles requerem um alto nível de confiabilidade. Existem várias técnicas de Ver- ificação e Validação (V&V) de software que se preocupam com controle de qualidade, segu- rança, robustez e confiabilidade; as mais conhecidas são Testes de Software e Métodos For- mais. Métodos formais e testes são técnicas que podem se complementar. Enquanto méto- dos formais provêem mecanismos confiáveis para raciocinar sobre o sistema em um nível mais abstrato, técnicas de teste ainda são necessárias para uma validação mais profunda e são frenquentemente requeridas por orgãos de certificação. Levando isto em consideração, BETA provê uma abordagem de testes baseada em modelos para o Método B, suportada por uma ferramenta, que é capaz de gerar testes de unidade a partir de máquinas abstratas B. Nesta tese de doutorado apresentamos melhorias realizadas em BETA e novos estudos de caso realizados para avaliá-la. Dentre as melhorias, integramos critérios de cobertura lógicos à abordagem, revisamos os critérios de cobertura baseados em espaço de entrada que já eram suportados e aperfeiçoamos as últimas etapas do processo de geração de testes. A abordagem agora suporta a geração automática de dados para os oráculos e preâmbulos para os casos de teste; ela também possui uma funcionalidade para concretização dos da- dos de teste e um módulo para gerar scripts de teste executáveis automaticamente. Outro objetivo desta tese foi realizar estudos de caso mais complexos utilizando BETA e avaliar a qualidade dos casos de teste que a abordagem produz. Estes estudos de caso foram os primeiros a avaliar o processo de geração de testes por completo, desde a especificação dos casos de teste até a sua implementação e execução. Em nossos últimos experimentos, analisamos a qualidade dos casos de teste gerados por BETA, considerando cada critério de cobertura suportado, utilizando métricas de cobertuda de código como cobertura de in- struções e ramificações. Também utilizamos testes de mutação para avaliar a capacidade dos casos de teste de detectar faltas na implementação dos modelos. O resultados obtidos foram promissores mostrando que BETA é capaz de detectar faltas introduzidas por progra- madores ou geradores de código e que a abordagem pode obter bons resultados de cobertura para a implementação de um sistema baseado em modelos B.
Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B
(Universidade Federal do Rio Grande do Norte, 2015-03-09) Fragoso, Paulo Ewerton Gomes; Deharbe, David Boris Paul; ; http://lattes.cnpq.br/2985658685449858; ; http://lattes.cnpq.br/9393335275523504; Gomes, Bruno Emerson Gurgel; ; http://lattes.cnpq.br/7812661521592212; Oliveira, Marcel Vinícius Medeiros; ; http://lattes.cnpq.br/1756952696097255; Bonichon, Richard Walter Alain;
Event-B é um método formal de modelagem e verificação de sistemas de transição discretos. O desenvolvimento com Event-B produz obrigações de prova que devem ser verificadas, isto é, ter sua validade verificada para manter a consistência dos modelos produzidos. Solucionadores de Satisfatibilidade Módulo Teoria são provadores automáticos de teoremas usados para verificar a satisfatibilidade de fórmulas lógicas considerando uma teoria (ou combinação de teorias) subjacente. Solucionadores SMT não apenas lidam com fórmulas extensas em lógica de primeira ordem, como também podem gerar modelos e provas, bem como identificar subconjuntos insatisfatíveis de hipóteses (núcleos insatisfatíveis). O suporte ferramental para Event-B é provido pela Plataforma Rodin: um IDE extensível, baseado no framework Eclipse, que combina funcionalidades de modelagem e prova. Um plug-in SMT para Rodin tem sido desenvolvido com o objetivo de integrar à plataforma técnicas alternativas e eficientes de verificação. Neste trabalho foi implementada uma série de complementos ao plug-in para solucionadores SMT em Rodin, a saber, melhorias na interface do usuário para quando obrigações de prova são reportadas como inválidas pelo plug-in. Adicionalmente, algumas características do plug-in, tais como suporte à geração de provas e extração de núcleo insatisfatível, foram modificadas de modo a tornaremse compatíveis com o padrão SMT-LIB para solucionadores SMT. Realizaram-se testes utilizando obrigações de prova aplicáveis para demonstrar as novas funcionalidades. As contribuições descritas podem, potencialmente, afetar a produtividade de forma positiva.
Development and results of an instrument to search for competences and abilities in information technology
(2015-12-25) Gomes, Apuena Vieira; Hazin, Izabel; Falcão, Jorge Tarcísio da Rocha; Meira, Luciano; Bendassolli, Pedro; Guerra, Amanda; Falcão, Taciana Pontual; Reis, Juliana Teixeira da Câmara; Oliveira, Marcel Vinícius Medeiros; Rêgo, José Ivonildo do
This article presents an analysis of the selection process of students from both private and public high schools in the state of Rio Grande do Norte (Northeast of Brazil), in order to form the first group of the Information Technology technical course of the Metrópole Digital project at the Federal University of Rio Grande do Norte (UFRN). The selection instrument consists of a written exam built on the basis of a set of matrices that depict relevant competences and abilities expected from the students. Data concerning the profile of distribution of performance per exam question are presented, together with empirical evidences of the effectiveness of the proposed competence matrices in the selection process. The correlation very fied among the matrices compounding the instrument and scores in courses, and the instrument as a wholeand scores in courses is moderate to strong (rS = 0.6 and rS = 0.7; p < 0,05). The association between the criterion variables (Average of Performance in the Basic Moduleof courses) and the explicative variables (Total score in the selection instrument (QTot) and each of the five compounding matrices) is moderate (rS=0.51, p = 0.001), and the matrices and QTot are jointly responsible for 25% of the variance of the performance in the basic module. The regression coefficient for matrix 1 is 1.38 (CI of 95% = 1.07-1.68); for matrix 2 it was 0.65 (CI of 95% = 036-0.95); for matrix 3, 1.2 (CI of 95% = 0.92 - 1,55); matrix 4 0,76 (CI of 95% = 0.45-1.06); matrix 5 1.08 (CI of 95% = 0.78-1.39). The effects of student-descriptive independent variables on performance in the exam are also presented and discussed, and predictive relationships between performance in the exam and performance in the disciplines of the course are verified. Data collected allow concluding that the instrument of selection proposed fits well the aim of forming a group of students to undertake a technical course in the area of information technology
Legis + SIAI AP Concessões: uma solução para automatizar a análise dos atos de concessão de benefício sujeitos à apreciação do Tribunal de Contas do Rio Grande do Norte
(Universidade Federal do Rio Grande do Norte, 2019) Soares, Renato Mesquita; Oliveira, Marcel Vinícius Medeiros; Franco, Evandro Nunes; Cavalcante, Everton Ranielly de S.; Cacho, Nelio Alessandro Azevedo
O TCE/RN é o órgão responsável pelo exercício do controle externo e, mais particulamente a DAP, pela execução de procedimentos de fiscalização dos atos de pessoal sujeitos a registro. Nesse sentido, pela falta de automação dos procedimentos realizados, o Tribunal sofre com o acúmulo desses processos, ocasionando, em algumas situações, gastos indevidos ao estado pela falta de celeridade na detecção de benefícios indevidamente concedidos. Nessa linha, foi concebido um projeto capaz de sistematizar os procedimentos inerentes ao fluxo do ato, através de um sistema chamado de SIAI AP Concessões. Ainda em fase de concepção, foi necessário o desenvolvimento de um outro sistema, chamado de Legis, responsável por ser a base legislativa para fundamentar o SIAI AP Concessões. Nesse contexto, o presente documento visa, além de relatar os procedimentos executados durante o desenvolvimento desses sistemas, expor todas informações que possam elucidar a compreensão desses sistemas.
Método B e a síntese verificada para código de montagem
(2016-03-08) Medeiros Júnior, Valério Gutemberg de; Deharbe, David Boris Paul; ; http://lattes.cnpq.br/2985658685449858; ; http://lattes.cnpq.br/7451897900811657; Musicante, Martin Alejandro; ; http://lattes.cnpq.br/6034405930958244; Oliveira, Marcel Vinícius Medeiros; ; http://lattes.cnpq.br/1756952696097255; Mota, Alexandre Cabral; ; http://lattes.cnpq.br/2794026545404598; Gomes, Bruno Emerson Gurgel; ; http://lattes.cnpq.br/7812661521592212
A síntese de código de montagem é um processo que exige um cuidado rigoroso. Normalmente, esse processo nos tradutores e nos compiladores mais maduros é relativamente seguro, apesar de que, esporadicamente, erros são identificados neles. Em um contexto mais restrito, os tradutores utilizados em comunidades menores e em constante desenvolvimento são mais suscetíveis a erros. Considerando esse contexto, duas abordagens de tradução e de verificação usando o método B são apresentadas. A primeira abordagem propõe a tradução do componente B para o código de montagem de uma plataforma específica, usando um modelo formal do conjunto de instruções, o qual possibilita também depurar e verificar as propriedades de programas. Essa abordagem é capaz de garantir formalmente a coerência semântica da tradução, apesar de ser um processo de verificação árduo e lento. Tal esforço de verificação foi aliviado através de uma ferramenta desenvolvida (BEval), que aproveitou melhor as técnicas de verificação. Após o processo de prova automática usando uma ferramenta B robusta (Atelier B), BEval ainda foi capaz de resolver em certos modelos muitas das obrigações de prova remanescentes, chegando a até 88% do total de obrigações. Contudo, o processo de verificação da abordagem de tradução continuou complexo, exigindo várias interações manuais. Afim de viabilizar uma tradução mais eficiente e também segura, uma segunda abordagem de tradução de B para o código de máquina virtual foi desenvolvida. A segunda abordagem utilizou o tradutor desenvolvido B2LLVM e aplicou a geração automática de testes para verificar a coerência entre a especificação do programa e o seu respectivo código de montagem. Esse tradutor também suporta a avaliação de cobertura do código e a inserção de anotações de rastreabilidade. Dessa forma, o trabalho contribuiu significativamente na tradução de B para o código de montagem, oferecendo um suporte rigoroso para a verificação da tradução. Atualmente, o B2LLVM já é capaz de gerar código para 84% dos exemplos de teste baseados na gramática que são traduzíveis por um relevante tradutor industrial (C4B). Ademais, o código gerado por B2LLVM apresenta vantagens importantes na ampla capacidade de verificação, de integração e de otimização.
Motor de associação de cálculos de benefícios
(Universidade Federal do Rio Grande do Norte, 2020) Nascimento, Ormazabal Lima do; Oliveira, Marcel Vinícius Medeiros; Barroca Filho, Itamir de Morais; Rocha, Sheyla Yusk Cunha Nelson dos Santos Cavalcanti da
O ato de concessão de benefício gera direito ao servidor público de receber uma contribuição financeira mensal através da previdência social. Compete ao Tribunal de Contas do Estado do Rio Grande do Norte (TCE/RN) a análise da legalidade dos atos advindos de seus jurisdicionados, e o SIAI AP Concessões é um sistema desenvolvido para auxiliar esse fim. Durante o cadastro de um ato, a aplicação deve calcular os benefícios financeiros o qual o servidor tem direito. O cálculo tem suas regras definidas em legislações que estão em constante alteração. Por este motivo, fazer com que essas regras sejam inseridas no código fonte pode provocar a constante necessidade de atualização do sistema. Diante dessa problemática foi desenvolvido o Motor de Associação de Cálculo de Benefícios (MAC), uma ferramenta que, por meio de parâmetros configuráveis, proporciona ao administrador do sistema a conversão de uma fundamentação jurídica em uma regra de cálculo que será entendida pelo sistema. Este trabalho apresentará a solução, discutirá as decisões tomadas, sua implementação e seus benefícios.
Uma plataforma de BI voltada para o acompanhamento das ações estratégicas do TCE/RN
(Universidade Federal do Rio Grande do Norte, 2020) Damasceno, Alexandre Luiz Galvão; Oliveira, Marcel Vinícius Medeiros; Júnior, João Carlos Xavier; Reginaldo, César Gláucio Torquato
Este trabalho apresenta os passos para o desenvolvimento de uma plataforma para auxiliar no monitoramento da execução dos planos estratégicos do Tribunal de Contas do Rio Grande do Norte, utilizando as tecnologias de Business Intelligence. Esse sistema objetiva reduzir o tempo e esforço gastos na gestão das ações estratégicas em curso no Tribunal, permitindo que estas também sejam acompanhadas por qualquer servidor desta corte de contas. Esta plataforma desenvolvida foi posta em operação, alimentada com os dados do sistema de acompanhamento de projetos e ações, Channel, e pode ser acessada dentro da intranet do TCE/RN, a ”Área Restrita”, e já está sendo usada para a produção dos relatórios dos resultados da execução das ações estratégicas da gestão do biênio 2019 e 2020.

SIGAA

Navegando por Autor "Oliveira, Marcel Vinícius Medeiros"