Designing and interoperability testing of distributed, application-level network protocols is complex. Windows, for example, supports currently more than 200 protocols, ranging from simple protocols for email exchange to complex ones for distributed file replication or real time communication. To fight this increasing complexity problem, we introduce a methodology and formal framework that uses model program composition to specify behavior of such protocols. A model program can be used to specify an increment of protocol functionality with a coherent purpose, which can be understood and analyzed separately. The overall behavior of a protocol can be defined by a composite model program, which defines how the individual parts interoperate.


Model Program Label Transition System Action Symbol Scenario Control Protocol Modeling 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Spec Explorer (released, January 2005),
  2. 2.
  3. 3.
    Avgustinov, P., Bodden, E., Hajiyev, E., Hendren, L., Lhoták, O., de Moor, O., Ongkingco, N., Sereni, D., Sittampalam, G., Tibble, J., Verbaere, M.: Aspects for trace monitoring. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol. 4262, pp. 20–39. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
    Batory, D.: A tutorial on feature oriented programming and the AHEAD tool suite. In: Lämmel, R., Saraiva, J., Visser, J. (eds.) GTTSE 2005. LNCS, vol. 4143, pp. 3–35. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Bjørner, N., de Moura, L.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). LNCS, vol. 4963, Springer, Heidelberg (2008)Google Scholar
  6. 6.
    Blass, A., Gurevich, Y.: Background, reserve, and gandy machines. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 1–17. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Blass, A., Gurevich, Y.: Ordinary interactive small-step algorithms, I. ACM Transactions on Computation Logic 7(2), 363–419 (2006)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)CrossRefzbMATHGoogle Scholar
  9. 9.
    Brinksma, E., Tretmans, J.: Testing Transition Systems: An Annotated Bibliography. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 187–193. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. 10.
    Calder, M., Kolberg, M., Magill, E.H., Reiff-Marganiec, S.: Feature interaction: a critical review and considered forecast. Computer Networks 41(1), 115–141 (2003)CrossRefzbMATHGoogle Scholar
  11. 11.
    Campbell, C., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., Veanes, M.: Testing concurrent object-oriented systems with Spec Explorer (extended abstract). In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 542–547. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Cottenier, T., van den Berg, A., Elrad, T.: Stateful aspects: the case for aspect-oriented modeling. In: AOM 2007, pp. 7–14. ACM, New York (2007)Google Scholar
  14. 14.
    de Alfaro, L.: Game models for open systems. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 269–289. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. 15.
    de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/FSE 2001, pp. 109–120. ACM, New York (2001)Google Scholar
  16. 16.
    de Moura, L., Bjørner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183–198. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    de Moura, L., Bjørner, N.: Model-based theory combination. In: 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), Berlin, Germany, July 2007, pp. 46–57 (2007)Google Scholar
  18. 18.
    Douence, R., Fradet, P., Südholt, M.: Aspect-Oriented Software Development. In: Trace-based Aspects, pp. 201–218. Addison Wesley, Reading (2004)Google Scholar
  19. 19.
    Elrad, T., Aksit, M., Kiczales, G., Lieberherr, K., Ossher, H.: Discussing aspects of AOP. Commun. ACM 44(10), 33–38 (2001)CrossRefGoogle Scholar
  20. 20.
    Frantzen, L., Tretmans, J., Willemse, T.: A symbolic framework for model-based testing. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds.) FATES 2006 and RV 2006. LNCS, vol. 4262, pp. 40–54. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  21. 21.
    Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. In: ISSTA 2002. Software Engineering Notes, vol. 27, pp. 112–122. ACM, New York (2002)Google Scholar
  22. 22.
    Grieskamp, W., Kicillof, N.: A schema language for coordinating construction and composition of partial behavior descriptions. In: 5th International Workshop on Scenarios and State Machines: Models, Algorithms and Tools (SCESM) (2006)Google Scholar
  23. 23.
    Grieskamp, W., Kicillof, N., Tillmann, N.: Action machines: a framework for encoding and composing partial behaviors. IJSEKE 16(5), 705–726 (2006)Google Scholar
  24. 24.
    Grieskamp, W., MacDonald, D., Kicillof, N., Nandan, A., Stobie, K., Wurden, F.: Model-based quality assurance of windows protocol documentation. In: First Intl. Conf. on Software Testing, Verification and Validation, ICST, Lillehammer, Norway (April 2008)Google Scholar
  25. 25.
    Gurevich, Y.: Specification and Validation Methods. In: Evolving Algebras 1993: Lipari Guide, pp. 9–36. Oxford University Press, Oxford (1995), Google Scholar
  26. 26.
    Gurevich, Y., Rossman, B., Schulte, W.: Semantic essence of asml. Theor. Comput. Sci. 343(3), 370–412 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Helander, J., Serg, R., Veanes, M., Roy, P.: Adapting futures: Scalability for real-world computing. In: Proc. 28th IEEE Real-Time Systems Symposium, pp. 105–116. IEEE, Los Alamitos (2007)Google Scholar
  28. 28.
    Hertel, C.: Implementing CIFS: The Common Internet File System. Prentice-Hall, Englewood Cliffs (2003)Google Scholar
  29. 29.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)zbMATHGoogle Scholar
  30. 30.
    Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-based Software Testing and Analysis with C#. Cambridge University Press, Cambridge (2007)CrossRefzbMATHGoogle Scholar
  31. 31.
    Keller, R.: Formal verification of parallel programs. Communications of the ACM, 371–384 (July 1976)Google Scholar
  32. 32.
    Lynch, N., Tuttle, M.: Hierarchical correctness proofs for distributed algorithms. In: 6th annual ACM Symposium on Principles of distributed computing, pp. 137–151. ACM, New York (1987)Google Scholar
  33. 33.
    Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI-Quarterly 2(3), 219–246 (1989)MathSciNetzbMATHGoogle Scholar
  34. 34.
    NModel (released, May 2007),
  35. 35.
    Utting, M., Legeard, B.: Practical Model-Based Testing - A tools approach. Elsevier Science, Amsterdam (2006)Google Scholar
  36. 36.
    Veanes, M., Bjørner, N., Raschke, A.: An SMT approach to bounded reachability analysis of model programs. In: Suzuki, K., Higashino, T., Yasumoto, K., El - Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 53–68. Springer, Heidelberg (2008)Google Scholar
  37. 37.
    Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L.: Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. In: Hierons, R., Bowen, J., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 39–76. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  38. 38.
    Veanes, M., Campbell, C., Schulte, W.: Composition of model programs. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574, pp. 128–142. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  39. 39.
    Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: Proc. ESEC/FSE-13, pp. 273–282. ACM, New York (2005)CrossRefGoogle Scholar
  40. 40.
    Veanes, M., Ernits, J., Campbell, C.: State isomorphism in model programs with abstract data structures. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574, pp. 112–127. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  41. 41.
    Z3 (released, September 2007),
  42. 42.
    Zave, P.: Feature interactions and formal specifications in telecommunications. Computer 26(8), 20–29 (1993)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Margus Veanes
    • 1
  • Wolfram Schulte
    • 1
  1. 1.Microsoft ResearchRedmondUSA

Personalised recommendations