Abstract
We present interface models that describe both the input assumptions of a component, and its output behavior. By enabling us to check that the input assumptions of a component are met in a design, interface models provide a compatibility check for component-based design. When refining a design into an implementation, interface models require that the output behavior of a component satisfies the design specification only when the input assumptions of the specification are satisfied, yielding greater flexibility in the choice of implementations. Technically, our interface models are games between two players, Input and Output; the duality of the players accounts for the dual roles of inputs and outputs in composition and refinement. We present two interface models in detail, one for a simple synchronous form of interaction between components typical in hardware, and the other for more complex synchronous interactions on bidirectional connections. As an example, we specify the interface of a bidirectional bus, with the input assumption that at any time at most one component has write access to the bus. For these interface models, we present algorithms for compatibility and refinement checking, and we describe efficient symbolic implementations.
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 grant CCR-9988172, the SRC grant 99-TJ-683.003, and the NSF CAREER award CCR-0132780.
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
M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable concurrent program specifications. In Proc. 16th Int. Colloq. Aut. Lang. Prog., volume 372 of Lect. Notes in Comp. Sci., pages 1–17. Springer-Verlag, 1989.
S. Abramsky. Games in the semantics of programming languages. In Proc. of the 11th Amsterdam Colloquium, pages 1–6. ILLC, Dept. of Philosophy, University of Amsterdam, 1997.
S. Abramsky, S. Gay, and R. Nagarajan. A type-theoretic approach to deadlock-freedom of asynchronous systems. In TACS’97: Theoretical Aspects of Computer Software. Third International Symposium, 1997.
R. Alur and T. A. Henzinger. Reactive modules. Formal Methods in System Design, pages 7–48, 1999.
R. Alur, T. A. Henzinger, O. Kupferman, and M. Y. Vardi. Alternating refinement relations. In CONCUR 97: Concurrency Theory, volume 1466 of Lect. Notes in Comp. Sci., pages 163–178. Springer-Verlag, 1998.
R. Alur, T. A. Henzinger, F. Y. C. Mang, S. Qadeer, S. K. Rajamani, and S. Tasiran. Mocha: modularity in model checking. In CAV 98: Proc. of 10th Conf. on Computer Aided Verification, volume 1427 of Lect. Notes in Comp. Sci., pages 521–525. Springer-Verlag, 1998.
E. Clarke, K. McMillan, S. Campos, and V. Hartonas-Garmhausen. Symbolic model checking. In CAV 96: Proc. of 8th Conf. on Computer Aided Verification, volume 1102 of Lect. Notes in Comp. Sci., pages 419–422. Springer-Verlag, 1996.
L. de Alfaro, R. Alur, R. Grosu, T. Henzinger, M. Kang, R. Majumdar, F. Mang, C. Meyer-Kirsch, and B. Y. Wang. Mocha: A model checking tool that exploits design structure. In ICSE 01: Proceedings of the 23rd International Conference on Software Engineering, 2001.
L. de Alfaro and T. A. Henzinger. Interface automata. In Proc. of 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on Foun-dations of Software Engineering (ESEC/FSE), pages 109–120. ACM Press, 2001.
L. de Alfaro and T. A. Henzinger. Interface theories for component-based design. In EMSOFT 01: Proc. of First Int. Workshop on Embedded Software, volume 2211 of Lect. Notes in Comp. Sci., pages 148–165. Springer-Verlag, 2001.
D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, 1988.
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
N. A. Lynch. Distributed Algorithms. Morgan-Kaufmann, 1996.
N. A. Lynch and M. Tuttle. Hierarcical correctness proofs for distributed algorithms. In Proc. of 6th ACM Symp. Princ. of Dist. Comp., pages 137–151, 1987.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.
R. Milner. An algebraic definition of simulation between programs. In Proc. of Second Int. Joint Conf. on Artificial Intelligence, pages 48–489. The British Computer Society, 1971.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
J. C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.
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., Mang, F.Y.C. (2002). Synchronous and Bidirectional Component Interfaces. 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_34
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_34
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