skip to main content
10.1145/1085130.1085133acmconferencesArticle/Chapter ViewAbstractPublication PagesaadebugConference Proceedingsconference-collections
Article

Specifying and checking component usage

Published: 19 September 2005 Publication History

Abstract

One of today's challenges is producing reliable software in the face of an increasing number of interacting components. Our system CHET lets developers define specifications describing how a component should be used and checks these specifications in real Java systems. Unlike previous systems, CHET is able to check a wide range of complex conditions in large software systems without programmer intervention. This paper explores the specification techniques that are used in CHET and how they are able handle the types of specifications needed to accurately model and automatically identify component checks.

References

[1]
Thomas Ball and Sriram K. Rajamani, "SLIC: a specification language for interface checking," Microsoft Research Technical Report MSR-TR-2001-21, (2001).]]
[2]
Thomas Ball, Todd Millstein, Rupak Majumdar, and Sriram K. Rajamani, "Automatic predicate abstraction of C programs," Proc. SIGPLAN 01, pp. 203--213 (June 2001).]]
[3]
Thomas Ball and Sriram K. Rajamani, "The SLAM project: debugging system software via static analysis," Proc. POPL 2002, (2002).]]
[4]
Guillaume Brat, Klaus Havelund, Seung Joon Park, and Willem Visser, "Java PathFinder: Second generation of a Java model checker," Proc. Post-CAV Workshop on Advances in Verification, (July 2000).]]
[5]
Guillaume Brat and WIllem Visser, "Combining static analysis and model checking for software analysis," Proc. ASE 2001, pp. 262--271 (2001).]]
[6]
Sagur Chaki, Edmund Clarke, Alex Groce, Somesh Jha, and Helmut Veith, "Modular verification of software components in C," IEEE Trans. on Software Engineering Vol. 30(6) pp. 388--402 (June 2004).]]
[7]
J. M. Cobleigh, L. A. Clarke, and L. J. Osterweil, "FLAVERS: A finite state verification technique for software systems," IBM Systems Journal Vol. 41(1) pp. 140--165 (2002).]]
[8]
James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby, "A language framework for expressing checkable properties of dynamic software," SPIN 2000, pp. 205--223 (2000).]]
[9]
James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Pasareanu, Robby, and Hongjun Zheng, "Bandera: extracting finite-state models from Java source code," ICSE 2000, pp. 439-448 (May 2000).]]
[10]
Manuvir Das, Sorin Lerner, and Mark Seigle, "ESP: Path-sensitive program verification in polynomial time," Proc. PLDI 2002, (June 2002).]]
[11]
Carolyn K. Duby, Scott Meyers, and Steven P. Reiss, "CCEL: a metalanguage for C++," Proc. Second Usenix C++ Conference, (August 1992).]]
[12]
Matthew B. Dwyer and John Hatcliff, "Slicing software for model construction," Proc. 1999 ACM Workshop on Partial Evaluation and Program Manipulation, pp. 105--118 (1999).]]
[13]
Matthew B. Dwyer, George S. Avrunin, and James C. Corbett, "Patterns in property specifications for finite-state verification," Proc. ICSE 99, pp. 411--420 (1999).]]
[14]
Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem, "Checking system rules using system-specific, programmer-written compiler extensions," Proc. 6th USENIX Conf. on Operating Systems Design and Implementation, (2000).]]
[15]
David Evans, John Guttag, James Horning, and Yang Meng Tan, "LCLint: a tool for using specifications to check code," Software Engineering Notes Vol. 19(5) pp. 87--96 (December 1994).]]
[16]
Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides, Design Patterns, Addison-Wesley (1995).]]
[17]
Klaus Havelund and Jens Ulrik Skakkebaek, "Applying model checking in Java verification," Proc. 5th and 6th SPIN Workshop, Lecture Notes in Computer Science Vol. 1680 pp. 216--231 Springer-Verlag, (1999).]]
[18]
Klaus Havelund and Thomas Pressburger, "Model checking Java programs using Java Pathfinder," Intl Journal on Software Tools for Technology Transfer Vol. 2(4)(April 2000).]]
[19]
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre, "Lazy abstraction," Proc. POPL '02, pp. 58--70 (2002).]]
[20]
Thomas A. Henzinger, Ranjit Jhala, Rpak Majumdar, and Kenneth L. McMillan, "Abstraction from proofs," Proc. POPL '04, pp. 232--244 (2004).]]
[21]
Gerard J. Holzmann and Margaret H. Smith, "Software model checking," Forte, pp. 481--497 (1999).]]
[22]
Gerard J. Holzmann and Margaret H. Smith, "Software model checking: extractin verification models from source code," Software Testing, Verification, and Reliability Vol. 11(2) pp. 65--79 (2001).]]
[23]
Daniel Jackson and Alan Fekete, "Lightweight analysis of object interactions," Proc TACS 2001, Springer-Verlag LNCS 2215, pp. 492--513 (2001).]]
[24]
G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm, and W. Griswold, "An Overview of AspectJ," in European Conference on Object-Oriented Programming, (2001).]]
[25]
I. Lee, S. Kannan, M. Kim, O. Sololsky, and M. Viswanathan, "Runtime assurance based on formal specifications," Intl. Conf. on Parallel and Distributed Processing Techniques and Applications, (June 1999).]]
[26]
Flavio Lerda and Willem Visser, "Addressing dynamic issues of program model checking," Lecture Notes in Computer Science, Proc. 8th SPIN Workship Vol. 2057 pp. 80--102 (2001).]]
[27]
G. Ramalingam, Alex Warshavsky, John Field, Deepak Goyal, and Mooly Sagiv, "Deriving specialized program analyses for certifying component-client conformance," PDLI 2002, pp. 83--94 (June 2002).]]
[28]
Steven P. Reiss, "Checking event-based specifications in Java systems," Proc. SoftMC 2005, (July 2005).]]
[29]
D. M. Ritchie, S. C. Johnson, M. E. Lesk, and B. W. Kernighan, "The C programming language," Bell Systems Tech. J. Vol. 57(6) pp. 1991--2020 (1978).]]
[30]
Willem Visser, Seung Joon Park, and John Penix, "Using predicate abstraction to reduce object-oriented programs for model checking," Proc. ACM SIGSOFT Workshop on Formal Methods in Software Practice, (August 2000).]]
[31]
Willem Visser, Klaus Havelund, Guillaume Brat, and Seung Joon Park, "Model checking programs," Automated Software Engineering Journal Vol. 10(2)(April 2003).]]

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
AADEBUG'05: Proceedings of the sixth international symposium on Automated analysis-driven debugging
September 2005
172 pages
ISBN:1595930507
DOI:10.1145/1085130
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 September 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. automata
  2. components
  3. finite-state
  4. flow analysis
  5. specifications
  6. verification

Qualifiers

  • Article

Conference

AADEBUG05

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)SPIDER: Specification-Based Integration Defect RevealerTools and Methods of Program Analysis10.1007/978-3-031-50423-5_10(107-119)Online publication date: 3-Jan-2024
  • (2011)Mining temporal specifications from object usageAutomated Software Engineering10.1007/s10515-011-0084-118:3-4(263-292)Online publication date: 1-Dec-2011
  • (2010)API conformance verification for Java programsProceedings of the 12th international conference on Formal engineering methods and software engineering10.5555/1939864.1939882(188-203)Online publication date: 17-Nov-2010
  • (2010)Deriving Framework Usages Based on Behavioral ModelsIEICE Transactions on Information and Systems10.1587/transinf.E93.D.733E93-D:4(733-744)Online publication date: 2010
  • (2010)API Conformance Verification for Java ProgramsFormal Methods and Software Engineering10.1007/978-3-642-16901-4_14(188-203)Online publication date: 2010
  • (2009)Mining Temporal Specifications from Object UsageProceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2009.30(295-306)Online publication date: 16-Nov-2009
  • (2007)Detecting object usage anomaliesProceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering10.1145/1287624.1287632(35-44)Online publication date: 7-Sep-2007
  • (2006)Incremental Maintenance of Software ArtifactsIEEE Transactions on Software Engineering10.1109/TSE.2006.9132:9(682-697)Online publication date: 1-Sep-2006

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media