BOGOR : A Model Checking Framework for Dynamic Software

CCR-0306607马修B。DwyerKansas State UniversityModel checking正在成为一种流行的技术，用于推理各种各样的软件工件的行为属性，包括：需求模型，架构描述，设计，实现和过程模型。 模型检测的复杂性是众所周知的，但成本效益的分析已经实现了利用特定的软件工件的语义属性。 调整模型检查工具以利用这种“领域知识”通常需要深入了解工具的实现。 我们相信，有了适当的工具支持，领域专家将能够开发有效的模型检查为基础的分析，为各种各样的软件models.To探索这一假设，我们的项目是开发博戈尔，模型检查框架与可扩展的输入语言定义特定领域的结构和模块化的接口设计，以简化特定领域的状态空间编码，减少和搜索算法的优化。 我们将使用博戈尔来研究模型检查算法的定制可以在多大程度上提高可扩展性。 具体来说，我们将调整博戈尔的原因事件驱动的基于组件的设计模型和原因多线程的Java程序。 我们将评估容易与whichdomain信息可以纳入框架和空间/时间的改进，可以通过利用这些信息。

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.