Navegando por Autor "Moreira, Anamaria Martins"

Agora exibindo 1 - 20 de 23

Agraphs: definição, implementação e suas ferramentas
(Universidade Federal do Rio Grande do Norte, 2006-05-19) Sena, Demóstenes Santos de; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; ; http://lattes.cnpq.br/3949512835562758; Déharbe, David Boris Paul; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5; Musicante, Martin Alejandro; ; http://lattes.cnpq.br/6034405930958244; Ierusalimschy, Roberto; ; http://lattes.cnpq.br/0427692772445368
Programas manipulam informações. Entretanto, as informações são essencialmente abstratas e precisam ser representadas, normalmente por estruturas de dados, permitindo a sua manipulação. Esse trabalho apresenta os AGraphs, um formato de representação e transferência de dados que usa grafos direcionados tipados que permitem a simulação de hiperarestas e de grafos hierárquicos. Associado ao formato AGraphs existe uma biblioteca de manipulação com uma interface simples de ser usada, mas dependente da linguagem. O formato AGraphs foi usado de maneira ad-hoc como formato de representação em algumas ferramentas desenvolvidas na UFRN, e, com a possibilidade de uso em outras aplicações, tornou-se necessária uma definição precisa e o desenvolvimento de ferramentas de suporte. A definição precisa e as ferramentas foram desenvolvidas e são descritas neste trabalho. Finalizando, comparações do formato AGraphs com outros formatos de representação e transferência de dados (ATerms, GDL, GraphML, GraX, GXL e XML) são realizadas. O principal objetivo destas comparações é obter as características significantes e em que conceitos o formato e a biblioteca AGraphs deve amadurecer
Aplicação do método B ao projeto formal de software embarcado
(Universidade Federal do Rio Grande do Norte, 2009-09-09) Medeiros Júnior, Valério Gutemberg de; Déharbe, David Boris Paul; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5; ; http://lattes.cnpq.br/7451897900811657; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; Cavalcanti, Ana Lúcia Caneca; ; http://lattes.cnpq.br/9213785092326881; Maitelli, André Laurindo; ; http://lattes.cnpq.br/0477027244297797
Este trabalho apresenta um método de projeto proposta para veri cação formal do modelo funcional do software até o nível da linguagem assembly. Esse método é fundamentada no método B, o qual foi desenvolvido com o apoio e interesse da multinacional do setor de petróleo e gás British Petroleum (BP). A evolução dessa metodologia tem como objetivo contribuir na resposta de um importante problema, que pertence aos grandes desa os da computação, conhecido como The Verifying Compiler . Nesse contexto, o presente trabalho descreve um modelo formal do microcontrolador Z80 e um sistema real da área de petróleo. O modelo formal do Z80 foi desenvolvido e documentado, por ser um pré-requisito para a veri cação até nível de assembly. A m de validar e desenvolver a metodologia citada, ela foi aplicada em um sistema de teste de produção de poços de petróleo, o qual é apresentado neste trabalho. Atualmente, algumas atividades são realizadas manualmente. No entanto, uma parte signifi cativa dessas atividades pode ser automatizada através de um compilador específi co. Para esse m, a modelagem formal do microcontrolador e a modelagem do sistema de teste de produção fornecem conhecimentos e experiências importantes para o projeto de um novo compilador. Em suma, esse trabalho deve melhorar a viabilidade de um dos mais rigorosos critérios de veri cação formal: acelerando o processo de verificação, reduzindo o tempo de projeto e aumentando a qualidade e con fiança do produto de software final. Todas essas qualidades são bastante relevantes para sistemas que envolvem sérios riscos ou exigem alta confiança, os quais são muito comuns na indústria do petróleo
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.
Beta: uma ferramenta para geração de testes de unidade a partir de especificações B
(Universidade Federal do Rio Grande do Norte, 2012-02-10) Matos, Ernesto Cid Brasil de; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; ; http://lattes.cnpq.br/4276245931614707; Coelho, Roberta de Souza; ; http://lattes.cnpq.br/9854634275938452; Machado, Patrícia Duarte de Lima; ; http://lattes.cnpq.br/2495918356675019
Métodos formais e testes são ferramentas para obtenção e controle de qualidade de software. Quando utilizadas em conjunto, elas provêem mecanismos para especificação, verificação e detecção de falhas de um software. Apesar de permitir que sistemas sejam matematicamente verificados, métodos formais não são suficientes pra garantir que um sistema esteja livre de defeitos, logo, técnicas de teste de software são necessárias para completar o processo de verificação e validação de um sistema. Técnicas de Testes Baseados em Modelos permitem que testes sejam gerados a partir de outros artefatos de software como especificações e modelos abstratos. Ao utilizarmos especificações formais como base para a criação de testes, podemos gerar testes de melhor qualidade pois estas especificações costumam ser precisas e livres de ambiguidade. Fernanda Souza (2009) propôs um método para definir casos de teste a partir de especificações do Método B. Este método utilizava informações do invariante de uma máquina e das pré-condições de uma operação para definir casos de teste positivos e negativos para tal operação, através de técnicas baseadas em particionamento em classes de equivalência e análise de valor limite. No entanto, a proposta de 2009 não incluía automação e possuía algumas deficiências conceituais como, por exemplo, não se encaixar exatamente em uma classificação de critérios de cobertura bem definida. Iniciamos nosso trabalho com um estudo de caso que aplicou o método a um exemplo de especificação B proveniente da indústria. A partir deste estudo obtivemos subsídios para o aperfeiçoá-lo. Em nosso trabalho aperfeiçoamos o método proposto, reescrevendo e adicionando características para torná-lo compatível com uma classificação de testes utilizada pela comunidade. O método também foi melhorado para suportar especificações estruturadas em vários componentes, utilizar informações sobre o comportamento da operação durante a criação de casos de teste e utilizar novos critérios de cobertura. Além disso, implementamos uma ferramenta para automatizá-lo e o submetemos a estudos de caso mais complexos
BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B
(Universidade Federal do Rio Grande do Norte, 2007-11-19) Gomes, Bruno Emerson Gurgel; Moreira, Anamaria Martins; Déharbe, David Boris Paul; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5; ; http://lattes.cnpq.br/5861361541278876; ; http://lattes.cnpq.br/7812661521592212; Oliveira, Marcel Vinicius Medeiros; ; http://lattes.cnpq.br/1756952696097255
A tecnologia Java Card permite o desenvolvimento e execução de pequenas aplicações embutidas em smart cards. Uma aplicação Java Card é composta por um cliente, externo ao cartão, e por uma aplicação contida no cartão que implementa os serviços disponíveis ao cliente por meio de uma Application Programming Interface (API). Usualmente, essas aplicações manipulam e armazenam informações importantes, tais como valores monetários ou dados confidenciais do seu portador. Sendo assim, faz-se necessário adotar um maior rigor no processo de desenvolvimento de uma aplicação smart card, visando melhorar a sua qualidade e confiabilidade. O emprego de métodos formais como parte desse processo é um meio de se alcançar esses requisitos de qualidade. O método formal B ´e um dentre os diversos métodos formais para a especificação de sistemas. O desenvolvimento em B tem início com a especificação funcional do sistema, continua com a aplicação opcional de refinamentos à especificação e, a partir do último nível de refinamento, é possível a geração de código para alguma linguagem de programação. O formalismo B conta com bom suporte de ferramentas e a sua aplicação a Java Card mostra-se bastante adequada, uma vez que a especificação e desenvolvimento de APIs ´e o ponto forte de B. O método BSmart aqui proposto visa promover o desenvolvimento rigoroso de aplicações Java Card a partir da geração de código da aplicação com base em refinamentos da sua especificação formal descrita na notação B. O processo de desenvolvimento descrito no método é apoiado pela ferramenta BSmart, a qual constitui-se por alguns programas que automatizam cada etapa do método; e por uma biblioteca de módulos B e classes Java Card que modelam tipos primitivos, classes essenciais da API Java Card e estruturas de dados reutilizáveis
BTS:uma ferramenta de suporte ao desenvolvimento sistemático de sistemas confiáveis baseados em componentes
(Universidade Federal do Rio Grande do Norte, 2013-12-13) Silva, Sarah Raquel da Rocha; Oliveira, Marcel Vinicius Medeiros; ; http://lattes.cnpq.br/1756952696097255; ; http://lattes.cnpq.br/3078875506981199; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; Mota, Alexandre Cabral; ; http://lattes.cnpq.br/2794026545404598
O desenvolvimento de sistemas baseados em componentes revolucionou o processo de desenvolvimento de software, facilitando a manutenção, trazendo mais confiabilidade e reutilização. Porém, mesmo com todas as vantagens atribuídas ao componente, é necessário uma análise detalhada de sua composição. Realizar verificação a partir de testes de software não é o suficiente para se ter uma composição segura, pois esses não são baseados em modelos semânticos formais nos quais podemos descrever precisamente o comportamento do sistema. Nesse contexto, os métodos formais oferecem a possibilidade de especificarmos sistemas de forma precisa, através de notações com forte base matemática, trazendo, entre outros benefícios, mais segurança. O método formal CSP possibilita a especificação de sistemas concorrentes e verificação de propriedades inerentes a tais sistemas, bem como refinamento entre diferentes modelos. Existem abordagens que aplicam restrições usando CSP, para verificar o comportamento da composição entre componentes, auxiliando a verificação desses componentes antecipadamente. Visando auxiliar esse processo, tendo em vista que o mercado de software busca cada vez mais automação, minimizando trabalhos e trazendo agilidade nos negócios, este trabalho apresenta uma ferramenta que automatiza a verificação da composição entre componentes, onde o conjunto de verificações CSP impostas é gerado e verificado internamente, oculto para o usuário. Dessa forma, através de uma interface simples, a ferramenta BTS (BRIC-Tool-Suport) ajuda a criar e compor componentes, prevendo, com antecedência, comportamentos indesejáveis no sistema, como deadlocks
Desenvolvimento formal de aplicações para smartcards
(Universidade Federal do Rio Grande do Norte, 2012-06-01) Gomes, Bruno Emerson Gurgel; Déharbe, David Boris Paul; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5; ; http://lattes.cnpq.br/7812661521592212; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; Sampaio, Augusto Cezar Alves; ; http://lattes.cnpq.br/3977760354511853; Oliveira, Marcel Vinicius Medeiros; ; http://lattes.cnpq.br/1756952696097255
As aplicações para smart cards representam um mercado que cresce a cada ano. Normalmente, essas aplicações manipulam e armazenam informações que requerem garantias de segurança, tais como valores monetários ou informações confidenciais. A qualidade e a segurança do software para cartões inteligentes pode ser aprimorada através de um processo de desenvolvimento rigoroso que empregue técnicas formais da engenharia de software. Neste trabalho propomos o método BSmart, uma especialização do método formal B dedicada ao desenvolvimento de aplicações para smart cards na linguagem Java Card. O método descreve, em um conjunto de etapas, como uma aplicação smart card pode ser gerada a partir de refinamentos em sua especificação formal. O desenvolvimento é suportado por um conjunto de ferramentas, automatizando a geração de parte dos refinamentos e a tradução para as aplicações Java Card cliente (host) e servidora (applet). Ressalta-se que o processo de especificação e refinamento descrito no método foi formalizado e verificado utilizando o próprio método B, com o auxílio da ferramenta Atelier B [Cle12a]. Destaca-se que a aplicação Java Card é traduzida a partir do último passo de refinamento, denominado de implementação. A especificação dessa tradução foi feita na linguagem ASF+SDF [BKV08]. Inicialmente, descreveu-se as gramáticas das linguagens B e Java (SDF) e, em uma etapa posterior, especificou-se as transformações de B para Java Card através de regras de reescrita de termos (ASF). Essa abordagem foi um importante auxílio durante o processo de tradução, além de servir ao propósito de documentálo. Cumpre destacar a biblioteca KitSmart [Dut06, San12], componente essencial ao método BSmart, que inclui modelos em B de todas as 93 classes/interfaces da API Java Card na versão 2:2:2, dos tipos de dados Java e Java Card e de máquinas que podem ser úteis ao especificador, mas que não estão presentes na API padrão. Tendo em vista validar o método, seu conjunto de ferramentas e a biblioteca KitSmart, procedeu-se com o desenvolvimento, seguindo o método BSmart, de uma aplicação de passaporte eletrônico. Os resultados alcançados neste trabalho contribuem para o desenvolvimento smart card, na medida em que possibilitam a geração de aplicações Java Card completas (cliente e servidor) e menos sujeitas a falhas.
Especiﬁcação do tipo intervalar parametrizado em CASL
(Universidade Federal do Rio Grande do Norte, 2006-05-19) Melo, Samara Pereira da Costa; Bedregal, Benjamin René Callejas; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4781417E7; ; http://lattes.cnpq.br/6933781856093521; Campos, Marcília Andrade; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4783192D1; Santiago, Regivan Hugo Nunes; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4790032Z4; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876
O uso do tipo intervalar em várias áreas favorece a idéia de se ter uma estrutura básica reutilizável, ou seja, um construtor intervalar que seja aplicado a um tipo de dados para se obter os intervalos desse tipo. Como um intervalo, intuitivamente é o conjunto de elementos que estão entre dois extremos, sua construção presupõe a noção de ordem, e portanto é razoável que este construtor trabalhe sobre tipos munidos de uma ordem parcial. Por outro lado, como o que se quer é operar com intervalos de objetos de um certo tipo como se opera com esses objetos, então também é razoável querer que as propriedades algébricas desses objetos sejam preservadas no seu tipo intervalar. Assim, o construtor intervalar fornece uma fundamentação teórica para o tipo intervalo parametrizado, ou seja, intervalos cujo parâmetro é generalizado podendo ser, por exemplo, números reais, complexos, etc. A aplicação do intervalo em certas estruturas algébricas nem sempre garante a preservação de suas características, por exemplo, quando se trabalha com intervalos de números reais, seria conveniente que estes pudessem se comportar como se fossem os reais. Isto não acontece pois os reais satisfazem as propriedades algébricas de corpo, já os intervalos de reais não (por exemplo, não suporta a propriedade distributiva). Para superar esta diﬁculdade Santiago introduziu a teoria da igualdade local numa forma de enfraquecer a noção de igualdade forte fazendo com que propriedades satisfeitas localmente sejam relevantes, propriedades estas que antes poderiam ser descartadas. A generalização da aritmética intervalar propõe a aplicação do construtor intervalar em estruturas algébricas ordenadas e enfraquecidas pela igualdade local, objetivando a manutenção de suas propriedades algébricas. Como os intervalos são importantes em aplicações que trabalhem com dados contínuos, é interessante descrever esta teoria usando uma linguagem de especiﬁcação que permita o desenvolvimento de sistemas computacionais que usem tipos intervalares de modo disciplinado, conﬁável e seguro. Atualmente, as linguagens de especiﬁcações algébricas, que se baseiam em modelos matemáticos, têm sido muito usadas para este proposito. Dentre as várias linguagens deste tipo existentes, foi escolhida CASL (Common Algebraic Speciﬁcation Language) por conter diversas características relevantes para especiﬁcação do tipo intervalar parametrizado como, por exemplo, admitir parametrização e parcialidade
Estendendo CRefine para o suporte de táticas de refinamento
(Universidade Federal do Rio Grande do Norte, 2011-10-07) Conserva Filho, Madiel de Souza; Oliveira, Marcel Vinicius Medeiros; ; http://lattes.cnpq.br/1756952696097255; ; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; Sampaio, Augusto Cezar Alves; ; http://lattes.cnpq.br/3977760354511853
A utilização de aplicações de software cada vez mais complexas está exigindo um maior investimento no desenvolvimento de sistemas, garantindo uma melhor qualidade das aplicações. Diante desse contexto, novas técnicas estão sendo utilizadas na área de Engenharia de Software, tornado o processo de desenvolvimento mais eficaz. Destacam- se, como exemplo dessas novas abordagens, os Métodos Formais. Estes métodos utilizam linguagens formais que têm sua base fundamentada na matemática, apresentando uma semântica e sintaxe bem definidas. Uma dessas linguagens é Circus, que possibilita a mo- delagem de sistemas concorrentes. Esta linguagem foi desenvolvida a partir da união dos conceitos das linguagens formais Z (que permitem a modelagem de dados complexos) e CSP Communicating Sequential Processes (que permitem a modelagem de sistemas con- correntes). Adicionalmente, Circus também possui um cálculo de refinamento associado, que pode ser utilizado para desenvolver software de forma precisa e gradual. Cada etapa deste cálculo é justificada pela aplicação de uma lei de refinamento (possivelmente com a prova de certas condições chamadas de obrigações de prova). Algumas vezes, as mesmas leis podem ser aplicadas da mesma forma em diferentes desenvolvimentos ou mesmo em partes diferentes de um único desenvolvimento. Uma estratégia para otimizar esse cál- culo é formalizar estas aplicações como táticas de refinamento, que podem ser utilizadas como uma simples regra de transformação. A ferramenta CRefine foi desenvolvida para realizar o suporte a este cálculo de refinamento de Circus. Entretanto, antes deste traba- lho, essa ferramenta não fornecia suporte para as táticas. A proposta desta dissertação é oferecer um suporte ferramental para a utilização das táticas no cálculo de refinamento de programas Circus. Para tanto, foi desenvolvido um novo módulo em CRefine, que auto- matiza o processo de definição e aplicação das táticas de refinamento. Nesta extensão as táticas são formalizadas na linguagem de táticas para sistemas concorrentes, ArcAngelC. Por fim, validamos a extensão, aplicando o novo módulo a um estudo de caso, que utiliza as táticas em uma estratégia de refinamento para verificação de implementações SPARK Ada de sistemas de controle. Nesta dissertação, aplicamos o novo modulo às duas fases iniciais desta estratégia.
Um estudo empírico sobre geração de testes com BETA: Avaliação e aperfeiçoamento
(2015-08-07) Souza Neto, João Batista De; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/2363575151206774; ; Deharbe, David Boris Paul; ; http://lattes.cnpq.br/2985658685449858; Gheyi, Rohit; ; http://lattes.cnpq.br/2931270888717344
A demanda de sistemas seguros e robustos fez com que crescesse a preocupação em desenvolver software de qualidade. Teste de Software e Métodos Formais são duas abordagens que possuem essa finalidade. Neste contexto, vários esforços vem sendo feitos para unir essas duas abordagens, que podem se complementar e trazer mais qualidade para o software. Em um desses esforços, foi desenvolvida a abordagem e ferramenta BETA (B Based Testing Approach). BETA gera testes de unidade a partir de especificações formais escritas na notação do Método B. O presente trabalho tem o objetivo de contribuir com a evolução e o aperfeiçoamento da abordagem e ferramenta BETA. Em uma primeira linha de ação, este trabalho propôs estratégias de oráculos de teste para a abordagem e desenvolveu um gerador de scripts de teste para a ferramenta. Com isso, este trabalho trouxe mais flexibilidade e automação para as últimas etapas de BETA. Em uma segunda linha de ação, este trabalho realizou um estudo empírico para avaliar a abordagem e ferramenta. Dessa forma, BETA foi aplicada em dois estudos de caso que possuíam diferentes objetivos e complexidades. Em ambos os estudos de caso, os resultados de BETA foram avaliados quantitativamente e qualitativamente. Com esse estudo, este trabalho conseguiu identificar qualidades e limitações de BETA e, com isso, estabelecer uma base para propor melhorias para a abordagem e ferramenta.
A family of coverage criteria based on patterns to the test of metaprograms
(2017-12-15) Antunes, Cleverton Hentz; Moreira, Anamaria Martins; ; ; Musicante, Martin Alejandro; ; Borba, Paulo Henrique Monteiro; ; Gheyi, Rohit; ; Costa, Umberto Souza da;
Apesar da existência de várias técnicas para a geração automática de dados de teste baseados em gramáticas, poucos trabalhos foram propostos no sentido de melhorar os dados de teste gerados aplicando restrições semânticas. Nesse sentido, contribuimos neste trabalho, nesta direção para o caso particular do teste de metaprogramas, um programa que tem como dado de entrada um outro programa. Atualmente, a alternativa natural para o teste deste tipo de programa é a técnica de testes baseados em gramáticas. Essa técnica de teste pode ser aplicada de maneira relativamente simples, porém com um custo de geração e execução do conjunto de testes elevado e uma efetividade baixa. Por outro lado, diversas pesquisas e ferramentas de grupos interessados no desenvolvimento de metaprogramas fazem uso intenso do recurso de casamento de padrões durante a sua implementação e especificação. Neste caso, os padrões oferecem uma fonte de informação interessante para a criação de testes que são sintaticamente válidos e também satisfazem restrições semânticas. Dada a limitação dos testes baseados em gramáticas e considerando a informação embutida nos padrões existentes nos metaprogramas, temos a oportunidade de contribuir para a melhoria do processo de teste para esses programas. Logo, o objetivo deste trabalho é avaliar o uso da informação de padrões para o teste de metaprogramas e com isso contribuir no seu processo de teste. No intuito de sistematizar o processo de teste de software, o documento apresenta um processo de design de teste e também uma família de critérios de cobertura baseados em padrões para o teste eficiente e sistematizado de metaprogramas baseados em padrões. São propostos quatro critérios de cobertura baseados em padrões e nos critérios de particionamento do espaço de entrada. Também é apresentada uma hierarquia entre os critérios propostos. Com isso, diferentes níveis de rigor podem ser requeridos no processo através da escolha do critério adequado. A validação dessas contribuições é feita através de um estudo de caso e uma validação empírica. O estudo de caso apresenta uma instanciação de referência para o processo de design de testes de um verificador de tipos implementado como metaprograma baseado em padrões. O verificador de tipos é testado usando um conjunto de testes gerados pelos critérios de cobertura baseados em padrões. A qualidade desse conjunto é avaliada utilizando a técnica de mutação e através da comparação dos resultados obtidos com testes gerados por critérios baseados em gramáticas. Os estudos experimentais indicam a efetividade da aplicação dos critérios baseados em padrões e o ganho em custo-benefício em relação aos critérios baseados em gramáticas no contexto do teste de metaprogramas baseados em padrões.
Geração automática de testes a partir de descrições de linguagens
(Universidade Federal do Rio Grande do Norte, 2010-03-01) Antunes, Cleverton Hentz; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; ; http://lattes.cnpq.br/7382708415783357; Coelho, Roberta de Souza; ; http://lattes.cnpq.br/9854634275938452; Ierusalimschy, Roberto; ; http://lattes.cnpq.br/0427692772445368
Alguns programas podem ter sua entrada formalizada através de gramáticas livres de contexto. Esta formalização facilita a utilização de ferramentas na sistematização e na elevação da qualidade do seu processo de teste. Dentro desta categoria de programas os compiladores foram os primeiros a utilizar este tipo de ferramenta para a automação de seus testes. Neste trabalho apresentamos uma abordagem para a definição de testes a partir da descrição formal das entradas do programa. A geração das sentenças é realizada levando em consideração aspectos sintáticos definidos pela especificação da entrada, a gramática. Por questões de otimização são utilizados critérios de cobertura para limitar a quantidade de testes sem diminuir a sua qualidade. Nossa abordagem utiliza estes critérios no direcionamento da geração de maneira a produzir sentenças que satisfaçam um critério de cobertura especifico. A abordagem apresentada se baseia na utilização da linguagem Lua, se apoiando fortemente em seus recursos de corotinas e construção dinâmica de funções. Com estes recursos, propomos uma implementação compacta e simples que pode ser otimizada e controlada de formas variadas, com o intuito de buscar a satisfação dos diferentes critérios de cobertura implementados. Para tornar simples o uso de nossa ferramenta foi adotada a notação EBNF para a especificação das entradas. O seu parser foi especificado na ferramenta Meta-Environment por esta favorecer a rápida prototipação
Geração de casos de teste a partir de especificações B
(Universidade Federal do Rio Grande do Norte, 2010-03-29) Souza, Fernanda Monteiro de; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; ; http://lattes.cnpq.br/5425053595403848; Coelho, Roberta de Souza; ; http://lattes.cnpq.br/9854634275938452; Mota, Alexandre Cabral; ; http://lattes.cnpq.br/2794026545404598; Oliveira, Marcel Vinicius Medeiros; ; http://lattes.cnpq.br/1756952696097255
Com o crescente aumento da complexidade dos sistemas de software, há também um aumento na preocupação com suas falhas. Essas falhas podem causar prejuízos financeiros e até prejuízos de vida. Sendo assim, propomos neste trabalho a minimização de falhas através de testes em softwares especificados formalmente. A conjunção de testes e especificações formais vem ganhando força na academia principalmente através dos TBM (Testes Baseados em Modelos). O desenvolvimento de software a partir de especificações formais, quando todo o processo de refinamento é feito rigorosamente, garante que o que está especificado será implementado na aplicação. Sendo assim, a implementação gerada a partir destas especificações iria retratar fielmente o que estaria especificado. Mas nem sempre a especificação é refinada até o nível de implementação e geração de código, e nesses casos os testes gerados a partir da especificação tendem a encontrar falhas. Adicionalmente, a geração dos chamados testes inválidos , ou seja, testes que exercitem cenários da aplicação que não foram tratados na especificação, complementa mais significativamente o processo de desenvolvimento formal. Sendo assim, neste trabalho é proposto um método para geração de testes a partir de especificações formais B. Este método foi estruturado em pseudo-código. O método se baseia na sistematização das técnicas de testes caixa preta da análise do valor limite, particionamento de equivalência, bem como da técnica dos pares ortogonais. O método foi aplicado em uma especificação B e foram geradas máquinas B de teste que geram casos de teste independentes de linguagem de implementação. Com o intuito de validação do método, os casos de teste foram transformados manualmente em casos de teste do JUnit e a aplicação, criada a partir da especificação B, e desenvolvida em Java foi testada. Foram encontradas falhas com a execução dos casos de teste JUnit
Geração de interfaces de usuário de sistemas Web para múltiplos dispositivos com o uso de componentes de IU
(Universidade Federal do Rio Grande do Norte, 2007-08-20) Sousa, Lirisnei Gomes de; Leite, Jair Cavalcanti; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4782411P6; ; http://lattes.cnpq.br/5317953035421833; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; Santos, Celso Alberto Saibel; ; http://lattes.cnpq.br/7614206164174151
Este trabalho apresenta um processo de geração de protótipos de Interfaces de Usuário (IU) para software que tem como plataforma operacional um navegador Web. Este processo faz o uso de componentes de interface de usuário mais complexos que os elementos HTML. Para descrever estes componentes mais complexos este trabalho sugere o uso da linguagem XICL (eXtensible User Interface Components Language). A XICL é uma linguagem, baseada em XML, para a descrição de componentes de IU e de IUs. A XICL permite reusabilidade e extensibilidade no desenvolvimento de interfaces de usuários. Foram desenvolvidos dois compiladores, um que gera código XICL a partir de código IMML (Interactive Message Modeling Language) e outro que a partir de XICL gera DHTML
Geração de testes a partir de gramáticas: áreas de aplicação
(Universidade Federal do Rio Grande do Norte, 2013-12-13) Ramalho, Viviane de Menezes; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; ; http://lattes.cnpq.br/3208954190963847; Aquino Júnior, Gibeon Soares de; ; Machado, Patrícia Duarte de Lima; ; http://lattes.cnpq.br/2495918356675019
O trabalho proposto por Cleverton Hentz (2010) apresentou uma abordagem para definição de testes a partir da descrição formal das entradas do programa. Considerando que alguns programas podem ter suas entradas formalizadas através de gramáticas, como é o caso dos compiladores, é comum o uso de gramáticas livres de contexto para especificar o conjunto de entradas válidas. No trabalho original foi desenvolvida LGen, uma ferramenta que consiste na geração automática de testes para compiladores. No presente trabalho identificamos tipos de problemas recorrentes em diferentes áreas, onde gramáticas são usadas para descrevê-los, como por exemplo, para especificar configurações de software, e que são situações potenciais para o uso de LGen. Além disso, realizamos estudos de caso com gramáticas de domínios diferentes e a partir destes estudos foi possível avaliar o comportamento e o desempenho de LGen durante o processo de geração das sentenças, avaliando aspectos como tempo de execução, quantidade de sentenças geradas e satisfação de critérios de cobertura disponíveis em LGen
JCML - Java Card Modeling Language: Definição e Implementação
(Universidade Federal do Rio Grande do Norte, 2007-09-06) Souza Neto, Plácido Antônio de; Moreira, Anamaria Martins; Costa, Umberto Souza da; ; http://lattes.cnpq.br/9526809466920084; ; http://lattes.cnpq.br/5861361541278876; ; http://lattes.cnpq.br/3641504724164977; Musicante, Martin Alejandro; ; http://lattes.cnpq.br/6034405930958244; Borba, Paulo Henrique Monteiro; ; http://lattes.cnpq.br/9395715443254344
Métodos formais poderiam ser usados para especificar e verificar software on-card em aplicações Java Card. O estilo de programação para smart cards requer verificação em tempo de execução para condições de entrada em todos os métodos Java Card, onde o objetivo principal é preservar os dados do cartão. Projeto por Contrato, em particular, a linguagem JML, é uma opção para este tipo de desenvolvimento e verificação, pelo fato da verificação em tempo de execução ser parte da implementação pela JML. Contudo, JML e suas respectivas ferramentas para verificação em tempo de execução não foram projetadas com o foco nas limitações Java Card, sendo, dessa forma, não compatíveis com Java Card. Nesta dissertação, analisamos o quanto esta situação é realmente intrínseca às limitações Java Card e, se é possível re-definir a JML e suas ferramentas. Propomos requisitos para uma nova linguagem, a qual é compatível com Java Card e apresentamos como o compilador desta linguagem pode ser construído. JCML retira da JML aspectos não definidos em Java Card, como por exemplo, concorrência e tipos não suportados. Isto pode não ser o bastante, contudo, sem o esforço em otimização de código de verificação gerado pelo compilador, não é possível gerar código de verificação para rodar no cartão. O compilador JCML, apesar de ser bem mais restrito em relação ao compilador JML, está habilitado a gerar código de verificação compatível com Java Card, para algumas especificações lightweight. Como conclusão, apresentamos uma variante da JML compatível com Java Card, JCML (Java Card Modeling Language), com uma versão de seu compilador
JCML: A specification language for the runtime verification of Java Card programs
(Elsevier, 2010-03-19) Moreira, Anamaria Martins; Costa, Umberto Souza da; Musicante, Martin A.; Souza Neto, Plácido A.
KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B
(Universidade Federal do Rio Grande do Norte, 2012-02-10) Santos, Simone de Oliveira; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/5861361541278876; ; http://lattes.cnpq.br/5922034090094531; Déharbe, David Boris Paul; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5; Gheyi, Rohit; ; http://lattes.cnpq.br/2931270888717344
O desenvolvimento de aplicações para smart cards requer um alto grau de confiabilidade. Métodos formais fornecem meios para que esta confiabilidade seja alcançada. O método e a ferramenta BSmart fornecem uma contribuição para que o desenvolvimento para smart cards seja feito com o auxílio do método formal B, gerando código Java Card a partir de especificações B. Para que o desenvolvimento com o BSmart seja efetivamente rigoroso sem sobrecarregar o usuário do método é importante que haja uma biblioteca de componentes reutilizáveis feitos em B. O KitSmart tem como objetivo prover esse auxílio. Um primeiro estudo sobre a composição dessa biblioteca foi tema de uma monografia de graduação do curso de Bacharelado em Ciência da Computação da Universidade Federal do Rio Grande do Norte, feita por Thiago Dutra em 2006. Esta primeira versão do kit resultou na especificação dos tipos primitivos permitidos em Java Card (byte, short e boolean) em B e a criação de componentes reutilizáveis para o desenvolvimento de aplicações. Esta dissertação provê o aperfeiçoamento do KitSmart com o acréscimo da especificação da API Java Card em B, e um guia para o desenvolvimento de novos componentes. A API Java Card especificada em B, além de estar disponível para ser usada no desenvolvimento de projetos, serve como documentação ao especificar restrições de uso para cada classe da API. Os componentes reutilizáveis correspondem a módulos para manipulação de estruturas específicas, como data e hora, por exemplo. Estes tipos de estruturas não estão disponíveis em B ou Java Card. Os componentes reutilizáveis para Java Card são gerados a partir das especificações verificadas formalmente em B. O guia contém informações de consulta rápida para especificação de diversas estruturas e como algumas situações foram contornadas para adaptar a orientação a objetos ao Método B. Este trabalho foi avaliado através de um estudo de caso feito com a ferramenta BSmart que faz uso da biblioteca KitSmart. Neste estudo de caso, é possível ver a contribuição dos componentes em uma especificação B. Este kit deverá ser útil tanto para usuários do método B como para desenvolvedores de aplicações Java Card em geral
A linguagem de especificação algébrica CASL e o Tipo de Dados Intervalos
(Universidade Federal do Rio Grande do Norte, 2004-04-16) Lopes, Katiane Ribeiro; Santiago, Regivan Hugo Nunes; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4790032Z4; http://lattes.cnpq.br/9992509167692509; Campos, Marcília Andrade; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4783192D1; Moreira, Anamaria Martins; http://lattes.cnpq.br/5861361541278876
Na computação científica é necessário que os dados sejam o mais precisos e exatos possível, porém a imprecisão dos dados de entrada desse tipo de computação pode estar associada às medidas obtidas por equipamentos que fornecem dados truncados ou arredondados, fazendo com que os cálculos com esses dados produzam resultados imprecisos. Os erros mais comuns durante a computação científica são: erros de truncamentos, que surgem em dados infinitos e que muitas vezes são truncados", ou interrompidos; erros de arredondamento que são responsáveis pela imprecisão de cálculos em seqüências finitas de operações aritméticas. Diante desse tipo de problema Moore, na década de 60, introduziu a matemática intervalar, onde foi definido um tipo de dado que permitiu trabalhar dados contínuos,possibilitando, inclusive prever o tamanho máximo do erro. A matemática intervalar é uma saída para essa questão, já que permite um controle e análise de erros de maneira automática. Porém, as propriedades algébricas dos intervalos não são as mesmas dos números reais, apesar dos números reais serem vistos como intervalos degenerados, e as propriedades algébricas dos intervalos degenerados serem exatamente as dos números reais. Partindo disso, e pensando nas técnicas de especificação algébrica, precisa-se de uma linguagem capaz de implementar uma noção auxiliar de equivalência introduzida por Santiago [6] que ``simule" as propriedades algébricas dos números reais nos intervalos. A linguagem de especificação CASL, Common Algebraic Specification Language, [1] é uma linguagem de especificação algébrica para a descrição de requisitos funcionais e projetos modulares de software, que vem sendo desenvolvida pelo CoFI, The Common Framework Initiative [2] a partir do ano de 1996. O desenvolvimento de CASL se encontra em andamento e representa um esforço conjunto de grandes expoentes da área de especificações algébricas no sentido de criar um padrão para a área. A dissertação proposta apresenta uma especificação em CASL do tipo intervalo, munido da aritmética de Moore, afim de que ele venha a estender os sistemas que manipulem dados contínuos, sendo possível não só o controle e a análise dos erros de aproximação, como também a verificação algébrica de propriedades do tipo de sistema aqui mencionado. A especificação de intervalos apresentada aqui foi feita apartir das especificações dos números racionais proposta por Mossakowaski em 2001 [3] e introduz a noção de igualdade local proposta por Santiago [6, 5, 4]
Local livelock analysis of component-based models
(2016-08-12) Conserva Filho, Madiel de Souza; Oliveira, Marcel Vinicius Medeiros; Cavalcanti, Ana Lucia Caneca; ; ; http://lattes.cnpq.br/1756952696097255; ; Mota, Alexandre Cabral; ; http://lattes.cnpq.br/2794026545404598; Moreira, Anamaria Martins; ; http://lattes.cnpq.br/2363575151206774; Ribeiro, Leila; ; Musicante, Martin Alejandro; ; http://lattes.cnpq.br/6034405930958244
O uso crescente de sistemas complexos exige cada vez mais um maior investimento de recursos no desenvolvimento de software para garantir a confiabilidade dos mesmos. Para lidar com esta complexidade, abordagens composicionais podem ser utilizadas no desenvolvimento de sistemas de software, possibilitando a integração e a reutilização de componentes existentes. Entretanto, a fim de garantir o sucesso desta abordagem, é essencial confiar no comportamento dos componentes e, além disso, nos sistemas que são desenvolvidos utilizando essa estratégia, uma vez que falhas podem ser introduzidas se a composição não assegurar propriedades importantes. Problemas podem surgir quando dois ou mais componentes são integrados pela primeira vez. Esta situação é ainda mais relevante quando um grupo de componentes trabalha em conjunto a fim de executar determinadas tarefas, especialmente em aplicações críticas, onde podem surgir problemas clássicos, como livelock. Esta tese de doutorado apresenta uma estratégia local para garantir ausência de livelock, por construção, em sistemas síncronos modelados com a notação padrão de CSP. A nossa técnica é baseada na análise local das mínimas sequências que levam o processo CSP ao seu estado inicial. O uso de técnicas locais evita a explosão do espaço de estados gerado pela integração dos componentes. A verificação destas condições locais utilizam metadados que permitem armazenar resultados parciais das verificações, reduzindo o esforço durante a análise. A abordagem proposta também pode ser aplicada para verificar ausência de livelock em modelos que realizam comunicações assíncronas. Neste caso, analisamos o modelo de componentes BR IC, cujo comportamento dos componentes é representado por um processo CSP. A fim de realizar esta verificação, consideramos duas versões para BR IC: BR IC , o qual realiza composições assíncronas através de buffers finitos, e BR IC¥ no qual a assincronicidade é realizada através de buffers infinitos. Estas duas abordagens foram analisadas porque a possibilidade de introduzir livelock em sistemas assíncronos depende diretamente da finitude do buffer. As técnicas propostas para garantir ausência de livelock em CSP e BR IC foram avaliadas através de três estudos de caso: o escalonador de Milner e duas variações do jantar dos filósofos. Uma versão apresenta um sistema livre de livelock, e a outra apresenta um sistema com livelock. Neste estudo, avaliamos a nossa abordagem em comparação com outras duas técnicas para verificação de ausência de livelock, a análise global tradicional do FDR e a análise estática de livelock do SLAP. Este estudo comparativo demonstra que a nossa estratégia pode ser aplicada como uma alternativa para a verificação de ausência de livelock em grandes sistemas.

SIGAA

Navegando por Autor "Moreira, Anamaria Martins"