Developing a software protocol stack is a complex task with many parties and products involved over multiple years. There are many issues that have to be resolved in the process, and it is incredibly hard to get all of them correct for all platforms and all possible states of a system. Hence, there are numerous examples of serious errors that ended up in production, where the cost of fixing them is high. Software protocol stacks are widely used in many domains, and rigorous methods to improve their reliability would have a very broad impact.
The project develops a more rigorous approach to developing and maintaining such complex software protocol stacks.In particular, formal methods are used to find errors early through rigorous verification and testing, as well as to assist the analysis in locating reported errors. The approach is based on automatically learning abstract and succinct protocol models at different layers of the target software stack. Compositional reasoning is then applied to find errors effectively and precisely. The generated models are leveraged to help with error localization and diagnosis. The usability of the approach is assessed through a real-life case study on the Android Bluetooth software stack.
