BOGOR : A Model Checking Framework for Dynamic Software

matthew B. dwyer堪萨斯州立大学模型检查正在作为一种流行的技术出现，用于对各种软件工件的行为属性进行推理，这些工件包括：需求模型、体系结构描述、设计、实现和过程模型。模型检查的复杂性是众所周知的，但是通过利用特定软件工件的语义属性已经实现了经济有效的分析。调整模型检查工具来利用这种“领域知识”通常需要对工具的实现有深入的了解。我们相信，有了适当的工具支持，领域专家将能够为各种软件模型开发有效的基于模型检查的分析。为了探索这一假设，我们的项目正在开发BOGOR，这是一个模型检查框架，具有用于定义特定领域结构的可扩展输入语言和模块化接口设计，以简化特定领域状态空间编码、约简和搜索算法的优化。我们将使用BOGOR来研究定制模型检查算法可以提高可扩展性的程度。具体来说，我们将调整BOGOR来解释事件驱动的基于组件的设计模型和多线程Java程序。我们将评估将领域信息纳入框架的难易程度，以及利用这些信息可以实现的空间/时间改进。

CCR-0306607Matthew B. DwyerKansas State UniversityModel checking is emerging as a popular technology for reasoning about behavior properties of a wide variety of software artifacts including: requirements models, architectural descriptions, designs, implementations, and process models. The complexity of model checking is well-known, yet cost-effective analyses have been achieved by exploiting semantic properties of specific software artifacts. Adapting a model checking tool to exploit this kind of "domain knowledge" often requires in-depth knowledge of the tool's implementation. We believe that with appropriate tool support, domain experts will be able to develop efficient model hecking-based analyses for a variety of software models.To explore this hypothesis, our project is developing BOGOR, a model checking framework with an extensible input language for defining domain-specific constructs and a modular interface design to ease the optimization of domain-specific state-space encodings, reductions and search algorithms. We will use BOGOR to investigate the degree to which customization of model checking algorithms can yield improvedscalability. Specifically, we will adapt BOGOR to reason about event-driven component-based design models and to reason about multi-threaded Java programs. We will evaluate the ease with whichdomain information can be incorporated into the framework and the space/time improvements that can be achieved by exploiting that information.