We present a theory of timed interfaces, which is capable of specifying both the timing of the inputs a component expects from the environment, and the timing of the outputs it can produce. Two timed interfaces are compatible if there is a way to use them together such that their timing expectations are met. Our theory provides algorithms for checking the compatibility between two interfaces and for deriving the composite interface; the theory can thus be viewed as a type system for real-time interaction. Technically, a timed interface is encoded as a timed game between two players, representing the inputs and outputs of the component. The algorithms for compatibility checking and interface composition are thus derived from algorithms for solving timed games.
Unable to display preview. Download preview PDF.
- Abr96.S. Abramsky. Semantics of interaction. In Trees in Algebra and Programming, volume 1059 of Lect. Notes in Comp. Sci., page 1. Springer, 1996.Google Scholar
- AH97.R. Alur and T.A. Henzinger. Modularity for timed and hybrid systems. In Concurrency Theory, volume 1243 of Lect. Notes in Comp. Sci., pages 74–88. Springer, 1997.Google Scholar
- AMPS98.E. Asarin, O. Maler, A. Pnueli, and J. Sifakis. Controller synthesis for timed automata. In Proc. IFAC Symp. System Structure and Control, pages 469–474. Elsevier, 1998.Google Scholar
- CRR02.S. Chaki, S.K. Rajamani, and J. Rehof. Types as models: Model checking message-passing programs. In Proc. Symp. Principles of Programming Languages, pages 45–57. ACM, 2002.Google Scholar
- dAH01a.L. de Alfaro and T.A. Henzinger. Interface automata. In Proc. Symp. Foundations of Software Engineering, pages 109–120. ACM, 2001.Google Scholar
- dAH01b.L. de Alfaro and T.A. Henzinger. Interface theories for component-based design. In Embedded Software, volume 2211 of Lect. Notes in Comp. Sci., pages 148–165. Springer, 2001.Google Scholar
- dAHM01.L. de Alfaro, T.A. Henzinger, and R. Majumdar. Symbolic algorithms for infinite-state games. In Concurrency Theory, volume 2154 of Lect. Notes in Comp. Sci., pages 536–550. Springer, 2001.Google Scholar
- Dil88.D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, 1988.Google Scholar
- EJ91.E.A. Emerson and C.S. Jutla. Tree automata, mu-calculus, and determinacy. In Proc. Symp. Foundations of Computer Science, pages 368–377. IEEE Computer Society, 1991.Google Scholar
- MMT91.M. Merritt, F. Modugno, and M. Tuttle. Time constrained automata. In Concurrency Theory, volume 527 of Lect. Notes in Comp. Sci., pages 408–423. Springer, 1991.Google Scholar
- MPS95.O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In Theoretical Aspects of Computer Science, volume 900 of Lect. Notes in Comp. Sci., pages 229–242. Springer, 1995.Google Scholar
- RR01.S.K. Rajamani and J. Rehof. A behavioral module system for the pi-calculus. In Static Analysis Symposium, volume 2126 of Lect. Notes in Comp. Sci., pages 375–394. Springer, 2001.Google Scholar
- Tho90.W. Thomas. Automata on infinite objects. In J. van Leeuwen, ed., Handbook of Theoretical Computer Science, volume B, pages 135–191. Elsevier, 1990.Google Scholar
- Yi90.Wang Yi. Real-time behaviour of asynchronous agents. In Concurrency Theory, volume 458 of Lect. Notes in Comp. Sci., pages 502–520. Springer, 1990.Google Scholar