|
 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.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
 |
1
|
|
| |
2
|
Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
|
| |
3
|
G. Brat, K. Havelund, S. Park, and W. Visser. Java PathFinder -- a second generation of a Java model-checker. In Proceedings of the Workshop on Advances in Verification, July 2000.
|
| |
4
|
|
| |
5
|
William Chan , Richard J. Anderson , Paul Beame , David Notkin , David H. Jones , William E. Warner, Optimizing Symbolic Model Checking for Statecharts, IEEE Transactions on Software Engineering, v.27 n.2, p.170-190, February 2001
[doi> 10.1109/32.908961]
|
| |
6
|
A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV : a new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2(4):410--425, 2000.
|
| |
7
|
E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Jan. 2000.
|
| |
8
|
James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland
[doi> 10.1145/337180.337234]
|
| |
9
|
J. C. Corbett, M. B. Dwyer, J. Hatcliff, and Robby. Expressing checkable properties of dynamic systems: The Bandera Specification Language. International Journal on Software Tools for Technology Transfer, 2002.
|
| |
10
|
|
| |
11
|
X. Deng, M. B. Dwyer, J. Hatcliff, G. Jung, and Robby. Model-checking middleware-based event-driven real-time embedded software. In Proceedings of the 1st International Symposium on Formal Methods for Components and Objects, Nov. 2002. (to appear).
|
| |
12
|
M. B. Dwyer, J. Hatcliff, V. R. Prasad, and Robby. Exploiting object escape and locking information in partial order reductions for concurrent object-oriented programs. Technical Report SAnToS-TR2003-1, Kansas State University, Mar. 2003. (submitted for publication).
|
| |
13
|
M. B. Dwyer, Robby, X. Deng, and J. Hatcliff. Space reductions for model checking quasi-cyclic systems. In Proceedings of the 3rd International Conference on Embedded Software, Oct. 2003. (to appear).
|
| |
14
|
M. B. Dwyer and V. Wallentine. A framework for parallel adaptive grid simulations. Concurrency : Practice and Experience, 9(11):1293--1310, Nov. 1997.
|
| |
15
|
Eclipse website. http://www.eclipse.org|.
|
| |
16
|
|
| |
17
|
FDR2 website. http://www.fsel.com|.
|
| |
18
|
E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns. Addison-Wesley Pub. Co., Jan. 1995.
|
| |
19
|
D. Garlan, S. Khersonsky, and J. S. Kim. Model checking publish-subscribe systems. In Proceedings of the 10th International SPIN Workshop on Model Checking of Software, May 2003.
|
| |
20
|
|
| |
21
|
|
| |
22
|
John Hatcliff , Xinghua Deng , Matthew B. Dwyer , Georg Jung , Venkatesh Prasad Ranganath, Cadena: an integrated development, analysis, and verification environment for component-based systems, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
|
| |
23
|
Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
|
| |
24
|
|
| |
25
|
|
| |
26
|
|
| |
27
|
Bogor Website. http://bogor.projects.cis.ksu.edu|.
|
| |
28
|
Robby, M. B. Dwyer, J. Hatcliff, and R. Iosif. Space-reduction strategies for model checking dynamic systems. In Proceedings of the 2003 Workshop on Software Model Checking, July 2003. (to appear).
|
CITED BY 46
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Matthew B. Dwyer , John Hatcliff Robby , Matthew Hoosier, Supporting model checking education using BOGOR/Eclipse, Proceedings of the 2004 OOPSLA workshop on eclipse technology eXchange, p.88-92, October 24-24, 2004, Vancouver, British Columbia, Canada
|
|
|
|
|
|
|
|
|
Venkatesh Prasad Ranganath , Adam Childs , Jesse Greenwald , Matthew B. Dwyer , John Hatcliff , Gurdip Singh, Cadena: enabling CCM-based application development in Eclipse, Proceedings of the 2003 OOPSLA workshop on eclipse technology eXchange, p.20-24, October 27-27, 2003, Anaheim, California
|
|
|
Stephen F. Siegel , Anastasia Mironova , George S. Avrunin , Lori A. Clarke, Using model checking with symbolic execution to verify parallel numerical programs, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
|
|
|
John Penix , Willem Visser , Seungjoon Park , Corina Pasareanu , Eric Engstrom , Aaron Larson , Nicholas Weininger, Verifying Time Partitioning in the DEOS Scheduling Kernel, Formal Methods in System Design, v.26 n.2, p.103-135, March 2005
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Paolina Centonze , Gleb Naumovich , Stephen J. Fink , Marco Pistoia, Role-Based access control consistency validation, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Luciano Baresi , Giorgio Gerosa , Carlo Ghezzi , Luca Mottola, Playing with time in publish-subscribe using a domain-specific model checker, Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, p.55-62, September 03-04, 2007, Dubrovnik, Croatia
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Franjo Ivani , Zijiang Yang , Malay K. Ganai , Aarti Gupta , Pranav Ashar,
Efficient SAT-based bounded model checking for software verification, Theoretical Computer Science, v.404 n.3, p.256-274, September, 2008
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.2