GAMES FOR FORMAL DESIGN AND VERIFICATION OF REACTIVE SYSTEMS

摘要：随着状态空间遍历算法和源代码自动抽象技术的发展，模型检查已成为分析和调试软件系统的关键工具。这个建议围绕着游戏在软件系统建模和分析中的作用展开。在明确区分由不同组件（游戏邦注：例如，系统及其环境）所控制的选择的开放系统中，游戏非常有用。本研究的第一个重点是研究游戏在基于组件的设计和模块验证中的应用。它将探讨如何使用游戏来生成抽象，以捕获满足需求所需的最一般环境假设，并作为界面的动态类型。第二个推力将解决在分析问题的高计算复杂性存在的可扩展性的挑战。符号技术和启发式解决与部分信息博弈将开发使用可满足解算器和包操作二进制决策图。这些技术将实现并应用于网络协议、设备驱动程序和医疗设备等领域的案例研究。

CCR 0306382PI: Rajeev Alur University of PennsylvaniaAbstract:With recent advances in algorithms for state-space traversal and in techniques for automatic abstraction of source code, model checking has emerged as a key tool for analyzing and debugging software systems. This proposal is centered around the role of games in modeling and analysis of software systems. Games are useful in modeling open systems where the distinction among the choices controlled by different components (for instance, the system and its environment) is made explicit. The first thrust of this research will investigate application of games for component-based design and modular verification. It will explore how games can be used to generate abstractions that capture the most general environment assumptions needed to satisfyrequirements, and as dynamic types for interfaces. The second thrust will address the challenge of scalability in presence of high computational complexity of the analysis problems. Symbolic techniques and heuristics for solving games with partial information will be developed using satisfiability solvers and packages for manipulating binary decision diagrams. These techniques will be implemented and and applied to case studies in domains such as network protocols, device drivers, and medical devices.