Validating Behavioral Component Interfaces in Rewriting Logic

• Autorzy: Johnsen E.B. , Owe O. , Torjusen A.B.
• Języki publikacji: EN

Abstrakty

EN

Many distributed applications can be understood in terms of components interacting in an open environment such as the Internet. Open environments are subject to change in unpredictable ways, as applications may arrive, evolve, or disappear. In order to validate components in such environments, it can be useful to build simulation environments which reflect this highly unpredictable behavior. This paper considers the validation of components with respect to behavioral interfaces. Behavioral interfaces specify semantic requirements on the observable behavior of components, expressed in an assume-guarantee style. In our approach, a rewriting logic model is transparently extended with the history of all observable communications, and metalevel strategies are used to guide the simulation of environment behavior. Over-specification of the environment is avoided by allowing arbitrary environment behavior within the bounds of the assumption on observable behavior, while the component is validated with respect to the guarantee of the behavioral interface.

Słowa kluczowe

EN

validation; components; behavioral interfaces; adaptive testing; rewriting logic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 82, nr 4
• Strony: 341--359
• Opis fizyczny: bibliogr. 35 poz.

Twórcy

autor

Johnsen E.B.

autor

Owe O.

autor

Torjusen A.B.

• Department of Informatics, University of Oslo, P.O. Box 1139 Blindern, N-0316 Oslo, Norway,

Bibliografia

• [1] Ábrahám, E., Bonsangue, M. M., de Boer, F. S., Steffen, M.: Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes, in: Proceedings of the 1st International Colloquium on Theoretical Aspects of Computing (ICTAC 2004) (Z. Liu, K. Araki, Eds.), vol. 3407 of Lecture Notes in Computer Science, Springer-Verlag, 2005, 37-51.
• [2] Aichernig, B. K., Delgado, C. C.: FromFaults Via Test Purposes to Test Cases: On the Fault-Based Testing of Concurrent Systems., in: 9th International Conference on Fundamental Approaches to Software Engineering (FASE 2006) (L. Baresi, R. Heckel, Eds.), vol. 3922 of Lecture Notes in Computer Science, 2006, 324-338.
• [3] Alpern, B., Schneider, F. B.: Defining Liveness, Information Processing Letters, 21(4), October 1985, 181-185.
• [4] Barbey, S., Buchs, D., Péraire, C.: A Theory of Specification-Based Testing for Object-Oriented Software, in: Proceedings of the European Dependable Computing Conference (EDCC2), vol. 1150 of Lecture Notes in Computer Science, Springer-Verlag, 1996, 303-320.
• [5] Cai, K.-Y., Chen, T. Y., Li, Y.-C., Ning, W.-Y., Yu, Y. T.: Adaptive Testing of Software Components, Proceedings of the Symposium on Applied Computing (SAC 2005) (H. Haddad, L. M. Liebrock, A. Omicini, R. L. Wainwright, Eds.), ACM Press, 2005.
• [6] Chen, H. Y., Tse, T. H., Chan, F. T., Chen, T. Y.: In Black andWhite: An Integrated Approach to Class-Level Testing of Object-Oriented Programs, ACM Transactions on Software Engineering and Methodology, 7(3), 1998, 250-295.
• [7] Clavel, M.: Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications, CSLI Publications, Stanford, California, 2000.
• [8] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J. F.: Maude: Specification and Programming in Rewriting Logic, Theoretical Computer Science, 285, August 2002, 187-243.
• [9] Clavel, M., Meseguer, J.: Reflection in Conditional Rewriting Logic, Theoretical Computer Science, 285, August 2002, 245-288.
• [10] Dahl, O.-J.: Can Program Proving Be Made Practical?, in: Les Fondements de la Programmation (M. Amirchahy, D. Néel, Eds.), Institut de Recherche d'Informatique et d'Automatique, Toulouse, France, December 1977, 57-114.
• [11] Doong, R.-K., Frankl, P. G.: The ASTOOT Approach to Testing Object-Oriented Programs, ACM Transactions on Software Engineering and Methodology, 3(2), 1994, 101-130.
• [12] Durán, F., Roldán, M., Vallecillo, A.: Invariant-Driven Strategies for Maude, Electronic Notes in Theoretical Computer Science, 124(2), 2005, 17-28, Proceedings of the 4th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2004).
• [13] Gaudel, M.-C., James, P. R.: Testing Algebraic Data Types and Processes: A Unifying Theory, Formal Aspects of Computing, 10(5-6), 1998, 436-451.
• [14] Goguen, J. A., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ, in: Software Engineering with OBJ: Algebraic Specification in Action (J. A. Goguen, G. Malcolm, Eds.), Advances in Formal Methods, chapter 1, Kluwer Academic Publishers, 2000, 3-167.
• [15] Hoare, C. A. R.: Communicating Sequential Processes, International Series in Computer Science, Prentice Hall, Englewood Cliffs, NJ., 1985.
• [16] International Telecommunication Union: Open Distributed Processing - Reference Model parts 1-4, Technical report, ISO/IEC, Geneva, July 1995.
• [17] Jeffrey, A., Rathke, J.: A Fully Abstract May Testing Semantics for Concurrent Objects, in: Proceedings of the 17th Annual Symposium on Logic in Computer Science (LICS 2002), IEEE Computer Society Press, 2002, 101-112.
• [18] Johnsen, E. B., Owe, O.: A Compositional Formalism for Object Viewpoints, in: Proc. 5th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'02) (B. Jacobs, A. Rensink, Eds.), Klüwer Academic Publishers, March 2002, 45-60.
• [19] Johnsen, E. B., Owe, O.: Object-Oriented Specification and Open Distributed Systems, in: From Object-Orientation to Formal Methods: Essays in Memory of Ole-Johan Dahl (O. Owe, S. Krogdahl, T. Lyche, Eds.), vol. 2635 of Lecture Notes in Computer Science, Springer-Verlag, 2004, 137-164.
• [20] Johnsen, E. B., Owe, O., Axelsen, E. W.: A Run-Time Environment for Concurrent Objects with AsynchronousMethod Calls, Electronic Notes in Theoretical Computer Science, 117(2), January 2005, 375-392, Proceedings of the 5th InternationalWorkshop on Rewriting Logic and its Applications (WRLA'04).
• [21] Johnsen, E. B., Owe, O., Torjusen, A. B.: Validating Behavioral Component Interfaces in Rewriting Logic, Electronic Notes in Theoretical Computer Science, 159, May 2006, 187-204, Proceedings of the IPM InternationalWorkshop on Foundations of Software Engineering (FSEN 2005).
• [22] Johnsen, E. B., Owe, O., Yu, I. C.: Creol: A Type-Safe Object-Oriented Model for Distributed Concurrent Systems, Theoretical Computer Science, 365(1-2), November 2006, 23-66.
• [23] Jones, C. B.: Development Methods for Computer Programmes Including a Notion of Interference, Ph.D. Thesis, Oxford University, UK, June l981.
• [24] Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley, 2002.
• [25] Meseguer, J.: Conditional Rewriting Logic As a Unified Model of Concurrency, Theoretical Computer Science, 96, 1992, 73-155.
• [26] Meseguer, J., Ro¸su, G.: Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools, in: Proceedings of the Second International Joint Conference on Automated Reasoning (IJCAR 2004) (D. A. Basin,M. Rusinowitch, Eds.), vol. 3097 of Lecture Notes in Computer Science, Springer-Verlag, 2004, 1-44.
• [27] Plotkin, G. D.: A Structural Approach to Operational Semantics, Journal of Logic and Algebraic Progamming, 60, 2004, 17-139.
• [28] Pretschner, A., Lötzbeyer, H., Philipps, J.: Model Based Testing in Incremental System Development, Journal of Systems and Software, 70(3), 2004, 315-329.
• [29] de Roever,W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and NoncompositionalMethods, Number 54 in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, UK, November 2001.
• [30] Ro¸su, G., Havelund, K.: Rewriting-Based Techniques for Runtime Verification, Journal of Automated Software Engineering, 12(2), 2005, 151-197.
• [31] Rusu, V., Marchand, H., Tschaen, V., Jéron, T., Jeannet, B.: From Safety Verification to Safety Testing, in: 16th IFIP International Conference on Testing of Communicating Systems (TestCom 2004) (R. Groz, R. M. Hierons, Eds.), vol. 2978 of Lecture Notes in Computer Science, Springer-Verlag, 2004, 160-176.
• [32] Tyler, B., Soundarajan, N.: Black-Box Testing of Grey-Box Behavior, in: 3rd Intl. Workshop on Formal Approaches to Testing of Software (FATES 2003) (A. Petrenko, A. Ulrich, Eds.), vol. 2931 of Lecture Notes in Computer Science, Springer-Verlag, 2004, 1-14.
• [33] Van Aertryck, L., Benveniste, M., Le Metayer, D.: CASTING : A Formally Based Software Test Generation Method, Proceedings of the 1st IEEE International Conference on Formal Engineering Methods (ICFEM'97), IEEE Computer Society Press, November 1997.
• [34] Venkatasubramanian, N., Talcott, C. L.: Reasoning About Meta Level Activities in Open Distributed Systems, Proceedings of the 14th Annual ACM Symposium on Principles of Distributed Computing (PODC'95), ACM Press, August 1995.
• [35] Walter, T., Schieferdecker, I., Grabowski, J.: Test Architectures for Distributed Systems - State of the Art and Beyond, in: Proceedings of the IFIP TC6 11th International Workshop on Testing Communicating Systems (IWTCS'98) (A. Petrenko, N. Yevtushenko, Eds.), vol. 131 of IFIP Conference Proceedings, Kluwer Academic Publishers, June 1998, 149-174.