*banner
 

Error-Completion in Interface Theories
Stavros Tripakis, Christos Stergiou, Manfred Broy, Edward A. Lee

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

Citation formats  
  • 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.
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.

You are not logged in 
©2002-2014 Chess