BOGOR : A Model Checking Framework for Dynamic Software

BOGOR：动态软件的模型检查框架

• 批准号: 0306607
• 负责人: Matthew Dwyer
• 金额: $ 18万
• 依托单位: Kansas State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2003
• 资助国家: 美国
• 起止时间: 2003-06-01 至 2004-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0306607&HistoricalAwards=false
• 关键词: BOGOR; Model; Checking; Framework; Dynamic

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.

CCR-0306607Matthew B. Dwyerkansas State Universitymodel检查已成为一种流行技术，用于推理各种软件文物的行为属性，包括：需求模型，建筑描述，设计，实施，实现和过程模型。 模型检查的复杂性是众所周知的，但通过利用特定软件伪像的语义属性来实现具有成本效益的分析。 调整模型检查工具来利用这种“域知识”通常需要对工具的实现进行深入了解。 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. 我们将使用Bogor来研究模型检查算法的自定义可以提高范围的性能。 具体来说，我们将适应Bogor，以推理基于事件驱动的组件设计模型，并推荐多线程Java程序。 我们将评估可以将域信息纳入框架的易用性以及通过利用该信息来实现的空间/时间改进。