Bogor: an extensible and highly-modular software model checking framework

Model checking is emerging as a popular technology for reasoning about behavioral 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 costeffective analyses have been achieved by exploiting, for example, naturally occurring abstractions and semantic properties of target 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 checking-based analyses for a variety of software-related models. To explore this hypothesis, we have developed 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 e...

• Type: Conference
• Year: 2003
• Where: SIGSOFT
• Authors: Robby, Matthew B. Dwyer, John Hatcliff
• Keywords: Model Checking Framework, Model Checking Tool, Model Checking-based Analyses, SIGSOFT 2003, Software Engineering