Webinar - InfoBlender
Verification of system-wide safety properties of ROS applications
Resumo:
Os robôs estão atualmente implantados em domínios de segurança crítica, mas as técnicas adequadas para avaliar a segurança funcional de seu software ainda não foram adotadas. Isso é particularmente crítico em ROS, onde robôs altamente configuráveis são construídos através da composição de módulos de terceiros. Para promover a adoção, defendemos o uso de métodos formais leves, técnicas automáticas com entrada mínima do utilizador e feedback intuitivo.
Este artigo propõe uma técnica para verificar automaticamente as propriedades de segurança de todo o sistema de aplicações baseadas em ROS em tempo estático. É baseado na formalização de modelos de arquitetura ROS e comportamento de nó no Electrum, sobre os quais as especificações de todo o sistema são posteriormente verificadas no modelo. Para automatizar a análise, é implementado como um plug-in para HAROS, um framework de avaliação da qualidade de software ROS voltado para a comunidade ROS. A técnica é avaliada num robô real com resultados positivos.
Biografia:
Nuno Macedo é Professor Auxiliar da Faculdade de Engenharia da Universidade do Porto (FEUP) e investigador do HASLab. A sua investigação centra-se no desenvolvimento, ensino e aplicação de técnicas formais para engenharia de software com o objetivo de promover o desenvolvimento de software confiável. O seu principal interesse de investigação reside no design de software confiável, particularmente em abordagens baseadas em métodos formais leves apoiados por verificação e descoberta de modelos. Ele também adaptou essas técnicas para o domínio da robótica, para promover o desenvolvimento de software de robótica seguro.
Notas:
Inscreva-se aqui até o dia 28 de outubro para aceder ao link da sessão de Zoom.
Os slides encontram-se disponíveis aqui.