Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Spec Explorer (released, January 2005), http://research.microsoft.com/specexplorer
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)
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)
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)
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)
Blass, A., Gurevich, Y.: Ordinary interactive small-step algorithms, I. ACM Transactions on Computation Logic 7(2), 363–419 (2006)
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
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)
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)
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)
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)
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)
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)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/FSE 2001, pp. 109–120. ACM, New York (2001)
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)
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)
Douence, R., Fradet, P., Südholt, M.: Aspect-Oriented Software Development. In: Trace-based Aspects, pp. 201–218. Addison Wesley, Reading (2004)
Elrad, T., Aksit, M., Kiczales, G., Lieberherr, K., Ossher, H.: Discussing aspects of AOP. Commun. ACM 44(10), 33–38 (2001)
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)
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)
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)
Grieskamp, W., Kicillof, N., Tillmann, N.: Action machines: a framework for encoding and composing partial behaviors. IJSEKE 16(5), 705–726 (2006)
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)
Gurevich, Y.: Specification and Validation Methods. In: Evolving Algebras 1993: Lipari Guide, pp. 9–36. Oxford University Press, Oxford (1995), research.microsoft.com/~gurevich/Opera/103.pdf
Gurevich, Y., Rossman, B., Schulte, W.: Semantic essence of asml. Theor. Comput. Sci. 343(3), 370–412 (2005)
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)
Hertel, C.: Implementing CIFS: The Common Internet File System. Prentice-Hall, Englewood Cliffs (2003)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)
Jacky, J., Veanes, M., Campbell, C., Schulte, W.: Model-based Software Testing and Analysis with C#. Cambridge University Press, Cambridge (2007)
Keller, R.: Formal verification of parallel programs. Communications of the ACM, 371–384 (July 1976)
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)
Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI-Quarterly 2(3), 219–246 (1989)
NModel (released, May 2007), http://www.codeplex.com/NModel
Utting, M., Legeard, B.: Practical Model-Based Testing - A tools approach. Elsevier Science, Amsterdam (2006)
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)
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)
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)
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)
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)
Z3 (released, September 2007), http://research.microsoft.com/projects/z3
Zave, P.: Feature interactions and formal specifications in telecommunications. Computer 26(8), 20–29 (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Veanes, M., Schulte, W. (2008). Protocol Modeling with Model Program Composition. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2008. FORTE 2008. Lecture Notes in Computer Science, vol 5048. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68855-6_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-68855-6_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68854-9
Online ISBN: 978-3-540-68855-6
eBook Packages: Computer ScienceComputer Science (R0)