Citation
Stavros Tripakis, Christos Stergiou, Manfred Broy, Edward A. Lee. "Error-Completion in Interface Theories". International SPIN Symposium on Model Checking of Software, 2013.

Abstract
Interface theories are compositional theories where components are represented as abstract, formal interfaces which describe the component's input/output behavior. A key characteristic of interface theories is that interfaces are non-input-complete, meaning that they allow specification of illegal inputs. As a result of non-input-completeness, interface theories use game-theoretic definitions of composition and refinement, which are both conceptually and computationally more complicated than standard notions of composition and refinement that work with input-complete models. In this paper we propose a lossless transformation, called error-completion, which allows to transform a non-input-complete interface into an input-complete interface while preserving and allowing to retrieve completely the information on illegal inputs. We show how to perform composition of relational interfaces on the error-complete domain. We also show that refinement of such interfaces is equivalent to standard implication of their error-completions.

Electronic downloads

• error_complete.pdf · application/pdf · 332 kbytes
• http://dx.doi.org/10.1007/978-3-642-39176-7_22. (In Proceedings of SPIN 2013, pp 358-375.)

• HTML

  Stavros Tripakis, Christos Stergiou, Manfred Broy, Edward A.
  Lee. <a
  href="http://chess.eecs.berkeley.edu/pubs/987.html"
  >Error-Completion in Interface Theories</a>,
  International SPIN Symposium on Model Checking of Software,
  2013.

• Plain text

  Stavros Tripakis, Christos Stergiou, Manfred Broy, Edward A.
  Lee. "Error-Completion in Interface Theories".
  International SPIN Symposium on Model Checking of Software,
  2013.

• BibTeX

  @inproceedings{TripakisStergiouBroyLee13_ErrorCompletionInInterfaceTheories,
      author = {Stavros Tripakis and Christos Stergiou and Manfred
                Broy and Edward A. Lee},
      title = {Error-Completion in Interface Theories},
      booktitle = {International SPIN Symposium on Model Checking of
                Software},
      year = {2013},
      abstract = {Interface theories are compositional theories
                where components are represented as abstract,
                formal interfaces which describe the component's
                input/output behavior. A key characteristic of
                interface theories is that interfaces are
                non-input-complete, meaning that they allow
                specification of illegal inputs. As a result of
                non-input-completeness, interface theories use
                game-theoretic definitions of composition and
                refinement, which are both conceptually and
                computationally more complicated than standard
                notions of composition and refinement that work
                with input-complete models. In this paper we
                propose a lossless transformation, called
                error-completion, which allows to transform a
                non-input-complete interface into an
                input-complete interface while preserving and
                allowing to retrieve completely the information on
                illegal inputs. We show how to perform composition
                of relational interfaces on the error-complete
                domain. We also show that refinement of such
                interfaces is equivalent to standard implication
                of their error-completions. },
      URL = {http://chess.eecs.berkeley.edu/pubs/987.html}
  }
  

Posted by Christos Stergiou on 22 Apr 2013.
Groups: actionwebs
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.