Abstract
Networked services, constituted by the structural and behavior arrangement of service components are considered. A service component is executed as a generic software component, denoted as an actor, which is able to download and execute different EFSM (Extended Finite State Machine) based functionality. The functionality of an actor is denoted as its role, while a role session is a projection of the role with respect to the interaction with one other actor. We propose an approach for verification of the services, based on interface verification techniques for the verification of the role sessions. The service component specifications used for actor execution are based on XML representations, while the verification of the role sessions is based on a behavior type language. This language has a sound theoretical basis, and is used to avoid ”message-not-understood” errors. Rules are given for automatic translation from the XML manuscripts to this behavioral type language. This translation first makes projection to the role session, using hidden actions. Those hidden actions are then removed so a sound verification can take place.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Aagesen, F.A., Helvik, B.E., Anutariya, C., Shiaa, M.M.: On adaptable networking. In: ICT 2003, Proceedings, Assumption University, Thailand (2003)
Carrez, C.: Contrats Comportementaux pour Composants. PhD thesis, ENST, Paris, France (December 2003)
Carrez, C., Fantechi, A., Najm, E.: Behavioural contracts for a sound composition of components. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767. Springer, Heidelberg (2003)
Carrez, C., Fantechi, A., Najm, E.: Assembling components with behavioural contracts. Annals of Telecomms (2005), To appear. Ext. of [CFN03]
de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/FSE 2001. Software Engineering Notes, vol. 26(5). ACM Press, New York (2001)
Floch, J.: Towards Plug-and-Play Services: Design and Validation using Roles. PhD thesis, NTNU, Trondheim, Norway (February 2003)
Gay, S., Vasconcelos, V.T., Ravara, A.: Session types for inter-process communication. Preprint, Dept. of Computer Science, Univ. of Lisbon (2002)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1990)
Jiang, S., Aagesen, F.A.: XML-based dynamic service behaviour representation. In: NIK 2003, Proceedings, Oslo, Norway (November 2003)
Johansen, U., Aagesen, F.A., Helvik., B.E., Bræk, R.: Design specification of the PaP support functionality. Technical Report 1999-12-10, Department of Telematics, NTNU (1999)
Lam, S.S., Shankar, A.U.: Protocol verification via projections. IEEE Transactions on Software Engineering 10(4), 325–342 (1984)
Lee, E.A., Xiong, Y.: A behavioral type system and its application in ptolemy ii. Formal Aspects of Computing 16(3), 210–237 (2004)
Nierstrasz, O.: Regular types for active objects. In: Object-Oriented Software Composition, pp. 99–121. Prentice-Hall, Englewood Cliffs (1995)
Najm, E., Nimour, A., Stefani, J.-B.: Infinite types for distributed objects interfaces. In: FMOODS 1999, Proceedings, Firenze, Italy (February 1999)
Ravara, A., Vasconcelos, V.T.: Typing non-uniform concurrent objects. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 474–488. Springer, Heidelberg (2000)
Sanders, R., Bræk, R.: Discovering service opportunities by evaluating service goals. In: EUNICE 2004, Proceedings, Tampere, Finland (June 2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jiang, S., Carrez, C., Aagesen, F.A. (2005). Automatic Translation of Service Specification to a Behavioral Type Language for Dynamic Service Verification. In: Guelfi, N. (eds) Rapid Integration of Software Engineering Techniques. RISE 2004. Lecture Notes in Computer Science, vol 3475. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11423331_4
Download citation
DOI: https://doi.org/10.1007/11423331_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25812-4
Online ISBN: 978-3-540-32039-5
eBook Packages: Computer ScienceComputer Science (R0)