article

Synthesis of interface specifications for Java classes

Authors:

Wonhong NamAuthors Info & Claims

ACM SIGPLAN Notices, Volume 40, Issue 1

Pages 98 - 109

https://doi.org/10.1145/1047659.1040314

Published: 12 January 2005 Publication History

Abstract

While a typical software component has a clearly specified (static) interface in terms of the methods and the input/output types they support, information about the correct sequencing of method calls the client must invoke is usually undocumented. In this paper, we propose a novel solution for automatically extracting such temporal specifications for Java classes. Given a Java class, and a safety property such as "the exception E should not be raised", the corresponding (dynamic) interface is the most general way of invoking the methods in the class so that the safety property is not violated. Our synthesis method first constructs a symbolic representation of the finite state-transition system obtained from the class using predicate abstraction. Constructing the interface then corresponds to solving a partial-information two-player game on this symbolic graph. We present a sound approach to solve this computationally-hard problem approximately using algorithms for learning finite automata and symbolic model checking for branching-time logics. We describe an implementation of the proposed techniques in the tool JIST--- Java Interface Synthesis Tool---and demonstrate that the tool can construct interfaces accurately and efficiently for sample Java2SDK library classes.

References

[1]

S. Abramsky. Semantics of interaction. Technical report, Oxford University, 2002.

[2]

R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):1--42, 2002.

Digital Library

[3]

G. Ammons, R. Bodík, and J. Larus. Mining specifications. In Proc. 29th ACM POPL, pages 4--16, 2002.

Digital Library

[4]

D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75:87--106, 1987.

Digital Library

[5]

T. Ball, R. Majumdar, T.D. Millstein, and S.K. Rajamani. Automatic predicate abstraction of C programs. In Proc. PLDI, ACM SIGPLAN Notices 36(5), pages 203--213, 2001.

Digital Library

[6]

T. Ball and S.K. Rajamani. The SLAM project: Debugging system software via static analysis. In Proc. 29th ACM POPL, pages 1--3, 2002.

Digital Library

[7]

H. Barringer, C.S. Pasareanu and D. Giannakopolou. Proof rules for automated compositional verification through learning. In Proc. of the 2nd Int'l Workshop on Specification and Verification of Component Based Systems, 2003.

[8]

T. Berg, B. Jonsson, M. Leucker, and M. Saksena. Insights to Angluin's learning. In Proc. of International Workshop on Software Verification and Validation, 2003.

[9]

A. Chakrabarti, L. de Alfaro, T.A. Henzinger, M. Jurdzinski, and F. Mang. Interface compatibility checking for software modules. In Proc. 14th CAV, LNCS 2404, Springer, pages 428--441, 2002.

Digital Library

[10]

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV Version 2: An Opensource tool for symbolic model checking. In Proc. 14th CAV, LNCS 2404, Springer, pages 359--364, 2002.

Digital Library

[11]

E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. of Workshop on Logic of Programs, pages 52--71, 1981.

Digital Library

[12]

J.M. Cobleigh, D. Giannakopoulou, and C.S. Pasareanu. Learning assumptions for compositional verification. In Proc. 9th TACAS, LNCS 2619, Springer, pages 331--346, 2003.

Digital Library

[13]

J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C.S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proc. 22nd ICSE, pages 439--448, 2000.

Digital Library

[14]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM POPL, pages 238--252, 1977.

Digital Library

[15]

P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. 5th ACM POPL, pages 84--96, 1978.

Digital Library

[16]

L. de Alfaro and T.A. Henzinger. Interface automata. In Proc. 9th ACM FSE, pages 109--120, 2001.

Digital Library

[17]

R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. In Proc. ACM POPL, pages 59--69, 2001.

Digital Library

[18]

D. Giannakopoulou, C.S. Pasareanu and H. Barringer. Assumption generation for software component verification. In Proc. 17th ASE, pages 3--12, 2002.

Digital Library

[19]

S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Proc. 9th CAV, LNCS 1254, pages 72--83, 1997.

Digital Library

[20]

T.A. Henzinger, R. Jhala, R. Majumdar, K.L. McMillan. Abstractions from proofs. In Proc. 31st ACM POPL, pages 232--244, 2004.

Digital Library

[21]

T.A. Henzinger, R. Jhala, R. Majumdar, G. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In Proc. of CAV, LNCS 2404, pages 526--538. Springer, 2002.

Digital Library

[22]

G. Holzmann and M. Smith. Software model checking - extracting verification models from source code. In Formal Methods for Protocol Engineering and Distributed Systems, pages 481--497, 1999.

Digital Library

[23]

F. Logozzo. Automatic inference of class invariants. In Proc. of VMCAI, LNCS 2937, pages 211--222, 2004.

[24]

J. Nimmer and M. Ernst. Automatic generation of program specification. In Proc. of ISSTA, pages 229--239, 2002.

Digital Library

[25]

G. Ramalingam, A. Warshavsky, J. Field, D. Goyal and M. Sagiv. Deriving specialized program analyses for certifying component-client conformance. In ACM PLDI, pages 83--94, 2002.

Digital Library

[26]

J.H. Reif. Universal games of incomplete information. In Proc. of the 11th ACM symposium on Theory of computing, pages 288--308. ACM Press, 1979.

Digital Library

[27]

R. L. Rivest and R. E. Schapire. Inference of finite automata using homing sequences. Information and Computation, 103(2):299--347, 1993.

Digital Library

[28]

W. Thomas. Infinite games and verification. In Proc. 14th CAV, LNCS 2404, pages 58--64. Springer, 2002.

Digital Library

[29]

O. Tkachuk, M.B. Dwyer, and C.S. Pasareanu. Automated environment generation for software model checking. In Proc. 18th ASE, pages 116--127, 2003.

Digital Library

[30]

R. Vallée-Rai, L. Hendren, V. Sundaresan, E.G. Patrick Lam, and P. Co. Soot - a Java optimization framework. In Proc. CASCON, pages 125--135, 1999.

[31]

D. Walker. A type system for expressive security policies. In Proc. 27th ACM POPL, pages 254--267, 2000.

Digital Library

[32]

J. Whaley, M.C. Martin, and M.S. Lam. Automatic extraction of object-oriented component interfaces. In Proc. ISSTA, pages 218--228, 2002.

Digital Library

Cited By

Ahmed MNadimi BZheng H(2024)AutoModel: Automatic Synthesis of Models From Communication Traces of SoC DesignsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.336259843:7(2191-2204)Online publication date: 5-Feb-2024
https://dl.acm.org/doi/10.1109/TCAD.2024.3362598
Astorga AHsieh CMadhusudan PMitra S(2023)Perception Contracts for Safety of ML-Enabled SystemsProceedings of the ACM on Programming Languages10.1145/36228757:OOPSLA2(2196-2223)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622875
Berndt SLiśkiewicz MLutter MReischuk R(2022)Learning residual alternating automataInformation and Computation10.1016/j.ic.2022.104981289:PAOnline publication date: 1-Nov-2022
https://dl.acm.org/doi/10.1016/j.ic.2022.104981
Show More Cited By

Index Terms

Synthesis of interface specifications for Java classes
1. Software and its engineering
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Synthesis of interface specifications for Java classes
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

While a typical software component has a clearly specified (static) interface in terms of the methods and the input/output types they support, information about the correct sequencing of method calls the client must invoke is usually undocumented. In ...
Tools to generate and check consistency of model classes for Java PathFinder

Java PathFinder (JPF) is a model checker for Java applications. Like any other model checker, JPF has to combat the notorious state space explosion problem. Since JPF is a JVM, it can only model check Java bytecode and needs to handle native calls ...
SAT-based counterexample-guided abstraction refinement

We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 40, Issue 1

Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

391 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1047659

Issue’s Table of Contents

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
402 pages
ISBN:158113830X
DOI:10.1145/1040305
General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

Copyright © 2005 ACM.

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2005

Published in SIGPLAN Volume 40, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

315
Total Citations
View Citations
1,373
Total Downloads

Downloads (Last 12 months)22
Downloads (Last 6 weeks)4

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ahmed MNadimi BZheng H(2024)AutoModel: Automatic Synthesis of Models From Communication Traces of SoC DesignsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.336259843:7(2191-2204)Online publication date: 5-Feb-2024
https://dl.acm.org/doi/10.1109/TCAD.2024.3362598
Astorga AHsieh CMadhusudan PMitra S(2023)Perception Contracts for Safety of ML-Enabled SystemsProceedings of the ACM on Programming Languages10.1145/36228757:OOPSLA2(2196-2223)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622875
Berndt SLiśkiewicz MLutter MReischuk R(2022)Learning residual alternating automataInformation and Computation10.1016/j.ic.2022.104981289:PAOnline publication date: 1-Nov-2022
https://dl.acm.org/doi/10.1016/j.ic.2022.104981
Salva SBlot E(2022)Learning of behavioural models and dependency graphs for communicating systems with CkTailv2International Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-022-00651-524:4(529-548)Online publication date: 1-Aug-2022
https://dl.acm.org/doi/10.1007/s10009-022-00651-5
Ye HRao JShi YLi Z(2021)ProExtor: Mining API Protocols for Program Vulnerability DetectionProceedings of the 3rd International Conference on Advanced Information Science and System10.1145/3503047.3503100(1-7)Online publication date: 26-Nov-2021
https://dl.acm.org/doi/10.1145/3503047.3503100
Ali SSun HZhao Y(2021)Model learning: a survey of foundations, tools and applicationsFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-019-9212-z15:5Online publication date: 1-Oct-2021
https://dl.acm.org/doi/10.1007/s11704-019-9212-z
Pick LFedyukovich GGupta A(2021)Unbounded Procedure Summaries from Bounded EnvironmentsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_14(291-324)Online publication date: 12-Jan-2021
https://doi.org/10.1007/978-3-030-67067-2_14
Salva SBlot E(2020)Model generation of component-based systemsSoftware Quality Journal10.1007/s11219-019-09485-y28:2(789-819)Online publication date: 1-Jun-2020
https://dl.acm.org/doi/10.1007/s11219-019-09485-y
Mrowca ANocker MSteinhorst SGünnemann S(2019)Learning Temporal Specifications from Imperfect Traces Using Bayesian InferenceProceedings of the 56th Annual Design Automation Conference 201910.1145/3316781.3317847(1-6)Online publication date: 2-Jun-2019
https://dl.acm.org/doi/10.1145/3316781.3317847
Narayan AFischmeister S(2019)Mining Time for Timed Regular Specifications2019 IEEE International Conference on Systems, Man and Cybernetics (SMC)10.1109/SMC.2019.8914490(63-69)Online publication date: Oct-2019
https://doi.org/10.1109/SMC.2019.8914490
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents