TY - GEN
T1 - Error-completion in interface theories
AU - Tripakis, Stavros
AU - Stergiou, Christos
AU - Broy, Manfred
AU - Lee, Edward A.
N1 - Funding Information:
This work was supported in part by the iCyPhy Center (supported by IBM and United Technologies), the CHESS Center (supported by awards NSF #0720882 (CSR-EHS: PRET) and #0931843 (ActionWebs), NRL #N0013-12-1-G015, Bosch, National Instruments, and Toyota), and by the NSF Expeditions in Computing project ExCAPE: Expeditions in Computer Augmented Program Engineering.
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84884912717&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-39176-7_22
DO - 10.1007/978-3-642-39176-7_22
M3 - Conference contribution
AN - SCOPUS:84884912717
SN - 9783642391750
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 358
EP - 375
BT - Model Checking Software - 20th International Symposium, SPIN 2013, Proceedings
PB - Springer Verlag
T2 - 20th International Symposium on Model Checking Software, SPIN 2013
Y2 - 8 July 2013 through 9 July 2013
ER -