Abstract
We report on the design, implementation, and use of C Wolf, a toolset which extracts finite labeled transition systems from C programs. The extraction process is guided by user input on how a program should be abstracted, and what events should be made observable to the user. The output is an abstracted model suitable for input to the Concurrency Workbench. Additionally, facilities are provided to carry out simple observational equivalence-preserving transformations which reduce the size of the generated model. Finally, we report our experiences in using the toolset to analyze the GNU i-protocol(V ersion 1.04) and the BSD ftp daemon (Version 0.3.3).
Supported in part by ARO under grants DAAG55-98-1-03093 and DAAD-19-01-1- 0683, and by NSF under 0098037
Chapter PDF
Similar content being viewed by others
Keywords
References
Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram Rajamani. Automatic predicate abstraction of c programs. In Proceedings of the ACM SIGPLAN 2001 Conference of Programming Language Design and Implementation (PLDI 2001). ACM Press, June 2001.
Thomas Ball and Sriram K. Rajamani. Automatically validating temporal safety properties of interfaces. In The 8th International SPIN Workshop on Model Checking of Software (SPIN 2001), volume 2057 of LNCS, pages 103–122, New York-Berlin-Heidelberg, May 2001. Springer-Verlag.
Thomas Ball and Sriram K. Rajamani. The slam toolkit. In 13th Conference on Computer Aided Verification (CAV’ 01), volume 2102 of LNCS, New York-Berlin-Heidelberg, July 2001. Springer-Verlag.
Ahmed Bouajjani, Rachid Echahed, and Peter Habermehl. Verifying in.nite state processes with sequential and parallel composition. In Conference Record of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’95), pages 95–106, San Francisco, California, January 22–25, 1995. ACM Press.
Guillaume Brat, Klaus Havelund, SeungJoon Park, and William Visser. Java pathfinder: Second generation of a java modelc hecker, July 2000.
O. Burkart and B. Steffen. Model-checking the full-modal mu-calculus for infinite sequentialpro cesses. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Automata, Languages and Programming (ICALP’ 97), volume 1256 of Lecture Notes in Computer Science, pages 419–429, Bologna, Italy, July 1997. Springer-Verlag. Full version to appear in Theoretical Computer science.
Andy Chou, Benjamin Chelf, Dawson Engler, and Mark Heinrich. Using meta-level compilation to check FLASH protocol code. ACM SIGPLAN Notices, 35(11):59–70, November 2000.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporall ogic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April1986.
E. M. Clarke and J. M. Wing. Formal methods: state of the art and future directio ns. ACM Computing Surveys, 28(4):626–643, December 1996.
James Corbett, Matthew Dwyer, John Hatcli., Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: extracting.nite-state models from Java source code. In 22nd International Conference on Software Engineering, pages 439–448, Limerick, Ireland, June 2000. IEEE Computer Society.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, January 1977.
C.R. Ramakrishnan, I.V. Ramakrishnan, S. A. Smolka, Y. Dong, X. Du, A. Roychoudhury, and V.N. Venkatakrishnan. XMC: A logic-programming-based verification toolset. In Computer Aided Verification (CAV 2000), Chicago, Illinois, June 2000.
Claudio Demartini, Radu Iosif, and Riccardo Sisto. A deadlock detection tool for concurrent java programs. Software: Practice and Experience, 29(7):577–603, June 1999.
Yifei Dong, Xiaoqun Du, Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka, Oleg Sokolsky, Eugene W. Stark, and David Scott Warren. Fighting livelock in the i-protocol: A comparative study of verification tools. In Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’ 99), volume 1579 of Lecture Notes in Computer science, pages 74–88. Springer-Verlag, 1999.
Daniel C. Du Varney. Abstraction-Based Generation of Finite State Models from C Programs. PhD thesis, North Carolina State University, 2002.
M. B. Dwyer, J. Hatcli., R. Joehanes, S. Laubach, Robby, C. S. Pasareanu, W. Visser, and H. Zheng. Tool-supported program abstraction for finite-state verification. In Proceedings of the 23rd International Conference on Software Engineering (ICSE-01), pages 177–187, Los Alamitos, California, May 12–19 2001. IEEE Computer Society.
E. M. Clarke, K. L. McMillan, S. Campos, and V. Hartonas-Garmhausen. Symbolic modelc hecking. In Proceedings of the Eighth International Conference on Computer Aided Veri.cation CAV, volume 1102 of Lecture Notes in Computer Science, pages 419–422. Springer Verlag, July/August 1996.
Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In 4th Symposium on Operating System Design and Implementation, Berkeley, CA, October 2000. USENIX Association.
M. Fröhlich and M. Werner. Demonstration of the interactive graph-visualization system davinci. In R. Tamassia and I. G. Tollis, editors, Graph Drawing, volume 894 of Lecture Notes in Computer Science, pages 266–269. DIMACS, Springer-Verlag, October 1994. ISBN 3-540-58950-3.
Patrice Godefroid. Modelc hecking for programming languages using VeriSoft. In The 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997), pages 174–186, Paris, France, 1997. ACM SIGACT and SIGPLAN, ACM Press.
Patrice Godefroid, Bob Hanmer, and Lalita Jagadeesan. Model checking without a model: An analysis of the heart-beat monitor of a telephone switch using verisoft. In Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA’ 98), pages 124–133, Clearwater Beach, FL, March 1998. ACM Press.
Patrice Godefroid, Bob Hanmer, and Lalita Jagadeesan. Systematic software testing using verisoft: An analysis of the 4ess heart-beat monitor. Bell Labs Technical Journal, 3(2), April-June 1998.
K. Havelund and T. Pressburger. Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer, 2(4), april1998.
G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, Englewood Cli.s, New Jersey, 1991.
Gerard J. Holzmann. The engineering of a modelc hecker: the gnu i-protocolcase study revisited. In Proceedings of the 6th Spin Workshop, volume 1680 of LNCS, Toulouse, France, Sept. 1999. Springer Verlag.
Gerard J. Holzmann. Logic verification of ANSI-C code with SPIN. In Proceedings of the 7th International SPIN Workshop, volume 1885 of LNCS. Springer-Verlag, September 2000.
G.J. Holzmann and Margaret H. Smith. Software model checking-extracting verification models from source code. In Formal Methods for Protocol Engineering and Distributed Systems, pages 481–497, Kluwer Academic Publ., Oct. 1999. also in: Software Testing, Veri.cation and Reliability, Vol. 11, No. 2, June 2001, pp. 65–79.
Radu Iosif. Formalv erification applied to java concurrent software. In Proceedings of the 22nd International Conference on Software Engineering, pages 707–709, June 2000.
Eleftherios Koutsofios. Drawing graphs with dot. Technicalrep ort, AT&T Bell Laboratories, Murray Hill, NJ, USA, November 1996. This report, and the program, is included in the graphviz package, available for non-commercial use at URL http://www.research.att.com/sw/tools/graphviz/.
David Ladd, Satish Chandra, Michael Siff, Nevin Heintze, Dino Oliva, and Dave MacQueen. Ckit: A front end for c in sml, March 2000. Available from URLhttp://cm.bell-labs.com/cm/cs/what/smlnj/doc/ckit/index.html.
David Lie, Andy Chou, Dawson Engler, and David L. Dill. A simple method for extracting models from protocol code. In Proceedings of the 28th Annual International Symposium on Computer Architecture, pages 192–203, Göteborg, Sweden, June 30-July 4, 2001. IEEE Computer Society and ACM SIGARCH.
McMillan, K. L. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.
R. Milner. Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, 1989.
R. Cleaveland and S. Sims. The NCSU concurrency workbench. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the Eighth International Conference on Computer Aided Veri.cation CAV, volume 1102 of Lecture Notes in Computer Science, pages 394–397, New Brunswick, NJ, USA, July/August 1996. Springer Verlag.
G. Sander. Vcg-visualization of compiler graphs. Technical Report A01-95, Universität des Saarlande, FB 14 Informatik, 1995.
Scott Stoller. Model checking multi-threaded distributed java programs. In Proceedings of the 7th International SPIN Workshop, volume 1885 of LNCS, pages 224–244. Springer-Verlag, 2000.
William Visser, Kluas Havelund, Guillaume Brat, and SeungJoon Park. Model checking programs. In P Alexander and Pierre Flener, editors, Proceedings of ASE-2000: The 15th IEEE Conference on Automated Software Engineering, Grenoble, France, September 2000. IEEE Computer Society Press.
David Wagner and Drew Dean. Intrusion detection via static analysis. In Francis M. Titsworth, editor, Proceedings of the 2001 IEEE Symposium on Security and Privacy (S&P-01), pages 156–169, Los Alamitos, CA, May 14–16 2001. IEEE Computer Society.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Du Varney, D.C., Purushothaman Iyer, S. (2002). C Wolf - A Toolset for Extracting Models from C Programs. In: Peled, D.A., Vardi, M.Y. (eds) Formal Techniques for Networked and Distributed Sytems — FORTE 2002. FORTE 2002. Lecture Notes in Computer Science, vol 2529. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36135-9_17
Download citation
DOI: https://doi.org/10.1007/3-540-36135-9_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00141-6
Online ISBN: 978-3-540-36135-0
eBook Packages: Springer Book Archive