Ana Cristina Vieira de Melo.

Processo Fapesp:20/09850-0Platafroma IASMIN (Inteligência Artificial Soluções para Manufatura Inteligente)Pesquisador Associado dentro da linha de pesquisa: Interoperabilidade e Integração da CadeiaInstituição SedeInstituto de Pesquisas Tecnológicas do Estado de São Paulo S/A (IPT) Empresas ParceirasSiemens LtdaSiemens Infraestrutura E Indústria LtdaRobert Bosch LimitadaKlabin S.AFCA Fiat Chrysler Automoveis Brasil LtdaBraskem S.A Instituições ParceirasAssociação Parque Tecnológico de São José dos Campos/APQTEC/APQTECCentro Universitário FACENS/UNIFACENS/ACRTSEscola Politécnica/EP/USPInstituto de Matemática e Estatística/IME/USPFundação Parque Tecnológico Itaipu - Brasil/FPTI-BR/FPTI-BRInstituto de Ciência e Tecnologia de Sorocaba/ICTS/UNESPInstituto Tecnológico de Aeronáutica/ITAUniversidade Técnica Federal do Paraná - UTFPRUniversidade Federal de São Paulo/UNIFESPUniversidade Federal do ABC/UFABCAgência Unesp de Inovação/AUIN/UNESPUniversidade Estadual de Campinas / UNICAMP

Cooperação acadêmica; intercâmbio de estudantes de graduação e de pós-graduação.

Cooperação em projeto de pesquisa -Prof. Mauro Javier Jaskelioff e Alexandre Garcia de OliveiraUniversidad Nacional de Rosario- Argentina

Cooperação internacional para fins de co-orientação de doutoradoProf. Mauro Javier Jaskelioff

Cooperação acadêmica; intercâmbio de estudantes de graduação e de pós-graduação.

Cooperação acadêmica; intercâmbio de estudantes de graduação e de pós-graduação.

Cooperação acadêmica; intercâmbio de estudantes de graduação e de pós-graduação.

Programa de Estímulo ao Ensino de Graduação (PEEG) - 1 aluno
A disciplina necessita de um novo material didático no que diz respeito à implementação dos algoritmos básicos em Python. Esta monitoria será dedicada à implementação de cada um dos algoritmos básicos, juntamente com scripts de correção para fins didáticos. A linguagem Python está sendo adotada nesta disciplina pela primeira (turma Web). Então, faz-se necessário readaptar o material existente para a nova linguagem.

This Research Internship Abroad (BEPE) project is part of the Ph.D work under the São Paulo Research Foundation (FAPESP) process: 2011/01928-1. The main objective of the Ph.D work is to help software developers in applying formal verification in practice. To do this, we propose an approach that generates the corresponding source code of the system properties that should be verified to assure the software quality. This code generation will be guided by the test purposes derived from the system specification.

The main challenge of the Ph.D research is to synchronize the test purposes at implementation and specification levels in order to automate the properties code generation. To solve this problem, we have decided to make a theoretical work over this synchronization and then apply its results in practice using the Java PathFinder (JPF), a virtual machine that can be used as a model checker to verify Java programs.

In this BEPE project, we will focus on the application of the theoretical results in practice: we are going to proceed to the implementation of general properties templates in JPF. These templates will be used to automate the generation of properties code that a system must satisfy to guarantee its quality. And the generated property code will be registered in JPF so that it will be able to check whether the system satisfies this property or not. To validate the implementation of those JPF general properties templates, a set of tests for each property template must be created and executed.

Para que haja uma garantia de que o software desenvolvido é confiável, atividades de testes e verificação formal devem ser realizadas. Contudo, a viabilidade prática de execução dessas atividades depende de métodos de desenvolvimento que explorem o uso conjunto das técnicas, bem como de ferramentas que auxiliem sua realização, uma vez que a execução de ambas constitui um alto custo para o desenvolvimento do software.

Tendo em vista a necessidade de facilitar a realização de testes e verificação formal nos sistemas de software de missão crítica, este projeto se propõe a desenvolver uma metodologia integrada, com apoio de ferramentas computacionais, para a verificação formal e testes desses sistemas, levando em conta a redução dos custos das atividades de Verificação & Validação (V&V). Os principais objetos de estudo que constituem um desafio científico ao projeto é a exploração da complementariedade das duas atividades de forma transversal ao desenvolvimento de sistemas críticos para possibilitar o uso conjunto dessas atividades e avaliar o custo de sua aplicação.

Programa de Estímulo de Ensino de Graduação (PEEG) - 2 alunos selecionados
A disciplina necessita de um novo material didático no que diz respeito à implementação dos conceitos fundamentais de programação. Esta monitoria será dedicada à implementação de cada um dos conceitos para uma linguagem de programação a ser utilizada para fins didáticos. A partir dessas novas implementações, os alunos da disciplina desenvolverão os trabalhos práticos.

Com a presença cada vez maior de sistemas computacionais e novas tecnologias no cotidiano das pessoas, garantir que eles não falhem e funcionem corretamente tornou-se algo de extrema importância. Além de indicar a qualidade do sistema, assegurar seu bom funcionamento é essencial para se evitar perdas, desde financeiras até de vidas.

Uma das técnicas utilizadas para esta finalidade é a chamada verificação formal de programas. A partir da especificação do sistema, descrita numa linguagem formal, são definidas propriedades a serem satisfeitas e que certificariam a qualidade do software. Estas propriedades devem então ser implementadas para uso num verificador, que é a ferramenta responsável por executar a verificação e informar quais propriedades foram satisfeitas e quais não foram, indicando aos desenvolvedores os possíveis locais com código incorreto no sistema. A desvantagem do uso da verificação formal é, além do seu alto custo, a necessidade de haver pessoas com treinamento em linguagens e métodos formais. Ademais, a implementação de propriedades relativas a um sistema em particular para uso num verificador é uma tarefa bastante complexa e de alto custo. 

Para auxiliar os desenvolvedores na utilização da verificação formal em programas escritos em Java, este trabalho propõe a geração de código de propriedades para uso direto no verificador, a partir de casos de testes derivados dos requisitos formais de sistemas.

A cada dia a internet vem sendo mais utilizada pelas empresas para divulgar seus produtos, conhecer melhor ou conquistar mais clientes. Com o surgimento da WEB 2.0 bem como a facilidade de acesso a banda larga, cada vez mais usuários colaboram gerando conteúdo na web. O sucesso de um projeto web depende muito da aceitação dos usuários que o utilizam. Métodos de avaliação de usabilidade têm sido empregados para garantir uma boa qualidade desses produtos. Esse trabalho de pesquisa propõe um estudo e comparação dos métodos para avaliação de usabilidade para a WEB 2.0.

Este convênio tem como objeto a cooperação acadêmica através do intercâmbio de docentes e pesquisadores, bem como de estudantes de pós-graduação entre o grupo de Engenharia de Software e Métodos Formais da USP (São Paulo) e o Laboratoire de Recherche en Informatique (LRI) da Université Paris-Sud 11.

A colaboração proposta tem como objetivo principal o desenvolvimento conjunto de pesquisas científicas em tópicos relacionados ao desenvolvimento formal de sistemas de software, dentre os quais teste e verificação formal de sistemas. Dentro desta área de pesquisa, em particular, definimos como projeto inicial: ?Verificação de sistemas distribuídos e móveis orientado por informação de simulação e escolha estatística de testes?. No âmbito deste projeto, o grupo de Engenharia de Software e Métodos Formais da USP (São Paulo) tem desenvolvido técnicas de verificação e simulação de sistemas distribuídos e móveis, enquanto o Laboratoire de Recherche en Informatique (LRI) da Université Paris-Sud 11 tem aplicado métodos estatísticos para a escolha de conjuntos de testes relevantes. Desta forma, a colaboração propiciará o desenvolvimento de métodos estatísticos para a escolha de informação de simulação dos sistemas distribuídos e móveis que sejam relevantes à verificação de propriedades sobre tais sistemas.

 (Proc. 08.1.01153.45.4)

Aplicativos Web Services oferecem serviços através de uma rede e são
cada vez mais utilizados para integrarem sistemas e soluções das
mais variadas complexidades. Os Web Services estão sendo cada vez
mais usados em sistemas altamente complexos, principalmente com a
chegada da web 2.0. Em alguns cenários com maior criticidade, a
confiança no Web Service passa a ser um fator de fundamental
importância. Atualmente, uma das suas principais características é o
fato de que sua comunicação é feita em um ambiente com baixa
confiabilidade, como a Internet, cujos protocolos de comunicação nem
sempre provêm as garantias necessárias de funcionamento correto. De
fato, isso é uma barreira que impede que empresas invistam em
aplicativos críticos que dependam de integração com Web services.

Com o objetivo de garantir um serviço de qualidade, a comunidade
acadêmica e até mesmo a indústria têm despendido um grande esforço
para definir modelos de Qualidade de Serviço especificamente para
Web Services, e estudar alternativas para o problema de forma a
aumentar a confiabilidade nos serviços oferecidos por eles. Estudar
a fundo uma possível solução requer conhecimento sobre as diversas
alternativas já pesquisadas e sobre as tendências tecnológicas que
prometem ajudar a suprir as atuais necessidades. Assim, a proposta
do presente estudo é analisar os principais problemas relacionados à
confiabilidade de Web Services, com o objetivo de obter as
informações necessárias para prover subsídios de como implementar
soluções adequadas a situações específicas. Além disso, o estudo
pode servir como referência para que sejam pesquisadas novas
soluções.

Multi-agent systems are useful to model complex systems in
which the entities to be studied can be decomposed into several
interacting pieces called agents. Human societies, computer
networks, neural tissue and cell biology are examples of systems
that can be seen from this perspective. There are a number of ways
that such modelling can be done, ranging from purely formal
approaches to entirely experimental ones. Our work, which is
situated between these two extremes, focuses on employing simulation
in order to study such multi-agent models. That is, we specify the
agents as computer programs and run interesting scenarios in a
simulator, hoping to learn something about the model after several
simulations. As one would expect, simple simulation approaches of
this kind are already in use nowadays. However, they are also rather
naive with respect to automated analysis of simulation results.
Typically, one merely runs the simulation several times and collect
statistics about some variables. Clearly, though, as the simulation
runs in a computer and is specified as a program, it must be
possible to perform many kinds of automated analyses beyond such
simple statistics compilation. Our work, thus, focuses on this
issue: what kind of algorithms, theories and software infrastructure
are required in order to have a simulator capable of helping an
experimenter discover useful information about a simulation model.
We believe that many ideas and techniques from the Formal Methods
and Software Testing communities can be successfully adapted to this
context. The crucial insight here is that simulations can be seen as
incomplete explorations of state-spaces, and as such we can hope,
for example, to apply approximate versions of Model Checking and
other techniques of automated reasoning. To fulfill this vision, we
intend to develop both the necessary theory and its implementation
as a simulator. We expect, thus, to create a technology that can
signific

Com o crescimento e popularização do mercado de componentes, muitos
fornecedores de software têm se especializado no desenvolvimento e
comercialização de componentes que atendam às necessidades
específicas dos desenvolvedores de sistemas. Estes componentes são
mais conhecidos como Commercial-Off-The-Shelf .

Entretanto, a montagem de sistemas corporativos que sejam confiáveis
e tolerantes a falhas, a partir da integração de componentes
comerciais, tem-se mostrado uma atividade relativamente complexa. Garantir que esta integração não falhe passou a ser algo imprescindível.

Com o objetivo de definir quais requisitos são necessários para estabelecer um bom teste do software, definem-se os critérios de teste. Mesmo considerando o direcionamento da escolha de conjuntos de testes a serem realizados a partir dos critérios, tais conjuntos são, na sua maioria, ainda muito complexos. Uma outra abordagem para garantir o funcionamento do software como inicialmente especificado, são as técnicas de verificação formal de programas, as quais garantem que os programas funcionam de acordo com a especificação ou atendem a um conjunto de propriedades relevantes. 

A viabilidade prática de testes de software depende de mecanismos e ferramentas que auxiliem esta atividade, de forma a automatizar a geração de casos e dados de testes a serem aplicados. Por outro lado, a aplicação prática de verificadores formais em linguagens de programação depende da predefinição de propriedades, já que os "desenvolvedores" de software, em geral, não possuem treinamento adequado para definir novas propriedades. Além disso, faz-se necessário o uso conjunto de ferramentas de ambas as atividades para
que sejam exploradas suas complementariedades. Este projeto de Mestrado se propõe a desenvolver um ambiente integrado para a verificação e teste de protocolos para a coordenação do comportamento execepcional de componentes.

Component-based software is one of the reuse approaches successfully
used. The task of developing software components can be seen from two
different perspectives. One that would take care of building
components useful in many different situations, and another that
would develop the final software using these reusable components.
Naturally, technology alone does not guarantee the creation of
reusable components. Truly component-oriented approaches require
methods that can define what kind of entities the components must
represent, how they are composed and how such compositions are to be
employed. Having all this together to end up with a set of
components easily built and that can be reused in an appropriate way
is not very straightforward.

To make components construction more cost-effective and of a better
quality, the model-driven development can be adopted. In this case,
a design model language is required for components design, together
with a code generation mechanism. Booster is a design
language developed at the University of Oxford (UK) for components
construction via code generation. It is an object-oriented language
based on formal methods, namely B and Z, that is actually able to
generate components under the contexts of sequential composition. In
practice, however, component-based software naturally encompass
contexts in which components are concurrently composed instead of
purely sequential.

This project is about a study on how to improve the model-driven
components development with concurrent composition. From a
theoretical point-of-view, a study on the abstraction level for
specifying, through formal means, the required and provided
interfaces of components must be carried on to end up with a model
from which programs code can be generated. Also, mechanisms for
components orchestration in the context of concurrent composition
must be developed in order to provide an architecture and a
corresponding protocol to coordi

Com a popularização das redes de computadores e dos gerenciadores de
banco de dados, os sistemas de informação tornaram-se elementos
essenciais de suporte a processos de negócio de empresas
fornecedoras de serviços indispensáveis à sociedade, tais como automação
bancária e telefonia. Esses sistemas modernos são também
considerados de missão crítica pois qualquer falha pode provocar,
além de prejuízos financeiros, desgastes na imagem e reputação da
empresa envolvida. A utilização de componentes na estruturação desses sistemas
promove maior qualidade, confiabilidade e flexibilidade ao produto e
agiliza o processo de desenvolvimento. Entretanto, para que estes
benefícios sejam totalmente observados, é fundamental que os
provedores de componentes projetem-nos com especificações precisas,
completas e consistentes. Uma estratégia para a especificação de componentes tolerantes a falhas é informar a ocorrência de erros através de exceções e realizar a recuperação dos
mesmos por rotinas de tratamento correspondentes. 

Contudo, o uso de notações precisas para representar os componentes tolerantes a falhas contribuem mas não são o suficiente para obtermos sistemas confiáveis. A falta de mecanismos adequados para a integração de componentes pode gerar comportamentos inesperados em sistemas construídos a partir da composição de componentes. Da mesma
forma, a integração dos comportamentos referentes ao tratamento de falhas dos componentes também podem proporcionar comportamentos inesperados se não forem coordenados adequadamente. Este projeto tem como objetivo principal aprofundar os estudos e desenvolver mecanismos para a integração adequada (através de métodos formais) de componentes, tanto para o comportamento normal quanto para o associado ao tratamento de falhas.

CNPq - Edital MCT/CNPq/CT-INFO no 07/2007
 (Proc. 551038/2007-1)

A disseminação de sistemas computacionais em atividades críticas tornou a confiabilidade uma característica indispensável a esses sistemas. Essa confiabilidade é obtida através de técnicas de tolerância a falhas, que aumentam a complexidade do desenvolvimento. Para auxiliar a construção de sistemas tolerantes a falhas, esse projeto de pesquisa propõe um método de desenvolvimento baseado em componentes que guiará tanto as fases de desenvolvimento quanto os testes, paralelizando essas atividades.

Número FAPESP: 04/10663-8

Estudo sobre cooperação entre agentes autônomos híbridos.

Pi-calculus é uma das teorias pioneiras sobre agentes móveis. Além do esforço na construção das teorias, foram desenvolvidas também ferramentas de suporte ao uso das mesmas. Existem atualmente algumas ferramentas para verificação formal de processos concorrentes e agentes móveis, tanto para pi-calculus
quanto para algumas outras teorias. Cada uma dessas ferramentas fornece serviços específicos para os quais elas foram concebidas. Algumas verificam se um dado modelo concorrente preserva algumas propriedades, enquanto outras verificam a equivalência entre modelos distintos. Apesar de todos os esforços, vários desafios ainda persistem na construção de ferramentas: o desenvolvimento de técnicas eficientes para a verificação de agentes móveis,
construir ferramentas de suporte à especificação e verificação que sejam de fácil uso por usuários comuns, diminuição do esforço na construção de ferramentas e desenvolvimento de novas técnicas que abranjam classes de problemas não tratados atualmente.

Considerando a diminuição do esforço de construção de novas ferramentas, um dos objetivos atuais na área de verificação formal é o compartilhamento de
serviços entre ferramentas distintas através da sua integração. Este projeto de pesquisa tem como objetivo a integração das ferramentas de verificação para agentes móveis descritos em pi-calculus. Dessa forma, não há a necessidade de reimplementar todos os serviços requisitados em um único verificador, mas estabelecer comunicação entre verificadores capazes de fornecer os requisitos
desejados.