This grant is framed in the context of the project SAFER - Safety Verification for Robotic Software - that has the goal of developing a framework for the verification of safety properties of software developed with the Robot Operating System (ROS). More specifically, the grant is framed in the context of Task 3 of this project, whose goal is to develop techniques for the verification of end-to-end properties of ROS systems, and has the following goals: - improve the state of the art in the scientific area of the grant, more specifically in the area of safety property verification for robotic software; - compare and select the model-checkers most suited for the verification of end-to-end properties of ROS systems; - specify and implement a technique to extract models from ROS systems (using the HAROS framework) to support the automatic verification of said properties using the selected model-checkers; - develop research skills through the application of the selected methods; - apply critical thinking in the evaluation of the research methods and results, namely in the evaluation of the effectiveness of the developed technique to detect problems in the software of realistic robotic systems.
Bachelor and master in Computer Engineering or related areas
Minimum profile required
1 peer reviewed international conference or jornal paper.Average BSc and MSc grades of at least 14.
Experience with the Robot Operating System; Experience in the development of model extraction techniques.
Since 12 Aug 2020 to 25 Aug 2020
Cluster / Centre
Computer Science / High-Assurance Software