GAMES FOR FORMAL DESIGN AND VERIFICATION OF REACTIVE SYSTEMS

CCR 0306382PI：宾夕法尼亚大学Rajeev Alur摘要：随着状态空间遍历算法和源代码自动抽象技术的最新进展，模型检测已成为分析和调试软件系统的关键工具。该提案围绕游戏在软件系统建模和分析中的作用展开。游戏在对开放系统建模时很有用，在开放系统中，由不同组件(例如，系统及其环境)控制的选择之间的区别是明确的。这项研究的第一个主旨将调查游戏在基于组件的设计和模块化验证中的应用。它将探索如何使用游戏来生成抽象，这些抽象捕捉满足需求所需的最一般的环境假设，并作为接口的动态类型。第二个重点将解决在分析问题的计算复杂性很高的情况下可伸缩性的挑战。将使用可满足性解算器和用于处理二元决策图的包来开发用于解决部分信息博弈的符号技术和启发式方法。这些技术将被实施并应用于网络协议、设备驱动程序和医疗设备等领域的案例研究。

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.