Synchronous and bidirectional component interfaces Conference Paper

Author(s): Chakrabarti, Arindam; de Alfaro, Luca; Henzinger, Thomas A; Mang, Freddy Y
Title: Synchronous and bidirectional component interfaces
Title Series: LNCS
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.
Conference Title: CAV: Computer Aided Verification
Volume: 2404
Conference Dates: July 27-31, 2002
Conference Location: Copenhagen, Denmark
Publisher: Springer  
Location: Berlin, Heidelberg
Date Published: 2002-06-19
Start Page: 414
End Page: 427
Sponsor: 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.
DOI: 10.1007/3-540-45657-0_34
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work