BOGOR : A Model Checking Framework for Dynamic Software

Ccr-0306607 Matthew B.DwyerKansas State University模型检查正在成为一种流行的技术，用于推理各种软件构件的行为属性，包括：需求模型、体系结构描述、设计、实现和过程模型。模型检测的复杂性是众所周知的，但已经通过利用特定软件构件的语义属性实现了具有成本效益的分析。采用模型检测工具来利用这种“领域知识”通常需要深入了解该工具的实现。我们相信，在适当的工具支持下，领域专家将能够为各种软件模型开发高效的基于模型Hecking的分析。为了探索这一假设，我们的项目正在开发Bogor，一个具有可扩展输入语言的模型检查框架，用于定义特定于领域的构造和模块化接口设计，以简化特定于领域的状态空间编码、约简和搜索算法的优化。我们将使用Bogor来研究模型检测算法的定制可以在多大程度上产生改进的可扩展性。具体地说，我们将采用Mogor来推理基于事件驱动的基于组件的设计模型，并推理多线程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.