- Bacharelado em Ciência da Computação - IME - USP
- camila.achutti@gmail.com
- Currículo Lattes
- BLOG: Mulheres na Computação
Nasci em 21 de dezembo de 1991, e já tive companhia mesmo nesse momento solitário para muitos. Comigo nasceu uma menina igualzinha a mim. Sim, eu tenho uma irmã gêmea. Cresci em São Paulo, mas me divertia mesmo em Sorocaba, contava os dias para que chegasse sexta e pudesse ir para chácara ser criança e estar cercada de primos, tios e tias. Enfim, fui uma criança feliz.
O tempo passou rápido e quando vi já tinha lá meus 17 anos e me vi tendo que tomar uma das decisões mais difíceis da minha vida: O que eu vou ser quando crescer?
Muitos me perguntam o que eu estou fazendo na Ciência da Computação. Sempre gostei muito de matemática e física, mas também gosto de escrever e me fazer entender através das palavras. Acho que tudo começou quando meu pai ainda jovem aprendeu a programar e acabou indo trabalhar em tecnologia. Imaginem só o que era para uma garotinha ver o homem que ela tanto admirava ditar, as vezes por telefone e de madrugada, o que hoje eu sei se tratar de código em COBOL, uma língua totalmente desconhecida, mas que magicamente resolvia problemas. Minha vontade era um dia entender essa tal língua. Queria ser como ele.
E com 18, me esforcei para ter a chance de estudar numa grande universidade aquilo que me faria entender tudo aquilo, ou melhor, quase tudo.
Entrei no IME em 2010, com 18 anos e muitos planos na cabeça. Logo descobri que aquele era o lugar onde, provavelmente, conheceria muitos dos amigos que levaria para o resto da minha vida e aprenderia coisas totalmente novas. Acertei. Descobri um mundo de possibilidades.
Aprendi a programar, aprendi que não sabia o que era matemática e física de verdade, entrei para atlética, joguei vôlei e basquete, fiz festa e estudei noites a fim, descobri que gosto de front-end e odeio maratona. Descobri que programar é uma arte, é concretizar uma ideia, é resolver um problema, é melhorar a vida das pessoas. Consegui atingir muitas pessoas com as minhas palavras e mudei a vida de algumas delas. Conheci pessoas maravilhosas, grandes mestres e aprendizes dedicados. Viajei, conheci outros continentes, conheci meus autores preferidos e os meus melhores amigos. Trabalhei e estudei como nunca antes. Fui estagiária, voluntária e bolsista FAPESP. Fui feliz.
A graduação já está acabando e em dezembro já não preciso passar meus dias no IME, mas acho que vou optar por isso. Quero sim fazer pós-graduação e aprender mais, muito mais. Dizer que quero seguir carreira acadêmica, empreender, inovar, trabalhar no banco, numa grande empresa ou numa startup pode não passar de mentira, não tenho certeza sobre isso ainda, essas são apenas algumas das infinitas possibilidades que o universo pode me oferecer.
Verificação e validação de sistemas críticos reais.
Existe atualmente uma crescente preocupação mundial com a qualidade dos softwares, sendo ele crítico ou não, já que a evolução dos sistemas computacionais aumentou exponencialmente e, portanto, as funcionalidades implementadas neles são cada vez mais completas e complexas, exigindo que o desenvolvedor e o cliente confiem na correção completa do projeto.
Outro motivo para tamanha preocupação são os grandes investimentos na melhoria dos processos de desenvolvimento de software. Quando tratamos de softwares críticos essa preocupação é ainda maior. Sendo assim, o investimento em técnicas para validação e verificação de softwares é cada vez maior e imprescindível.
Esse projeto vem então explorar a temática da qualidade de softwares em sistemas críticos através do estudo e aplicação de métodos de verificação sobre um sistema real da área espacial. Neste projeto, um estudo sobre a especificação formal de um sistema crítico será realizada para então desenvolver a implementação do projeto na linguagem Java e aplicar técnicas de verificação sobre o sistema desenvolvido. Para tanto, o verificador de modelos Java Pathfinder desenvolvido pela NASA, será utilizado já que ele tem sido amplamente desenvolvido pela comunidade científica. O objetivo é explorar todos os passos de uma verificação apropriados para um software de missão crítica e contribuir com a comunidade científica com um estudo sobre verificação formal de programas de sistemas críticos reais.
O caso real a ser desenvolvido será um software embarcado espacial, pois a necessidade de verificação e validação é ainda mais intensificada quando se trata de sistemas espaciais. Os resultados deste trabalho têm aplicação direta no mundo real e a experiência com tal desenvolvimento trará benefícios sobre a avaliação do uso de técnicas formais ao longo do desenvolvimento de um sistema real.
Como principal objetivo do projeto temos os estudos de como é feita a verificação de um sistema de missão crítica e do desenvolvimento formal de um software espacial embarcado. Além disso, a familiarização com uma ferramenta de destaque para esse fim, o JPF, para sua efetiva verificação. Tentando aproximar ao máximo da maneira como isso seria feito na realidade, por isso o uso de um software real e de uma ferramenta para esse fim já bastante explorada pela comunidade científica. Busca-se também com esse projeto, um estudo das especificações do software que será verificado, de maneira mais formal, visando uma compreensão ainda mais completa do sistema e do cenário crítico em que está inserido.
Inicialmente, haverá a familiarização com o software a ser verificado e o contexto em que está inserido para a criação de uma visão global do problema que o software se propõe a resolver. Em seguida, haverá a verificação das especificações do software já documentadas. Essa parte envolverá um estudo formal dessas especificações e a avaliação da correção das mesmas.
A etapa seguinte é a modelagem dos objetos e a adequação do software para a verificação com o JPF, ou seja, será feita uma implementação do software na linguagem Java. A etapa final será a efetiva verificação do mesmo usando a ferramenta. Essa etapa possibilita um maior entendimento da ferramenta, pois poderemos entender, na prática, o modelo de operação desse verificador.
O trabalho de formatura tem previsão de duração de aproximadamente 8 meses, com os últimos 5 meses em ritmo bastante acelerado. As atividades deverão seguir a sequência indicada no cronograma apresentado na figura abaixo, sendo levadas em conta as seguintes etapas:
Estudos Preliminares: aprofundamento nos estudos de verificação de software, métodos formais e da ferramenta JPF.
Estudo do software e seus elementos críticos: nesta etapa do projeto será realizado um estudo aprofundado do software de forma a isolar partes do software a ser efetivamente implementado juntamente com os elementos críticos que serão verificados. A partir desse estudo, poderemos dimensionar a parte do projeto a ser implementada dados os elementos críticos a serem verificados. Ao final desta etapa teremos um modelo abstrato de todo o software, as partes do mesmo que serão implementadas, e um conjunto dos elementos críticos a serem verificados.
Modelagem e implementação do software: modelagem de objetos e adequação do software para uso da ferramenta JPF. Juntamente com a modelagem do sistema, um ambiente de simulação será criado para ativar o funcionamento do sistema embarcado, de forma que ele seja executado em ambiente simulado.
Verificação do software: para a tarefa de verificação, propriedades sobre os elementos críticos devem ser definidas e escritas na forma de propriedades a serem submetidas ao JPF. As sub-tarefas envolvidas são o estudo das propriedades padrão a serem definidas e adaptação de tais propriedades para o JPF.
Avaliação da verificação e redação da monografia/pôster/apresentação como tarefa final será realizada a avaliação das facilidades e dificuldades da verificação formal de programas Java com o uso do JPF, escrita da monografia e preparação do pôster e da apresentação.
Diante desse calendário as atividades deste primeiro período envolveram:
1. Estudos preliminares do contexto do programa em teste e a ferramenta JPF.
2. Estudo do software e seus elementos críticos.
3. Modelagem e implementação inicial do sistema.
O resumo destas atividades organizado por tópicos será feito abaixo. Estes abrangem e detalham o acompanhamento das metas propostas no cronograma proposto.
Os trabalhos iniciais se concentraram principalmente no estudo da documentação do Java Pathfinder disponibilizada na sua página na web e na sua correta instalação no ambiente de desenvolvimento escolhido. Tal ambiente de desenvolvimento já descrito em detalhes acima compreende o uso da IDE NetBeans 7.2.1 para programação em Java, para que assim fosse possível ter uma noção geral da totalidade dela para tirarmos o máximo proveito, procuramos conhecer todas as características relativas ao Java Pathfinder. Estudando desde os objetivos que levaram ao seu desenvolvimento, passando por sua noção geral de sua implementação, até a aplicação da ferramenta final propriamente dita.
Somente a partir do correto conhecimento da ferramenta é que pudemos caracterizar como deveria ser um programa que tirasse proveito de todo os conceitos implementados em tal ferramentas. Sem tal preocupação poderíamos não aproveitar a ferramenta e acabar subjulgando seu potencial para verificação de programas.
Além disso, o próprio estudo do Java Pathfinder provocou o estudo de outros temas, já que seu desenvolvimento envolveu muitos conceitos e tecnologias diferentes. Assim, o estudo completo desta ferramenta consumiu pelo menos um mês, mas foi de suma importância para o desenvolvimento do trabalho e para a obtenção dos resultados imparciais e corretos.
Agora, com a clara noção das qualidades e deficiências do Java Pathfinder, pudemos dirigir nossos estudos e esforços para a produção de um software adequado de acordo com os objetivos do trabalho, e certificar a viabilidade das próximas atividades.
Nesta segunda fase do trabalho, que se estendeu aproximadamente até o final de abril foram realizados o estudo dos 2 principais documentos, cedidos pelo INPE, relacionados ao software que será implementado e testado. Sendo eles os seguintes: Especificação Técnica do software - QOO-ETS-V03 e Documento do Projeto do Software - Arquitetura POO - QOO-DPSW-V05
Diante do estudo dos mesmos, para simular o funcionamento do software, faremos o desenvolvimento de dois produtos independentes, um é o sistema SWPDC ( Software Piloto Embarcado no Payload Data Handling Computer) propriamente dito, implementado em Java e nas especificações descritas nos documentos citados acima. Tal sistema estará preparado para rodar e obter dados de um segundo produto totalmente independentemente para simular o PDC ( Payload Data Handling Computer), que na sua essência é quem recupera dados dos sensores (hardwares) e os provê para o software. Este simulará o acontecimentos de eventos que o SWPD deve saber lidar e que ocorreriam no ambiente real da aplicação, ou seja num ambiente especial onde um satélite estará inserido.
Além disso, com o estudo desses documentos foi possível perceber duas abordagens diferentes feitas pelo sistema em questão que seram resumidamente contextualizadas abaixo:
Fragmentação por Modos de Operação: mapeia o sistema de um ponto de vista mais subjetivo pensando nos possíveis estados do sistema. Distinguem-se quatro modos de operação, sendo eles:
-Diagnóstico: responsável pela verificação da "saúde" do sistema como um todo, verificando tanto se os sensores estão funcionando corretamente quanto se surgiu algum erro no software;
-Nominal: modo de operação de digestão dos dados obtidos pelos sensores, realização de cálculos e construção dos relatórios (produtos finais do sistema)
-Segurança: momento de recebimento dos dados externos e também momento de isolamento e resolução de problemas advindos de possíveis bugs encontrados.
-Inicialização: primeiro estado assumido pelo sistema, responsável pela inicializacão de todos os componentes e dá início aos primeiros procedimentos do sistema.
Fragmentação por Componentes: traz uma abordagem mais baixo nível e tenta isolar componentes fortemente dependentes, visando obter uma estrutura modularizada que faz bastante sentido nos softwares de missão crítica. Tal abordagem reconhece cinco componentes distintos:
-Dados: responsável por todo gerenciamento de dados, desde seu armazenamento até sua formatação;
-Suporte: responsável por procedimentos como a inicialização de sensores e aquisição de dados dos mesmos;
-Estado: gerencia os modos de operação, toda tolerância a falhas e se necessário é o responsável por modificações nos paramêtros do software;
-Comunicação: atua no gerenciamento de todos os canais de comunicação entre os OBDH (On-Board Data Handling) e os EPPs (Event Pre-Processor);
-Serviços: responsável pela execução dos comandos recebidos da interface de comunicação com o OBDH chamando os componentes envolvidos na tarefa.
O maior objetivo desse estudo era identificar com quais desses fragmentos poderíamos começar a trabalhar, levando em conta também, quais produziriam um resultado mais satisfatório, sabendo que seria impossível implementar o sistema inteiro, que é bastante complexo e foi produto de diversos pesquisadores durante anos. Vale ressaltar que esta foi uma restrição já prevista e definida no projeto submetido.
Observando os modos de operação, percebe-se que escolher um deles para analisar e implementar não é a melhor maneira de começar e de obter um feedback rápido, pois um modo de operação envolve pequenas partes de todos os componentes do software que estariam incompletos e não produziriam o efeito desejado. Sendo assim, optar pelo desenvolvimento por componentes se mostrou a decisão mais adequada, pois assim teríamos um módulo completo implementado e independente do ponto-de-vista de funcionamento. Este aspecto é bastante interesante para a realização da verificação de maneira que essa não tenha que ser refeita neste módulo posteriormente com a implementação de novas funcionalidades do sistema.
Dentre os componentes, começar pelo de dados foi a opção feita por ser um dos principais componentes do sistema, já que é responsável pelo gerenciamento de dados, a qual é a funcionalidade central do SWPDC.
Com o conhecimento e decisões tomadas nessa fase, partimos para a modelagem do sistema e demos início à implementação. O produto desta fase de modelagem está ilustrado abaixo no UML simplificado do sistema:
Diante desta proposta, foi dado início ao detalhamento de cada uma das classes e a efetiva implementação das mesmas que será feito de maneira progressiva e incremental para obtermos objetos concretos de forma rápida. A primeira rodada de detalhamento e implementações foi das classes relacionadas ao gerenciamento de dados que se valiam de buffers simples no processo.
Os avanços obtidos nas classes estão ilustrados na figura abaixo:
A classe RelatoEvento teve sua implementação adiada, pois essa será feita na etapa de integração com o segundo produto, o Simulador_PDC.
Outra decisão tomada foi iniciar os testes mais robustos com os dados de temperatura, eles servirão de modelo para os próximos tipos de dados. Para realizar esses testes será necessária a implementação de uma classe que efetue e regularize a entrada desses dados nesse primeiro momento, ainda a título de testes de validação.
Parte Objetiva
1.Introdução
2.Motivação
3.Objetivos
4.Conceitos e Tecnologias
4.1. Verificação de Softwares Críticos
4.1.1. Métodos usados
4.1.2. Ferramentas existentes
4.2. Validação de Software Críticos
4.2.1. Métodos usados
4.2.2. Ferramentas existentes
5.Estudo do Caso: SWPDC e JPF
5.1. JPF
5.2. SWPDC
6.Análise dos Resultados Obtidos
6.1. SWPDC desenvolvido.
6.2. Verificação do sistema usando JPF.
7.Considerações finais
8.Referências bibliográficas
Parte subjetiva
1.Desafios e frustrações
2.Disciplinas cursadas relevantes para o desenvolvimento do TCC
3.Observações sobre a aplicação real de conceitos estudados
4.Próximos passos
[1] Ammann, Paul e Jeff Offutt: Introduction to Software Testing. Cambridge University Press, New York, NY, USA, 1a edição, 2008, ISBN 0521880386, 9780521880381.
[2] Baier, Christel e Joost Pieter Katoen: Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008, ISBN 026202649X, 9780262026499.
[3] Bertolino, Antonia: Software Testing Research and Practice. In 10th International Workshop on Abstract State Machines, páginas 1–21, 2003.
[4]Dwyer, Matthew B., George S. Avrunin e James C. Corbett: Patterns in property specifications for finite-state verification. In Proceedings of the 21st international conference on Software engineering, ICSE '99, páginas 411–420, New York, NY, USA, 1999. ACM, ISBN 1-58113-074-0. http://doi.acm.org/10.1145/302405.302672.
[5] Francez, Nissim: Program Verification. Addison Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1992, ISBN 0201416085.
[6]Hoare, Tony e Jay Misra: Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project. In Meyer, Bertrand e Jim Woodcock (editores): Verified Software: Theories, Tools, Experiments, volume 4171 de Lecture Notes in Computer Science, páginas 1–18. Springer Berlin / Heidelberg, ISBN 978-3-540-69147-1.
[7]Pasareanu, Corina S., Peter C. Mehlitz, David H. Bushnell, Karen Gundy-Burlet, Michael Lowry, Suzette Person e Mark Pape: Combining unit-level symbolic execution and system-level concrete execution for testing nasa software. In Proceedings of the 2008 international symposium on Software testing and analysis, ISSTA ’08, páginas 15–26, New York, NY, USA, 2008. ACM, ISBN 978-1-60558-050-0. http://doi.acm.org/10.1145/1390630.1390635.
[8] Santiago Júnior, Valdivino Alexandre de: SOLIMVA: A Methodology for Generating Model-Based Test Cases from Natural Language Requirements and Detecting Incompleteness in Software Specifications, 2011.
[9]Boehm, Barry W.: Software Engineering Economics. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1981, ISBN 0138221227.
[10] Delamaro, Márcio Eduardo, José Carlos Maldonado e Mario Jino: Introdução ao Teste de Software. Elsevier, 2007.
[11] Java PathFinder. http://babelfish.arc.nasa.gov/trac/jpf/. Acesso em: Jul. 2012.
[12] Woodcock, Jim, Peter Gorm Larsen, Juan Bicarregui e John Fitzgerald: Formal methods: Practice and experience. ACM Comput. Surv., 41(4):19:1{19:36, outubro 2009, ISSN 0360-0300. http://doi.acm. org/10.1145/1592434.1592436.