*banner
 

An Interface Algebra for Real-time Components
Tom Henzinger, Slobodan Matic

Citation
Tom Henzinger, Slobodan Matic. "An Interface Algebra for Real-time Components". Proceedings of RTAS 2006, 253-263, April, 2006.

Abstract
We present an assume-guarantee interface algebra for real-time components. In our formalism a component implements a set of task sequences that share a resource. A component interface consists of an arrival rate function and a latency for each task sequence, and a capacity function for the shared resource. The interface specifies that the component guarantees certain task latencies depending on assumptions about task arrival rates and allocated resource capacities. Our algebra defines compatibility and refinement relations on interfaces. Interface compatibility can be checked on partial designs, even when some component interfaces are yet unknown. In this case interface composition computes as new assumptions the weakest constraints on the unknown components that are necessary to satisfy the specified guarantees. Interface refinement is defined in a way that ensures that compatible interfaces can be refined and implemented independently. Our algebra thus formalizes an interface-based design methodology that supports both the incremental addition of new components and the independent stepwise refinement of existing components. We demonstrate the flexibility and efficiency of the framework through simulation experiments.

Electronic downloads

Citation formats  
  • HTML
    Tom Henzinger, Slobodan Matic. <a
    href="http://chess.eecs.berkeley.edu/pubs/92.html"
    >An Interface Algebra for Real-time Components</a>,
    Proceedings of RTAS 2006, 253-263, April, 2006.
  • Plain text
    Tom Henzinger, Slobodan Matic. "An Interface Algebra
    for Real-time Components". Proceedings of RTAS 2006,
    253-263, April, 2006.
  • BibTeX
    @inproceedings{HenzingerMatic06_InterfaceAlgebraForRealtimeComponents,
        author = {Tom Henzinger and Slobodan Matic},
        title = {An Interface Algebra for Real-time Components},
        booktitle = {Proceedings of RTAS 2006},
        pages = {253-263},
        month = {April},
        year = {2006},
        abstract = {We present an assume-guarantee interface algebra
                  for real-time components. In our formalism a
                  component implements a set of task sequences that
                  share a resource. A component interface consists
                  of an arrival rate function and a latency for each
                  task sequence, and a capacity function for the
                  shared resource. The interface specifies that the
                  component guarantees certain task latencies
                  depending on assumptions about task arrival rates
                  and allocated resource capacities. Our algebra
                  defines compatibility and refinement relations on
                  interfaces. Interface compatibility can be checked
                  on partial designs, even when some component
                  interfaces are yet unknown. In this case interface
                  composition computes as new assumptions the
                  weakest constraints on the unknown components that
                  are necessary to satisfy the specified guarantees.
                  Interface refinement is defined in a way that
                  ensures that compatible interfaces can be refined
                  and implemented independently. Our algebra thus
                  formalizes an interface-based design methodology
                  that supports both the incremental addition of new
                  components and the independent stepwise refinement
                  of existing components. We demonstrate the
                  flexibility and efficiency of the framework
                  through simulation experiments.},
        URL = {http://chess.eecs.berkeley.edu/pubs/92.html}
    }
    

Posted by Slobodan Matic on 11 May 2006.
Groups: chess chesslocal
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess