Abstract
Model programs are a useful formalism for software testing and design analysis. They are used in industrial tools, such as SpecExplorer, as a compact, expressive and precise way to specify complex behavior. One of the challenges with model programs has been the difficulty to separate contract modeling from scenario modeling. It has not been clear how to separate those concerns in a clean way. In this paper we introduce composition of model programs, motivate why it is useful to be able to compose model programs, and what composition of model programs formally means.
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
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer (2003)
Brinksma, E., Tretmans, J.: Testing Transition Systems: An Annotated Bibliography. In: Summer School MOVEP’2k – Modelling and Verification of Parallel Processes. LNCS, vol. 2067, pp. 187–193. Springer, Heidelberg (2001)
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.A., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 542–547. Springer, Heidelberg (2005)
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)
El-Fakih, K., Petrenko, A., Yevtushenko, N.: Fsm test translation through context. In: Uyar, M.Ü., Duale, A.Y., Fecko, M.A. (eds.) TestCom 2006. LNCS, vol. 3964, Springer, Heidelberg (2006)
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.) Formal Approaches to Software Testing and Runtime Verification. LNCS, vol. 4262, pp. 40–54. Springer, Heidelberg (2006)
Grieskamp, W., Kicillof, N., Tillmann, N.: Action machines: a framework for encoding and composing partial behaviors. International Journal on Software and Knowledge Engineering 16(5), 705–726 (2006)
Gurevich, Y.: Evolving Algebras 1993: Lipari Guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford University Press, Oxford (1995)
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 (Submitted to publisher) (2007)
Keller, R.: Formal verification of parallel programs. Communications of the ACM, pp. 371–384 (July 1976)
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines – a survey. Proceedings of the IEEE 84(8), 1090–1123 (1996)
Lynch, N., Tuttle, M.: Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, pp. 137–151. ACM Press, New York (1987)
Tretmans, J., Brinksma, E.: TorX: Automated model based testing. In: 1st European Conference on Model Driven Software Engineering, Nuremberg, Germany, pp. 31–43 (December 2003)
Veanes, M., Campbell, C., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N.: Model-based testing of object-oriented reactive systems with Spec Explorer, 2005, Tech. Rep. MSR-TR-2005-59, Microsoft Research (to appear as a book chapter in Formal Methods and Testing)
Veanes, M., Campbell, C., Schulte, W., Tillmann, N.: Online testing with model programs. In: ESEC/FSE-13. Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, pp. 273–282. ACM, New York (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Veanes, M., Campbell, C., Schulte, W. (2007). Composition of Model Programs. In: Derrick, J., Vain, J. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2007. FORTE 2007. Lecture Notes in Computer Science, vol 4574. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73196-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-73196-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73195-5
Online ISBN: 978-3-540-73196-2
eBook Packages: Computer ScienceComputer Science (R0)