Please note: This master’s thesis presentation will take place in DC 3317.
Xiang
Yun
(Fa
Fa)
Ke,
Master’s
candidate
David
R.
Cheriton
School
of
Computer
Science
Supervisor: Professor Jo Atlee
Large software systems are developed by multiple teams of software engineers, each working on different components that are supposed to work together. Each component is responsible for a subset of system functionality and the components communicate with each other to react to information received from hardware sensors and user inputs. It is often infeasible to analyze large software systems because the code base may be too large, the components may be written in different languages or language variants, or the concurrency of components can lead to a state explosion of the system’s analysis space. To mitigate these challenges, we create a software model consisting of facts about the software system and perform analyses on the model.
Analyses performed on these software models are not always sound and complete. One of the reasons is that the order of execution of facts in the model is unknown, leading to many false-positive results that refer to infeasible execution paths. Our work addresses this problem by extending a fact-based software model with control-flow-graph facts and associating existing facts with their corresponding control flow blocks. Then, the analyses are revised to check that results correspond to execution paths (in terms of control-flow-graph facts) before reporting results to the engineers.
This extra execution-path check causes the revised analyses to exhibit significant performance overhead. To reduce the overall execution time of the analyses, we (1) stage analysis queries so that they work on a subset of the facts to generate partial results incrementally and (2) employ an on-the-fly execution path check that eliminates invalid sub-results within the analysis engine.
Our work is evaluated with ten different analyses performed on six software systems that use the ROS framework for cross-component communication. A detailed precision and performance evaluation was performed on Autonomoose and WISE-ADS, two ROS-based autonomous driving systems. In addition, this thesis adapts our approach to non-ROS systems (in which components communicate via function calls instead of passed messages) and we evaluate that work by analyzing a non-ROS software controller. The controller experiment is designed to test the scalability of our work when applied to large real-world applications.