Abstract
We propose a methodology based on testing as a framework to capture the interactions of a machine represented in a denotational model and the data it manipulates. Using a connection that models machines on the one hand, and the data they manipulate on the other, testing is used to capture the interactions of each with the objects on the other side: just as the data that are input into a machine can be viewed as tests that the machine can be subjected to, the machine can be viewed as a test that can be used to distinguish data. This approach is based on generalizing from duality theories that now are common in semantics to logical connections, which are simply contravariant adjunctions. In the process, it accomplishes much more than simply moving from one side of a duality to the other; it faithfully represents the interactions that embody what is happening as the computation proceeds.
Our basic philosophy is that tests can be used as a basis for modeling interactions, as well as processes and the data on which they operate. In more abstract terms, tests can be viewed as formulas of process logics, and testing semantics connects processes and process logics, and assigns computational meanings to both.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Moore, E.F.: Gedanken experiments on sequential machines. In: Automata Studies, Princeton, pp. 129–153 (1956)
Holzmann, G.J.: Design and Validation of Computer Protocols. Software Series. Prentice Hall, London (1991)
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - A survey. Proceedings of the IEEE 84, 1090–1126 (1996)
Mislove, M., Ouaknine, J., Pavlovic, D., Worrell, J.: Duality for labelled Markov processes. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 393–407. Springer, Heidelberg (2004)
Pavlovic, D., Smith, D.R.: Composition and refinement of behavioral specifications. In: Automated Software Engineering 2001. The Sixteenth International Conference on Automated Software Engineering, IEEE, Los Alamitos (2001)
Pavlovic, D., Smith, D.R.: Guarded transitions in evolving specifications. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 411–425. Springer, Heidelberg (2002)
Pavlovic, D., Pepper, P., Smith, D.R.: Colimits for concurrent collectors. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 568–597. Springer, Heidelberg (2004)
Jacobs, B.: Trace semantics for coalgebras. In: Coalgebraic Methods in Computer Science (CMCS) 2004. Electr. Notes in Theor. Comp. Sci., vol. 106 (2004)
Hasuo, I., Jacobs, B.: Context-free languages via coalgebraic trace semantics. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 213–231. Springer, Heidelberg (2005)
Johnstone, P.: Stone Spaces. Cambridge Studies in Advanced Mathematics, vol. 3. Cambridge University Press, Cambridge (1982)
Abramsky, S.: Domain theory in logical form. Annals of Pure and Applied Logic 51, 1–77 (1991)
Milner, R.: Communication and concurrency. International Series in Computer Science. Prentice Hall, London (1989)
Rutten, J.: Behavioral differential equations: a coinductive calculus of streams, automata and power series. Theor. Comp. Sci. 308, 1–53 (2003)
Glabbeek, R., Smolka, S.A., Steffen, B.: Reactive, generative, and stratified models of probabilistic processes. Inf. Comput. 121(1), 59–80 (1995)
DeNicola, R., Hennessy, M.: Testing equivalences for processes. Theoretical Computer Science 34, 83–133 (1984)
Abramsky, S.: A domain equation for bisimulation. Information and Computation 92, 161–218 (1991)
Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comp. Sci. 249, 3–80 (2000)
Plotkin, G.D., Turi, D.: Towards a mathematical operational semantics. In: Proceedings of LICS, vol. 308, pp. 280–291 (1997)
Kupke, C., Kurz, A., Pattinson, D.: Ultrafilter extensions for coalgebras. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 263–277. Springer, Heidelberg (2005)
Bonsangue, M., Kurz, A.: Duality for logics of transition systems. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 455–469. Springer, Heidelberg (2005)
Varacca, D.: The powerdomain of indexed valuations. In: Proceedings 17th IEEE Symposium on Logic in Computer Science, IEEE Press, Los Alamitos (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pavlovic, D., Mislove, M., Worrell, J.B. (2006). Testing Semantics: Connecting Processes and Process Logics. In: Johnson, M., Vene, V. (eds) Algebraic Methodology and Software Technology. AMAST 2006. Lecture Notes in Computer Science, vol 4019. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11784180_24
Download citation
DOI: https://doi.org/10.1007/11784180_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35633-2
Online ISBN: 978-3-540-35636-3
eBook Packages: Computer ScienceComputer Science (R0)