SHF:Small:Collaborative Research: Compositional Verification of Heterogeneous Software Protocol Stacks

SHF:Small:协作研究：异构软件协议栈的组合验证

• 批准号: 1421678
• 负责人: Zvonimir Rakamaric
• 金额: $ 25.3万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-07-01 至 2017-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1421678&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Compositional

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 errorsthat 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.

开发软件协议堆栈是一项复杂的任务，多年来涉及许多各方和产品。在此过程中必须解决许多问题，并且很难使所有平台和系统的所有可能状态正确所有问题。因此，有许多严重错误的例子最终出现在生产中，因此修复它们的成本很高。软件协议堆栈被广泛用于许多域中，并且可以提高其可靠性的严格方法将产生非常广泛的影响。该项目开发了一种更严格的方法来开发和维护此类复杂的软件协议堆栈。特别是，正式的方法用于通过严格的验证和测试来提早发现错误，并协助分析定位报告的错误。该方法基于目标软件堆栈不同层的自动学习抽象和简洁的协议模型。然后将组成推理应用以有效，精确地查找错误。利用生成的模型来帮助解决错误定位和诊断。通过对Android蓝牙软件堆栈的现实生活案例研究来评估该方法的可用性。