This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Interface Grammars for Modular Software Model Checking
Sept.-Oct. 2008 (vol. 34 no. 5)
pp. 614-632
ASCII Text
x 
 
Graham Hughes, Tevfik Bultan, "Interface Grammars for Modular Software Model Checking," IEEE Transactions on Software Engineering, vol. 34, no. 5, pp. 614-632, Sept.-Oct., 2008.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2008.72,
author = {Graham Hughes and Tevfik Bultan},
title = {Interface Grammars for Modular Software Model Checking},
journal ={IEEE Transactions on Software Engineering},
volume = {34},
number = {5},
issn = {0098-5589},
year = {2008},
pages = {614-632},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2008.72},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Interface Grammars for Modular Software Model Checking
IS - 5
SN - 0098-5589
SP614
EP632
EPD - 614-632
A1 - Graham Hughes,
A1 - Tevfik Bultan,
PY - 2008
KW - Model checking
KW - Languages
KW - interface grammars
KW - modular verification
VL - 34
JA - IEEE Transactions on Software Engineering
ER -
 
Graham Hughes, University of California, Santa Barbara, Santa Barbara
Tevfik Bultan, University of California, Santa Barbara, Santa Barbara
Verification techniques relying on state enumeration (e.g., model checking) face two important challenges: the state-space explosion, an exponential increase in the state space as the number of components increases; and environment generation, modeling components that are either not available for analysis, or that cannot be handled by the verification tool in use. We propose a semi-automated approach for attacking these problems. In our approach, interfaces for the components not under analysis are specified using a specification language based on grammars. Specifically, an interface grammar for a component specifies the sequences of method invocations that are allowed by that component. We have built an compiler that takes the interface grammar for a component as input and generates a stub for that component. The stub thus generated can be used to replace that component during state space exploration, either to moderate state space explosion, or to provide an executable environment for the component under verification. We conducted a case study by writing an interface grammar for the Enterprise JavaBeans (EJB) persistence interface, and using the resulting stub to check EJB clients using the JPF model checker. Our results show that EJB clients can be verified efficiently with JPF using our approach.

[1] E. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 1999.
[2] G.J. Holzmann, Design and Validation of Computer Protocols. Prentice Hall, 1991.
[3] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[4] P. Godefroid, “Model Checking for Programming Languages Using VeriSoft,” Proc. 24th ACM Symp. Principles of Programming Languages, pp. 174-186, Jan. 1997.
[5] W. Visser, K. Havelund, G. Brat, and S. Park, “Model Checking Programs,” Automated Software Eng. J., vol. 10, no. 2, pp. 203-232, 2003.
[6] T. Ball and S.K. Rajamani, “Automatically Validating Temporal Safety Properties of Interfaces,” Proc. SPIN Workshop, pp. 103-122, 2001.
[7] H. Chen, D. Dean, and D. Wagner, “Model Checking One Million Lines of C Code,” Proc. Network and Distributed System Security Symp., 2004.
[8] K. Havelund, M. Lowry, S. Park, C. Pecheur, J. Penix, W. Visser, and J. White, “Formal Analysis of the Remote Agent before and after Flight,” Proc. Fifth NASA Langley Formal Methods Workshop, June 2000.
[9] M. Musuvathi, D. Park, A. Chou, D.R. Engler, and D.L. Dill, “CMC: A Pragmatic Approach to Model Checking Real Code,” Proc. Fifth Symp. Operating Systems Design and Implementation, citeseer.ist.psu.edumusuvathi02cmc.html, Dec. 2002.
[10] W. Visser, K. Havelund, G. Brat, and S. Park, “Model Checking Programs,” Proc. 15th IEEE Int'l Conf. Automated Software Eng., p. 3, 2000.
[11] J. Yang, P. Twohey, D. Engler, and M. Musuvathi, “Using Model Checking to Find Serious File System Errors,” Proc. Sixth Symp. Operating Systems Design and Implementation), 2004.
[12] J.R. Levine, T. Mason, and D. Brown, Lex and Yacc. O'Reilly and Assoc., 1992.
[13] P. Godefroid, C. Colby, and L. Jagadeesan, “Automatically Closing Open Reactive Programs,” Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation, pp. 345-357, 1998.
[14] A.V. Aho, R. Sethi, and J.D. Ullman, Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1988.
[15] F. Nielson, H.R. Nielson, and C. Hankin, Principles of Program Analysis. Springer, 1999.
[16] ANother Tool for Language Recognition (ANTLR), http:/www.antlr.org/, 2008.
[17] G. Hughes and T. Bultan, “Interface Grammars for Modular Software Model Checking,” Proc. Int'l Symp. Software Testing and Analysis, pp. 39-49, x-yojimbo-item:/CC3D1214-37E5-4BFA-9D7F-D22F43161CEC , 2007.
[18] G. Hughes and T. Bultan, “Extended Interface Grammars for Automated Stub Generation,” Proc. Automated Formal Methods Workshop, 2007.
[19] P. Purdom, “A Sentence Generator for Testing Parsers,” BIT, vol. 12, no. 3, pp. 366-375, 1972.
[20] R. Lämmel and W. Schulte, “Controllable Combinatorial Coverage in Grammar-Based Testing,” Proc. 18th IFIP Int'l Conf. Testing Communicating Systems, U. Uyar, M. Fecko, and A. Duale, eds., May 2006.
[21] P.M. Maurer, “Generating Test Data with Enhanced Context-Free Grammars,” IEEE Software, vol. 7, no. 4, pp. 50-55, 1990.
[22] P.M. Maurer, “The Design and Implementation of a Grammar-Based Data Generator,” Software Practice and Experience, vol. 22, no. 3, pp. 223-244, Mar. 1992.
[23] J. Offutt, P.E. Ammann, and L.L. Liu, “Mutation Testing Implements Grammar-Based Testing,” Proc. Second Workshop Mutation Analysis, Nov. 2006.
[24] J.A. Bauer and A.B. Finger, “Test Plan Generation Using Formal Grammars,” Proc. Fourth Int'l Conf. Software Eng., pp. 425-432, Sept. 1979.
[25] A.G. Duncan and J.S. Hutchison, “Using Attributed Grammars to Test Designs and Implementations,” Proc. Fifth Int'l Conf. Software Eng., pp. 170-178, Mar. 1981.
[26] E. Sirer and B.N. Bershad, “Using Production Grammars in Software Testing,” Proc. Second Conf. Domain-Specific Languages, pp. 1-13, 1999.
[27] L. de Alfaro and T.A. Henzinger, “Interface Automata,” Proc. Ninth Ann. Symp. Foundations of Software Eng., pp. 109-120, 2001.
[28] A. Chakrabarti, L. de Alfaro, T. Henzinger, M. Jurdziński, and F. Mang, “Interface Compatibility Checking for Software Modules,” Proc. 14th Int'l Conf. Computer Aided Verification, pp. 428-441, 2002.
[29] J. Whaley, M. Martin, and M. Lam, “Automatic Extraction of Object-Oriented Component Interfaces,” Proc. ACM/SIGSOFT Int'l Symp. Software Testing and Analysis, 2002.
[30] R. Alur, P. Cerny, P. Madhusudan, and W. Nam, “Synthesis of Interface Specifications for Java Classes,” Proc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, 2005.
[31] A. Betin-Can and T. Bultan, “Verifiable Concurrent Programming Using Concurrency Controllers,” Proc. 19th IEEE Int'l Conf. Automated Software Eng., pp. 248-257, 2004.
[32] A. Betin-Can, T. Bultan, and X. Fu, “Design for Verification for Asynchronously Communicating Web Services,” Proc. 14th Int'l World Wide Web Conf., pp. 750-759, 2005.
[33] T. Ball and S.K. Rajamani, “SLIC: A Specification Language for Interface Checking,” Technical Report MSR-TR-2001-21, Microsoft Research, Jan. 2002.
[34] A. Betin-Can, T. Bultan, M. Lindvall, S. Topp, and B. Lux, “Application of Design for Verification with Concurrency Controllers to Air Traffic Control Software,” Proc. 20th IEEE Int'l Conf. Automated Software Eng., 2005.
[35] O. Tkachuk and M.B. Dwyer, “Adapting Side-Effects Analysis for Modular Program Model Checking,” Proc. 18th IEEE Int'l Conf. Automated Software Eng., pp. 188-197, 2003.
[36] O. Tkachuk, M.B. Dwyer, and C. Pasareanu, “Automated Environment Generation for Software Model Checking,” Proc. Fourth Joint Meeting of the European Software Eng. Conf. and ACM SIGSOFT Symp. Foundations of Software Eng., pp. 116-129, 2003.
[37] R. Alur and P. Madhusudan, “Visibly Pushdown Languages,” Proc. ACM Symp. Theory of Computing, 2004.
[38] A. Bouajjani, J. Esparza, and O. Maler, “Reachability Analysis of Pushdown Automata: Application to Model-Checking,” Proc. Eighth Int'l Conf. Concurrency Theory, pp. 135-150, 1997.
[39] R. Alur, K. Etessami, and P. Madhusudan, “A Temporal Logic of Nested Calls and Returns,” Proc. 10th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems K. Jensen and A. Podelski, eds., pp. 467-481, http://springerlink.meta press.comopenurl.asp?genre=article&issn=0302-9 743&volume= 2988&spage=467 , 2004.

Index Terms:
Model checking, Languages, interface grammars, modular verification
Citation:
Graham Hughes, Tevfik Bultan, "Interface Grammars for Modular Software Model Checking," IEEE Transactions on Software Engineering, vol. 34, no. 5, pp. 614-632, Sept.-Oct. 2008, doi:10.1109/TSE.2008.72
Usage of this product signifies your acceptance of the Terms of Use.