Lisa and rospy: Static Analysis for Robotics

In this thesis, we will show how a static analysis tool can be used to extract meanings from rospy source code. After a brief introduction about the theories that underlie static analysis we will talk about liSA, a static analysis framework maintained and developed by SSV (Software and System Verification) Research Group - a team of professors and researchers headquartered at Ca' Foscari University of Venice - and more specifically we will learn what a frontend for liSA is, how we can write our own one to analyse a specific program, and how liSA works internally in order to produce meaningful results. Extract meaning from code by scratch is a challenging task: it requires a solid understanding of mathematical and computational theories like abstract interpretation and, of course, a deep knowledge of the language under analysis. The peculiarity of using liSA is that these theories are abstracted away, providing and easy-to-use library. We will show how we can use pyLiSA - a python frontend for liSA - to develop domain-specific analysis in a straightforward way. We will focus specifically on the rospy library, the python client library for ROS (Robot Operating System) ecosystem and we will discover how liSA can be extended to perform static analysis of python code that uses the rospy library.