Evan Driscoll
Thomas Reps
ABSTRACT
This paper addresses the problem of identifying incompatibilities between two programs that operate in a producer/consumer relationship. It describes the techniques that are incorporated in a tool called PCCA (Producer-Consumer Conformance Analyzer), which attempts to (i) determine whether the consumer is prepared to accept all messages that the producer can emit, or (ii) find a counter-example: a message that the producer can emit and the consumer considers ill-formed.
- C. Allauzen, M. Riley, J. Schalkwyk, W. Skut, and M. Mohri. OpenFst: A general and efficient weighted finite-state transducer library. In CIAA, 2007. Google Scholar
Digital Library
- R. Alur and P. Madhusudan. Visibly pushdown languages. In STOC, 2004. Google ScholarDigital Library
- R. Alur and P. Madhusudan. Adding nesting structure to words. J. ACM, 56(3), 2009. Google ScholarDigital Library
- V. Bono, C. Messa, and L. Padovani. Typing copyless message passing. In ESOP, 2011. Google ScholarDigital Library
- A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model checking. In CONCUR, 1997. Google ScholarDigital Library
- A. Burton, A. Thakur, E. Driscoll,, and T. Reps. WALi: Nested-word automata. TR-1675, Comp. Sci. Dept., Univ. of Wisconsin, Madison, WI, July 2010.Google Scholar
- J. Caballero and D. Song. Polyglot: Automatic extraction of protocol format using dynamic binary analysis. In CCS, 2007. Google ScholarDigital Library
- D. Caucal. On the regular structure of prefix rewriting. In CAAP, 1990. Google ScholarDigital Library
- E. Clarke, N. Sharygina, and N. Sinha. Program compatibility approaches. In FMCO, 2005. Google ScholarDigital Library
- CodeSurfer system. www.grammatech.com/products/codesurfer.Google Scholar
- P. Collingbourne and P. Kelly. Inference of session types from control flow. ENTCS, 238(6), 2010. Google ScholarDigital Library
- W. Cui, M. Peinado, K. Chen, H. Wang, and L. Irun-Briz. Tupni: Automatic reverse engineering of input formats. In CCS, 2008. Google ScholarDigital Library
- M. Fähndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. Hunt, J. R. Larus, and S. Levi. Language support for fast and reliable message-based communication in Singularity OS. In EuroSys. 2006.Google Scholar
- A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. ENTCS, 9, 1997.Google Scholar
- S. Gay, V. Vasconcelos, and A. Ravara. Session types for inter-process communication. TR-2003-133, Dept. of Computing Sci., Univ. of Glasgow, March 2003.Google Scholar
- S. Hallem, B. Chelf, Y. Xie, and D. Engler. A system and language for building system-specific, static analyses. In PLDI, 2002. Google ScholarDigital Library
- K. Honda. Types for dyadic interaction. In CONCUR. 1993. Google ScholarDigital Library
- J. Hornick. Icons. http://msdn.microsoft.com/en-us/library/ms997538.aspx.Google Scholar
- R. Hu, D. Kouzapas, O. Pernet, N. Yoshida, and K. Honda. Type-safe eventful sessions in java. In ECOOP. 2010. Google ScholarDigital Library
- N. Kidd, A. Lal, and T. Reps. WALi: The Weighted Automaton Library, 2007. www.cs.wisc.edu/wpis/wpds/download.php.Google Scholar
- R. Komondoor and G. Ramalingam. Recovering data models via guarded dependences. In WCRE, 2007. Google ScholarDigital Library
- T. Kremenek, P. Twohey, G. Back, A. Ng, and D. Engler. From uncertainty to belief: inferring the specification within. In OSDI, 2006. Google ScholarDigital Library
- J. Lim, T. Reps, and B. Liblit. Extracting output formats from executables. In WCRE, 2006. Google ScholarDigital Library
- Z. Lin, X. Jiang, D. Xu, and X. Zhang. Automatic protocol format reverse engineering through context-aware monitored execution. In NDSS, 2008.Google Scholar
- Z. Lin and X. Zhang. Deriving input syntactic structure from execution. In FSE, 2008. Google ScholarDigital Library
- B. Liskov and J. Wing. Behavioral subtyping using invariants and constraints. In H. Bowman and J. Derrick, editors, Formal Methods for Distributed Processing: An Object Oriented Approach. Cambridge Univ. Press, 2001. Google ScholarDigital Library
- S. McCamant and M. Ernst. Early identification of incompatibilities in multicomponent upgrades. In ECOOP, 2004.Google ScholarCross Ref
- L. Mezzina. How to infer finite session types in a calculus of services and sessions. In D. Lea and G. Zavattaro, editors, Coordination Models and Languages. 2008. Google ScholarDigital Library
- O. Nierstrasz and M. Papathomas. Viewing object as patterns of communicating agents. In OOPSLA, 1990. Google ScholarDigital Library
- S. Rajamani and J. Rehof. Conformance checking for models of asynchronous message passing software. In CAV, 2002. Google ScholarDigital Library
- T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, 1995. Google ScholarDigital Library
- S. Schwoon. Model-Checking Pushdown Systems. PhD thesis, TUM, Munich, Germany, July 2002.Google Scholar
- Z. Stengel and T. Bultan. Analyzing Singluarity channel contracts. In ISSTA. 2009. Google ScholarDigital Library
- G. Wondracek, P. Comparetti, C. Kruegel, and E. Kirda. Automatic network protocol analysis. In NDSS, 2008.Google Scholar
Index Terms
- Checking conformance of a producer and a consumer
Recommendations
Consumer Addressability and Customized Pricing
The increasing availability of customer information is giving many firms the ability to reach and customize price and other marketing efforts to the tastes of the individual consumer. This ability is labeled as consumer addressability. Consumer ...
Shopping Behavior and Consumer Preference for Store Price Format: Why "Large Basket" Shoppers Prefer EDLP
<P>In recent years, the supermarket industry has become increasingly competitive. One outcome has been the proliferation of a variety of pricing formats, and considerable debate among academics and practitioners about how these formats affect consumers' ...
Research Note Consumer Addressability and Customized Pricing
The increasing availability of customer information is giving many firms the ability to reach and customize price and other marketing efforts to the tastes of the individual consumer. This ability is labeled as consumer addressability. Consumer ...
Comments