Bolsa de Iniciação Científica CNPq

As atividades de iniciação científica relacionadas ao projeto consistem em:

• Estudo de técnicas para a detecção e mitigação/resolução de conflitos para Open Radio Access Networks (O-RAN) [2,3]

• Especificação em Maude [1] para a análise da(s) abordagem(ns) propostas.

Dessa forma, pretende-se que o aluno tenha ao final da atividade a compreensão do problema de detecção de conflitos em O-RAN, e possíveis estratégias de mitigação/resolução, e a utilização de ferramenta de especificação de sistemas concorrentes, com geração de artefatos computáveis [1].

Quantidade de Bolsas: 1

Carga Horária: 12 horas (mínimo)

Valor da Bolsa: R$700,00

Interessados entrar em contato por email, enviando o histórico escolar. Será marcada uma data e hora para entrevista.

Data Limite: 8 de abril

Contatos: brunoos@ufg.br ou ventura@ufg.br

Referências  

[1] Peter Csaba Ölveczky. Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude. In Series Undergraduate Topics in Computer Science, Springer 2018.

[2] Cezary Adamczyk, Adrian Kliks. Conflict Mitigation Framework and Conflict Detection in O-RAN Near-RT RIC. IEEE Commun. Mag. 61(12): 199-205 (2023)

[3] Marcin Hoffmann et al.. Open RAN xApps Design and Evaluation: Lessons Learnt and Identified Challenges. IEEE J. Sel. Areas Commun. 42(2): 473-486 (2024)

Título: Aplicações de Formalismos Lógico-Semânticos em Programação Concorrente e Redes Móveis de Próxima Geração.

Resumo: Atualmente, sistemas concorrentes (i.e. sistemas baseados em agentes ou processos que interagem entre si) são ubíquos em diversos domínios e aplicações, cobrindo desde sistemas biológicos até serviços em nuvem e redes móveis. Em geral, sistemas concorrentes apresentam formas complexas de interação, e.g. os encontrados em modelos biológicos, sistemas multimídia interativos, redes sociais e dispositivos de Internet das Coisas (IoT). Os frameworks para especificação/verificação dos sistemas atuais devem ser escaláveis para o tratamento de grandes sistemas e propriedades cada vez mais intrincadas.

Este projeto tem por finalidade a aplicação de Métodos Formais em diferentes aspectos relacionados ao desenvolvimento de sistemas concorrentes. Investigamos dois domínios de aplicação em particular: a programação concorrente e as redes móveis de próxima geração (5G e 6G). Os grandes desafios postos pelos sistemas atuais estão presentes em ambos domínios: sistemas de nuvem, onde alocações (de recursos) podem ser aninhadas; redes móveis de próxima geração, onde slices devem ser criados e gerenciados de forma autônoma; e sistemas de tipos adequados para linguagens que dão suporte à programação concorrente. 

O estabelecimento de fundamentos rigorosos para tais sistemas apresenta um grande desafio à Ciência da Computação. Em particular, dois aspectos devem ser garantidos: representação adequada do sistema investigado (i.e. a evolução do sistema está em correspondência 1-1 com reduções/derivações no modelo); e oferta de ferramentas que permitam o raciocínio para a verificação de propriedades dos sistemas.

De fato, planejamos adotar abordagens complementares para atacar a complexidade inerente destes sistemas: modelos declarativos para concorrência e lógica de reescrita. Além disso, os tipos de sessão serão o fundamento para uma investigação operacional/denotacional em linguagem de programação concorrente.