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

@article{citeulike:4012721, abstract = {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 cost-effective analyses have been achieved by exploiting, for example, naturally occurring abstractions and semantic properties of a target software artifact. 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 encodings, reductions and search algorithms. We present the pattern-oriented design of Bogor and discuss our experiences adapting it to efficiently model check Java programs and event-driven component-based designs.}, author = {Robby and Dwyer, Matthew B. and Hatcliff, John}, citeulike-article-id = {4012721}, journal = {ACM SIGSOFT Software Engineering Notes}, keywords = {2003, bandera, modelchecking}, month = {September}, number = {5}, pages = {267--276}, posted-at = {2009-02-05 15:12:29}, priority = {2}, publisher = {ACM}, title = {Bogor: an extensible and highly-modular software model checking framework}, volume = {28}, year = {2003} }

TY - JOUR ID - citeulike:4012721 L3 - citeulike-article-id:4012721 N2 - 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 cost-effective analyses have been achieved by exploiting, for example, naturally occurring abstractions and semantic properties of a target software artifact. 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 encodings, reductions and search algorithms. We present the pattern-oriented design of Bogor and discuss our experiences adapting it to efficiently model check Java programs and event-driven component-based designs. IS - 5 JF - ACM SIGSOFT Software Engineering Notes EP - 276 TI - Bogor: an extensible and highly-modular software model checking framework PB - ACM VL - 28 SP - 267 KW - 2003 KW - bandera KW - modelchecking AU - Robby AU - Dwyer, Matthew AU - Hatcliff, John PY - 2003/09// ER -