Abstract
We present a formal methodology and tool for uncovering errors in the interaction of software modules. Our methodology consists of a suite of languages for defining software interfaces, and algorithms for checking interface compatibility. We focus on interfaces that explain the method-call dependencies between software modules. Such an interface makes assumptions about the environment in the form of call and availability constraints. A call constraint restricts the accessibility of local methods to certain external methods. An availability constraint restricts the accessibility of local methods to certain states of the module. For example, the interface for a file server with local methods open and read may assert that a file cannot be read without having been opened. Checking interface compatibility requires the solution of games, and in the presence of availability constraints, of pushdown games. Based on this methodology, we have implemented a tool that has uncovered incompatibilities in TinyOS, a small operating system for sensor nodes in adhoc networks.
This research was supported in part by the AFOSR grant F49620-00-1-0327, the DARPA grant F33615-00-C-1693, the MARCO grant 98-DT-660, the NSF grants CCR-9988172, CCR-0085949, CCR-0132780, the SRC grant 99-TJ-683, and the Polish KBN grant 7-T11C-027-20.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S. Abramsky. Semantics of Interaction. Lecture Notes, Oxford University, 2002.
R. Alur et al. jMocha: A model-checking tool that exploits design structure. Proc. Int. Conf. Software Engineering, pp. 835–836. IEEE, 2001.
R. Allen and D. Garlan. A formal basis for architectural connection. ACM Trans. Software Engineering &Methodology, 6:213–249, 1997.
A. Boujjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model checking. Concurrency Theory, LNCS 1243, pp. 135–150. Springer, 1997.
A. Beugnard, J.-M. Jézéquel, N. Plouzeau, and D. Watkins. Making components contract aware. IEEE Software, 16:38–45, 1999.
L. de Alfaro and T. A. Henzinger. Interface automata. Proc. Symp. Foundations of Software Engineering, pp. 109–120. ACM, 2001.
L. de Alfaro and T. A. Henzinger. Interface theories for component-based design. Embedded Software, LNCS 2211, pp. 148–165. Springer, 2001.
R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. Proc. Conf. Programming Language Design &Implementation, pp. 59–69. ACM, 2001.
D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. MIT Press, 1989.
J. Esparza and S. Schwoon. A BDD-based model checker for recursive programs. Computer-Aided Verification, LNCS 2102, pp. 324–336. Springer, 2001.
R. B. Findler, M. Latendresse, and M. Felleisen. Behavioral contracts and behavioral subtyping. Proc. Symp. Foundations of Software Engineering, pp. 229–236. ACM, 2001.
J. Foster, M. Fändrich, and A. Aiken. A theory of type qualifiers. Proc. Conf. Programming Language Design & Implementation, pp. 192–203. ACM, 1999.
J. Hill, R. Szewczyk, A. Woo, S. Hollar, D. Culler, and K. Pister. System architecture directions for networked sensors. Proc. Conf. Architectural Support for Programming Languages & Operating Systems, pp. 93–104. ACM, 2000.
J. R. Larus, S. K. Rajamani, and J. Rehof. Behavioral Types for Structured Asynchronous Programming. Technical Report, Microsoft Research, 2001.
D. C. Luckham and F. von Henke. An overview of Anna, a specification language for Ada. IEEE Software, 2:9–23, 1985.
D. L. Parnas. A technique for software module specification with examples. Communications of the ACM, 15:330–336, 1972.
D. S. Rosenblum. A practical approach to programming with assertions. IEEE Trans. Software Engineering, 21:19–31, 1995.
I. Walukiewicz. Pushdown processes: Games and model checking. Information and Computation, 164:234–263, 2001.
F. Somenzi. CUDD: CU decision diagram package. Technical Report, University of Colorado at Boulder, 1997.
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
Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Jurdziński, M., Mang, F.Y.C. (2002). Interface Compatibility Checking for Software Modules. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_35
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive