Please use this identifier to cite or link to this item: https://hdl.handle.net/1822/84361

Full metadata record
DC FieldValueLanguage
dc.contributor.advisorCunha, Alcinopor
dc.contributor.advisorSantos, André Filipe Fariapor
dc.contributor.authorRibeiro, Luís Mário Macedopor
dc.date.accessioned2023-05-09T20:51:04Z-
dc.date.available2023-05-09T20:51:04Z-
dc.date.issued2022-12-19-
dc.date.submitted2022-12-
dc.identifier.urihttps://hdl.handle.net/1822/84361-
dc.descriptionDissertação de mestrado integrado em Informatics Engineeringpor
dc.description.abstractIndustrial manufacturing is becoming highly reliant on automation developments, as they bring more efficient and accurate processes, with lower associated costs. Consequently, robots are increasingly being deployed in a wide range of scenarios, especially where safety is demanded. In such cases, it is critical to employ appropriate procedures to verify both the system’s quality and safety. Following the current growth of cyber-physical systems, as well as their usage in various technology domains, the development of software applications is becoming more demanding due to the complexity behind the integration of complementing services, beyond those provided by the operating system. One of the most popular open-source software platforms for building robotic systems is the Robot Operating System (ROS) [53] middleware, where highly configurable robots are usually built by composing third-party modules. Robot Operating System 2 (ROS2) is implemented using the Data Distribution Service (DDS) [49] communication protocol. ROS2 implicitly makes use of the DDS-Security artefacts through the Secure Robot Operating System 2 (SROS2) security toolset. The present study focus on detecting security problems in ROS2 networks, in which it is intended to verify, through formal techniques, security properties. However, security is a very broad subject, so this study focuses on a particular security property to show the viability of the proposed technique, namely Observational Determinism (OD). This dissertation introduces a software tool, named Security Verification in ROS (svROS), that provides multiple functionalities to support this type of security analysis using Alloy [32], a formal specification language and analysis tool.por
dc.description.abstractA crescente implementação de processos automáticos tem motivado a reestruturação nos mais diversos setores industriais, com o objetivo de aumentar a eficiência e precisão dos mesmos, e consequentemente, reduzir os custos associados. Além disso, esta ideia levou à integração da robótica nos mais amplos domínios tecnológicos, especialmente onde a segurança é exigida. Nestes casos, é fundamental adotar técnicas apropriadas de forma a verificar tanto a qualidade do sistema, como a segurança do mesmo. Como resultado do atual crescimento dos sistemas ciber-físicos, nomeadamente sistemas robóticos, bem como a sua utilização em vários domínios tecnológicos, o desenvolvimento de aplicações tem vindo a ficar mais exigente, em particular devido à complexidade da integração dos serviços necessários, tipicamente não fornecidos pelo sistema operativo. Uma das plataformas considerada como standard no que toca ao desenvolvimento de sistemas robóticos é o middleware ROS [53], onde robôs altamente configuráveis são construídos através da composição modular de software externo, oferecendo características como flexibilidade e interoperabilidade aos sistemas integrados. O ROS2 implementa um protocolo de comunicação, de nome DDS [49], que, para além de garantir serviços de comunicação, implementa a especificação DDS-Security, que oferece diferentes métodos de adoção de segurança, através de uma metodologia de plugins. Através do uso desta especificação, juntamente com o uso do toolset SROS2, é possível configurar o ROS2 de forma a proporcionar um ambiente seguro às aplicações integradas. O presente trabalho foca-se no estudo e deteção de problemas de segurança em topologias ROS2, através da verificação formal de propriedades de segurança. No entanto, a segurança é um assunto extenso, pelo que o foco de interesse nesta tese é numa propriedade particular de segurança para mostrar a viabilidade da presente técnica, de nome OD. Esta dissertação introduz a uma ferramenta de verificação de nome svROS, que contempla múltiplas funcionalidades para suportar este tipo de análise usando Alloy [32], uma linguagem de especificação formal e respectiva ferramenta de análise.por
dc.description.sponsorshipThis work is financed by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project LA/P/0063/2020.por
dc.language.isoengpor
dc.relationLA/P/0063/2020por
dc.rightsopenAccesspor
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/por
dc.subjectRoboticspor
dc.subjectROS2por
dc.subjectSROS2por
dc.subjectSecurity propertiespor
dc.subjectObservational determinismpor
dc.subjectSoftware verificationpor
dc.subjectAlloypor
dc.subjectRobóticapor
dc.subjectPropriedades de segurançapor
dc.subjectDeterminismo observacionalpor
dc.subjectVerificação de softwarepor
dc.titleFormalizing ROS2 security configuration with Alloypor
dc.typemasterThesiseng
dc.identifier.tid203261275por
thesis.degree.grantorUniversidade do Minhopor
sdum.degree.grade18 valorespor
sdum.uoeiEscola de Engenhariapor
dc.subject.fosEngenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informáticapor
Appears in Collections:BUM - Dissertações de Mestrado
DI - Dissertações de Mestrado

Files in This Item:
File Description SizeFormat 
Luis Mario Macedo Ribeiro.pdf3,15 MBAdobe PDFView/Open

This item is licensed under a Creative Commons License Creative Commons

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID