Category Archives: Destaque

DEI Talks | Formal Verification of Distributed Systems por Julien Brunel e David Chemouil

Posted on

Julien Brunel e David Chemouil são investigadores seniores na ONERA, em Toulouse, especializados em formal specification and verification. Juntamente com Nuno Macedo e Alcino Cunha (INESC TEC) conceberam a 6ª versão (até há pouco tempo designada Electrum) da linguagem e ferramenta Alloy (originalmente proposta pelo MIT). Nos últimos anos, Julien Brunel e David Chemouil têm vindo a estudar também a verificação de algoritmos distribuídos.

Segundo os investigadores “a recent highlight is the first mechanical proof of correctness of the distributed maintenance algorithm of the Chord peer-to-peer protocol, as well as formal techniques for the complete, semi-automatic verification of infinite-state systems, such as distributed algorithms”.

Junte-se a nós no dia 8 de Abril, às 14:30, na sala I-105 da FEUP, para a apresentação deste trabalho

 Abstract:

The verification of distributed systems is challenging because these systems combine a rich structure, a high number of elements and a non-trivial temporal evolution. A trade-off between automation and completeness of the verification has to be made. In particular, one can use theorem provers, which offer complete confidence but tend to require considerable expertise and effort. Another option is to use model checkers, which offer complete automation, but cannot handle complex data structures and configurations.

In this talk, they will present recent work on verification techniques for distributed systems that are automatic and “as complete as possible”, or complete and “as automatic as possible”. They will illustrate their work with the analysis of Chord, a scalable distributed hash table.

INFORMATICS.OnBoard, o programa de *Mentoria Interpares de Engenharia Informática, promoveu no passado dia 2 de abril mais um momento de convívio entre estudantes do 1º ano da L.EIC e seus mentores.

Posted on

O grupo saiu à descoberta do “Pequeno Tibete Português” através do Trilho das Brandas de Sistelo (Caminhada pelo PR14). Neste cenário de verdadeira beleza rural, onde os fabulosos socalcos se destacam na paisagem, estudantes e professores puderem conviver informalmente, em dinâmicas de colaboração que promovem a entreajuda, a integração, a amizade e o bem estar.

Esta foi a segunda atividade da edição de 2021/2022. Todas as outras podem ser vistas em Informatics On Board

*Mentoria Interpares

A Faculdade de Engenharia da Universidade do Porto tem em funcionamento um programa de MENTORIA INTERPARES, destinado aos estudantes que ingressam pela 1ª vez nesta instituição de Ensino Superior (mentorados), tanto nacionais como internacionais, com o objetivo de os apoiar nesta nova fase do seu percurso académico. A dinamização deste programa de integração social e académica é realizada por estudantes (mentores) que já frequentam os diferentes cursos em anos mais avançados, e coordenado por uma equipa de docentes, sendo adaptado a cada curso de acordo com as suas caraterísticas. Este programa é totalmente voluntário tanto para mentores como para mentorados. Esta iniciativa está atualmente integrada no Programa Mentoria U. Porto.

DEI Talks | JUMPING FINITE AUTOMATA por Prof. Alexander Meduna

Posted on

Prof. Alexander Meduna (nascido em 1957 em Olomouc, República Checa) é um cientista informático teórico e especialista em desenho de compiladores, linguagens formais e autómatos. É professor de Informática na Brno University of Technology.

Anteriormente, ensinou informática teórica em várias universidades europeias e americanas, incluindo a Universidade do Missouri, onde passou uma década a ensinar tópicos avançados de teoria da linguagem formal. Escreveu mais de noventa artigos relacionados com teoria da computação.

Junte-se a nós no dia 7 de Abril, às 14:30, na sala I-105 da FEUP, para a apresentação de JUMPING FINITE AUTOMATA

Abstract:

This talk proposes a new investigation area in automata theory — jumping finite automata. These automata work like classical finite automata except that they read input words discontinuously — that is, after reading a symbol, they can jump over some symbols within the words and continue their computation from there. The talk gives several results concerning jumping finite automata in terms of commonly investigated areas of automata theory, such as closure properties. Most importantly, it achieves several results that demonstrate differences between jumping finite automata and classical finite automata. In its conclusion, the talk  formulates several open problems and suggests future investigation areas.

O seu último livro é o Handbook of Mathematical Models for Languages and Computation

Meduna, Alexander; Tomko, Martin, Horacek, Petr (2019)

The Institution of Engineering and Technology, Stevenage, UK, ISBN: 978-1-78561-660-0

https://www.amazon.ae/Handbook-Mathematical-Models-Languages-Computation/dp/1785616595

Alguns dos livros anteriores:

  • Meduna, Alexander (2000). Automata and Languages: Theory and Applications. Springer Science & Business Media. ISBN 9781852330743.
  • Meduna, Alexander (2007). Elements of Compiler Design. CRC Press. ISBN 9781420063233.
  • Meduna, Alexander (2014). Formal Languages and Computation: Models and Their Applications. CRC Press. ISBN 9781466513457.
  • Meduna, Alexander; Švec, Martin (2005). Grammars with Context Conditions and Their Applications. John Wiley & Sons. ISBN 9780471736554.
  • Meduna, Alexander; Techet, Jiří (2010). Scattered Context Grammars and Their Applications. WIT Press. ISBN 9781845644260.
  • Meduna, Alexander; Zemek, Petr (2014). Regulated Grammars and Automata. Springer. ISBN 9781493903696.
  • Meduna, Alexander; Soukup, Ondřej (2017). Modern Language Models and Computation: Theory with Applications. Springer. ISBN 9783319630991.

Provas de Doutoramento em Engenharia Informática: ”Increasing the Dependability of Internet-of-Things Systems in the context of End-User Development Environments”

Posted on

Candidato:
João Pedro Matos Teixeira Dias

Data, Hora e Local
1 de abril, às 09:00, por videoconferência com transmissão em direto em: https://www.youtube.com/channel/UCvsg2ymeaHLRLbsGt67JmKw

Presidente do Júri
Doutor Rui Filipe Lima Maranhão de Abreu, Professor Catedrático da Faculdade de Engenharia da Universidade do Porto

Vogais
Doutor Dariusz Mrozek, Professor Associado do Department of Applied Informatics da Silesian University of Technology, Poland;
Doutor Pedro Nicolau Faria da Fonseca, Professor Auxiliar do Departamento de Eletrónica, Telecomunicações e Informática da Universidade de Aveiro;
Doutor André Monteiro de Oliveira Restivo, Professor Auxiliar do Departamento de Engenharia Informática da Faculdade de Engenharia da Universidade do Porto;
Doutor Hugo José Sereno Lopes Ferreira, Professor Auxiliar do Departamento de Engenharia Informática da Faculdade de Engenharia da Universidade do Porto (Orientador).

Resumo:

A ubiquidade da computação, conhecida como Internet-of-Things (IoT), tem moldado a maneira como as pessoas interagem com o mundo físico. No entanto, a escala, distribuição lógica e geográfica, densidade, heterogeneidade, interdependência, e os requisitos de segurança, fazem com que estes sistemas sejam complexos, criando vários desafios operacionais e de desenvolvimento. Embora exista um consenso alargado de que as práticas de engenharia de software amplamente utilizadas são inadequadas para o desenvolvimento de IoT, estas continuam a ser as soluções mais usadas. Este aspeto tem vindo a comprometer a confiabilidade destes sistemas, centralizando a maior parte da computação em infraestruturas cloud. Adicionalmente, a larga-escala destes sistemas em termos de dispositivos e aplicações supera os recursos técnicos existentes para a sua gestão e operação, sendo crucial torná-los o mais self-managed possível. No entanto, tem de ser dada a capacidade aos operadores do sistema (incluindo utilizadores finais) de configurá-los e entendê-los — principalmente usando soluções que não requerem alto conhecimento técnico, viz. soluções de desenvolvimento de low-code — incluindo a capacidade de configuração de medidas de resiliência em caso de falhas.

O foco principal desta dissertação é investigar como melhorar o status quo da confiabilidade em sistemas IoT. Este é um esforço multifacetado sendo necessário (1) perceber quais são as melhores práticas para desenvolver IoT de forma confiável e qual é sua solidez científica, (2) perceber se as soluções atuais fornecem mecanismos fundamentais que permitem desenhar e construir sistemas confiáveis, e, se não, que contribuições são necessárias para superar as limitações existentes e, por último, (3) dado que esses sistemas são operados por humanos com conhecimento técnico limitado, é necessário que os seus utilizadores sejam capazes de usar e configurar os sistemas sem comprometer o correto funcionamento dos mesmos. Enquanto nos propomos a enfrentar os desafios acima mencionados, afirmamos que:

É possível enriquecer os ambientes de desenvolvimento de IoT focados em utilizadores finais de tal forma que os sistemas resultantes têm um maior grau de confiabilidade, reduzindo o impacto no know-how destes utilizadores.

Para se melhor entender o que (e como) os utilizadores finais desejam automatizar os seus sistemas de IoT foi realizado um estudo para reunir cenários de automação, como pesquisa preliminar. De seguida, uma extensa pesquisa bibliográfica foi realizada de forma a extrair um conjunto de padrões que podem ser usados para melhorar os sistemas IoT do ponto de vista da sua confiabilidade. Estes padrões foram documentados em formconfiabilidadea sucinta, expondo problemas particulares dentro de um contexto específico. As relações de um subconjunto desses padrões foram estudadas, resultando numa linguagem de padrão de self-healing, endereçando as preocupações de confiabilidade em tempo de execução de forma autonómica.

A adoção destes padrões depende de aspetos arquiteturais e funcionais dos sistemas. Um dos aspetos limitadores é que a maioria dos sistemas e soluções atuais não fornece nenhum mecanismo para reajustar o comportamento do sistema durante o tempo de execução. Dado isto, os paradigmas de computação fog e edge foram explorados de forma a aproveitar os recursos computacionais em todas as camadas do sistema, com o objetivo de tornar os sistemas mais confiáveis e mais escaláveis. Com estas contribuições de base, exploramos e afirmamos a viabilidade de usar funções serverless no contexto de IoT, otimizando a escolha de contextos de execução de acordo com preferências, restrições e latências.

Para melhor entender como é que estes paradigmas podem ser potencializados para soluções amplamente utilizadas, selecionamos Node-RED como caso de estudo, dado ser um dos sistemas de desenvolvimento open-source mais utilizados. Este fornece uma interface de programação visual que potencia que utilizadores com diferentes níveis de conhecimento técnico o possam usar. E, tal como outras soluções, o Node-RED não fornece mecanismos para orquestrar tarefas entre dispositivos nem lidar com falhas de partes do sistema dinamicamente, limitando a confiabilidade dos sistemas construídos.

Começamos por avaliar empiricamente, tanto em configurações virtuais como físicas, a viabilidade de usar o Node-RED como um orquestrador, onde as tarefas computacionais são alocadas para os recursos disponíveis e as falhas de dispositivos são mitigadas com re-orquestrações. Também foi desenvolvido um conjunto de extensões para Node-RED que permitem enriquecer os programas existentes (flows) com mecanismos de self-healing — permitindo a deteção de diferentes erros durante o tempo de execução e reajustando o comportamento do sistema para este manter a sua operação dentro de níveis aceitáveis de Qualidade de Serviço.

Dado que os utilizadores de IoT têm diferentes níveis de conhecimento técnico, tentamos melhorar a interação com os ambientes de desenvolvimento destes sistemas para que os utilizadores pudessem melhor entender quais são as automações configuradas (viz. inspeção), como estas se estão a comportar (viz. observabilidade e feedback), e aumentar a sua capacidade de perceber qual foi a possível causa por trás de certos eventos (viz. causalidade). No primeiro estudo, começamos por estender as notações visuais e as funcionalidades do Node-RED para que pudéssemos melhorar o processo de desenvolvimento. De seguida avaliamos empiricamente o desempenho da solução desenvolvida em relação a uma versão do Node-RED sem modificações, observando melhorias estatisticamente significativas na capacidade dos utilizadores de evoluir sistemas de IoT existentes. Por fim, exploramos o uso de assistentes de voz como maneira alternativa de configurar, compreender e interagir com ambientes IoT, focando-nos particularmente na capacidade de um utilizador perceber a causa por trás de alguns eventos.

Verificamos a viabilidade do uso de sistemas de voz como forma alternativa de desenvolvimento de sistemas IoT, cobrindo todas as diferentes possibilidades de automação que o Node-RED suporta, com uma extensão considerável das possibilidades de interação devido ao suporte de diálogos multimensagem. Passamos a validar a viabilidade dos utilizadores usarem o assistente de voz para realizar diferentes tarefas, verificando que todos os utilizadores foram capazes de terminar as tarefas. Enquanto algumas frases válidas foram incorretamente reconhecidas pelo mecanismo de reconhecimento de voz, o que forçou alguns participantes a repetir a sua intenção, os participantes expressaram uma preferência por interfaces de voz preterindo interfaces visuais em termos de perceção subjetiva.

Essas contribuições materializam-se num conjunto básico de blocos de construção que, em conjunto, podem ser usados para melhorar a confiabilidade dos sistemas de IoT, ao mesmo tempo que potencializam a capacidade do utilizador de os configurar, usar e desenvolver sistemas deste tipo. As contrapartes experimentais destas contribuições fornecem evidências empíricas que sustentam a plausibilidade da hipótese.

Palestra | “Análise Musical Interactiva usando a DFT e Distribuições de Classes de Altura a partir de ficheiros MIDI” por Fabian C. Moss

Posted on

Fabien C. Moss é Investigador em Cultural Analytics na Universidade de Amesterdão (UvA). Trabalhando com grandes conjuntos de dados simbólicos de partituras musicais e anotações harmónicas, é  principalmente interessado em Análise Musical Computacional, Teoria Musical, Cognição Musical, e a sua relação mútua. A sua investigação é intrinsecamente interdisciplinar e tem como objetivo fazer a ponte entre as humanidades e as ciências, recorrendo a métodos e conceitos da Musicologia e Teoria Musical, Matemática, Recuperação de Informação Musical, Ciência de Dados e Aprendizagem de Máquinas, Psicologia e Cognição Musical, e Humanidades Digitais.

Junte-se a nós no dia 4 de Abril, às 14:30, na sala B015 da FEUP, para a apresentação de “Análise Musical Interactiva usando a DFT e Distribuições de Classes de Altura a partir de ficheiros MIDI”.

Pelo autor:

“A transformação discreta de Fourier (DFT) é um processo fundamental do processamento de sinais digitais e comummente utilizada para extrair periodicidades de sinais.

No entanto, nos últimos anos, os teóricos da música matemática começaram a explorar o potencial da DFT quando aplicada não ao tempo mas ao domínio das classes de altura, onde as periodicidades são dadas por divisões iguais da oitava [1-3]. No início deste ano, introduzimos as wavescapes [4], um método de visualização das relações hierárquicas de classe pitch em peças de música.

Com base neste trabalho, estamos atualmente a desenvolver midiVERTO [5], uma aplicação web interativa para analisar ficheiros MIDI utilizando o DFT, que permite aos utilizadores criar wavescapes e inspecionar a dinâmica das distribuições de classe pitch a vários níveis hierárquicos. Na minha apresentação, vou apresentar brevemente o trabalho teórico subjacente seguido de um tutorial sobre como utilizar a aplicação para análise musical.

[1] Amiot (2016). Music Through Fourier Space: Discrete Fourier Transform in Music Theory. Springer.

[2] Noll (2019). Insiders’ Choice: Studying Pitch Class Sets Through Their Discrete Fourier Transformations. InMathematics and Computation in Music (pp. 371–378). Springer. https://doi.org/10.1007/978-3-030-21392-3_32

[3] Tymoczko & Yust (2019). Fourier Phase and Pitch-Class Sum. In Mathematics and Computation in Music (pp. 46–58). Springer. https://doi.org/10.1007/978-3-030-21392-3_4

[4] Viaccoz, C., Harasim, D., Moss, F. C., & Rohrmeier, M. (2022). Wavescapes: A visual hierarchical analysis of tonality using the discrete Fourier transform. Musicae Scientiae. https://doi.org/10.1177/10298649211034906

[5] Harasim, D., Affatato, G., & Moss, F. C. (2022). midiVERTO: A Web Application to Visualize Tonality in Real Time. arXiv:2203.13158 [cs]. http://arxiv.org/abs/2203.13158”

Concursos documentais para recrutamento de 2 Professores Auxiliares para a área disciplinar de Engenharia Informática

Posted on

Candidaturas até ao dia 28 de abril de 2022

 Edital 279/2022

Professor Doutor José Manuel Pereira Dias de Castro Lopes, Professor Catedrático da Faculdade de Medicina da Universidade do Porto, Vice-Reitor da mesma Universidade:
Faço saber que, por meu despacho de 25 de fevereiro de 2022, no uso de competência delegada por Despacho n.º 8378/2021, publicado no Diário da República, 2.ª série, n.º 164 de 24 de agosto, pelo prazo de 30 (trinta) dias úteis a contar do dia imediato ao da publicação do presente edital no Diário da República, se abre concurso documental para recrutamento de um Professor Auxiliar para a área disciplinar de Engenharia Informática, do Departamento de Engenharia Informática (DEI), da Faculdade de Engenharia desta Universidade. Edital PT

Edital 280/2022

Professor Doutor José Manuel Pereira Dias de Castro Lopes, Professor Catedrático da Faculdade de Medicina da Universidade do Porto, Vice-Reitor da mesma Universidade:
Faço saber que, por meu despacho de 25 de fevereiro de 2022, no uso de competência delegada por Despacho n.º 8378/2021, publicado no Diário da República, 2.ª série, n.º 164 de 24 de agosto, pelo prazo de 30 (trinta) dias úteis a contar do dia imediato ao da publicação do presente edital no Diário da República, se abre concurso documental para recrutamento de um Professor Auxiliar para a área disciplinar de Engenharia Informática, do Departamento de Engenharia Informática (DEI), da Faculdade de Engenharia desta Universidade. Edital PT

Provas de Doutoramento em Media Digitais: ”Instagram Photography: Toward the profiling of photography sharing modes of practice”

Posted on

Candidato:
Cláudio António Moreira Alves do Carmo Reis

Data, Hora e Local
29 de março, às 10h00, na Sala de Atos da Faculdade de Engenharia e por videoconferência.

Streaming: https://www.youtube.com/channel/UCvsg2ymeaHLRLbsGt67JmKw

Presidente do Júri
Doutor António Fernando Vasconcelos Cunha Castro Coelho, Professor Associado c/ Agregação da FEUP

Vogais
Doutora Luísa Maria Lopes Ribas, Professora Auxiliar da Faculdade de Belas Artes da Universidade de Lisboa;
Doutora Sandra Vieira Jürgens, Professora Auxiliar Convidada do Departamento de História da arte da Faculdade de Ciências Sociais e Humanas da Universidade Nova de Lisboa;
Doutor João Pedro Ferreira Dias Leal, Professor Adjunto da Escola Superior de Media Artes e Design do Instituto Politécnico do Porto;
Doutor Pedro Leão Ramos Ferreira Neto, Professor Auxiliar da Faculdade de Arquitetura da Universidade do Porto;
Doutor Gilberto Bernardes de Almeida, Professor Auxiliar do Departamento de Engenharia Informática da Faculdade de Engenharia da Universidade do Porto;
Doutor José Manuel da Silva Fernandes de Carvalho Carneiro, Professor Auxiliar do Departamento de Design da Faculdade de Belas Artes da Universidade do Porto (Orientador).

‹Programming› 2022, Porto + Online

Posted on

A Conferência Internacional sobre Arte, Ciência e Engenharia da Programação é uma nova conferência centrada em temas de programação, incluindo a experiência de programar. Para abreviar foi intitulada ‘Programming’, apenas. A ‘Programming’ procura artigos que promovam o conhecimento da programação sobre qualquer tópico relevante, incluindo a prática e experiência da programação.
Depois de Bruxelas, Nice, Génova, Porto, Cambridge, esta sexta edição seguirá um formato dual, tendo lugar em dois momentos, dois locais, para oferecer dois tipos diferentes de experiência:

Primeiro no Porto, Seg 21 – Sex 25 de Março, 2022, uma cidade encantadora que ficará feliz por poder abraçar os participantes, assim que estes chegarem;
Mais tarde, num local online, Seg 11 – Qui 14 de Abril, 2022, 4 dias, 2,5 horas/dia, em diferentes fusos horários, para acolher em todo o mundo.

Ademar Aguiar, Professor Associado do DEI/FEUP, General Chair desta edição, conta-nos que a próxima semana será repleta de sessões interessantes, com 2 keynotes, 15 palestras, 6 demos, 3 workshops, 1 tutorial.
Em adição haverá também um Open Space que acolherá ideias e interesses de última hora proporcionando um fórum emergente não estruturado desenvolvido pelos participantes para os participantes.

O Programa Social inclui vários eventos sociais, proporcionando uma combinação das atrações do Porto, desde históricas a culturais, gastronómicas e sociais, incluindo a academia e indústria locais. Tudo isto para promover conversas informais e lúdicas, para garantir que a experiência será única e memorável.

De volta ao futuro é o lema para 2022!

Para + informações e inscrições: https://2022.programming-conference.org/

CreativityTalks | Prof. António Sampaio da Nóvoa será o próximo convidado

Posted on

Há muitos “futurismos” que sugerem uma educação sem escolas, baseada nas imensas possibilidades das tecnologias e da inteligência artificial. Estes “futurismos” ganharam força com a pandemia e as diferentes formas de isolamento a que temos estado sujeitos. Mas a educação não se faz em “confinamento”, exige sempre uma relação, um encontro, um trabalho conjunto. Não é o momento de anunciar a “morte da escola”, mas antes a inventar de novo.

“Inventar de novo a Escola” será  o tema da 6ª Creativity Talk, apresentado pelo Professor *António Sampaio da Nóvoa, no dia 17 de março, às 18:00, no Anfiteatro Nobre da FEUP (B032).

A sessão será moderada por Amélia Lopes, Professora Catedrática e Presidente do Conselho Cientifico da Faculdade de Psicologia e de Ciências da Educação da Universidade do Porto.

A participação presencial na palestra requer uma inscrição (gratuita) no Eventbrite (lugares disponíveis à lotação da sala pela ordem de registo).

Se não conseguir comparecer presencialmente na sessão, poderá assistir através do seguinte endereço: https://youtu.be/V2I0h0EQBO0

*Bio

António Sampaio da Nóvoa é Professor Catedrático da Universidade de Lisboa. É Doutor em História pela Universidade de Paris IV-Sorbonne e Doutor em Ciências da Educação pela Universidade de Genebra. Foi Reitor da Universidade de Lisboa entre 2006 e 2013. Foi Embaixador de Portugal junto da UNESCO entre 2018 e 2021.

DEI Talks | The Digital Score – “What’s really going on {in} here?” por Prof. Craig Vear

Posted on

Craig Vear é Professor e Investigador na Universidade de Montfort onde é também Diretor do Laboratório de IA e Robótica Criativa no Instituto de Tecnologias Criativas. A sua investigação é naturalmente híbrida, pois reúne os campos da música, desempenho digital, tecnologias criativas, inteligência artificial, criatividade, jogos, realidade mista e robótica. Tem estado envolvido em investigação baseada na prática com tecnologias emergentes há quase três décadas, e foi editor do The Routledge International Handbook of Practice-Based Research, publicado em 2022. A sua recente monografia The Digital Score: creativity, musicianship and innovation, foi publicada pela Routledge em 2019, sendo também editor da série The Springer’s Cultural Computing Series. Em 2021 recebeu uma bolsa de 2 milhões de euros da ERC Consolidator Grant para continuar a desenvolver a sua pesquisa Digital Score – digiscore.dmu.ac.uk

Junte-se a nós no dia 24 de fevereiro, às 14:30, na sala B024 da FEUP, e assista à apresentação e discussão deste projeto –  Investigating Technological Transformation of the Music Score (DigiScore).

A secção de abertura posicionará a partitura digital entre uma compreensão mais ampla da função e do objetivo de todas as partituras: a de uma interface de comunicação entre músicos. Depois de definir aquilo que assinala uma partitura digital como uma proposta diferente, resumirá as finalidades e objetivos da investigação do projeto DigiScore. Irá posicionar esta investigação entre os princípios centrais do fluxo, da fenomenologia, da incorporação e do efeito dos meios de comunicação, e delinear o foco da investigação como procura de sentido a partir do interior dos atos criativos da partitura digital musicking (Small 1989). A secção final delineará alguns dos novos conhecimentos atuais, e apresentará questões-chave que discutirá com os presentes na sala como forma de permitir a sua voz no desenvolvimento destes investigadores e na expansão da comunidade de investigação nesta área.