Abstract
We sketch some first steps towards the definition of a protocol algebra based on the framework of behavioural algebraic specification. Following the tradition of representing protocols as state machines, we use the notion of Observational Transition System to express them in an executable algebraic specification language such as CafeOBJ. This abstract approach allows defining several useful operators for protocol reasoning and proving properties of them using theorem proving techniques and CafeOBJ term rewriting machine. The proposed protocol algebra is inspired by the module algebra and the hierarchical object composition technique.
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
Diaconescu, R.: Behavioural Coherence in Object-Oriented Algebraic Specification. Universal Computer Science 6(1), 74–96 (2000)
Goguen, J.A., Diaconescu, R.: Towards an algebraic semantics for the object paradigm. In: Ehrig, H., Orejas, F. (eds.) ADT 1992 and COMPASS 1992. LNCS, vol. 785, pp. 1–34. Springer, Heidelberg (1994)
Goguen, J., Malcolm, G.: A hidden agenda. Technical Report CS97-538, University of California at San Diego (1997)
Diaconescu, R.: Behavioral Specification for Hierarchical Object Composition. Theoretical Computer Science 343, 305–331 (2005)
Diaconescu, R., Futatsugi, K.: CafeOBJ report. World Scientific (1998)
Bergstra, J.A., Heering, J., Klint, P.: Module Algebra. Journal of ACM 37(2), 335–372 (1990)
Diaconescu, R., Goguen, J.A., Stefaneas, P.: Logical Support for Modularisation. In: Huet, G., Plotkin, G. (eds.) Logical Environment, pp. 83–130 (1993)
Ouranos, I., Stefaneas, P., Frangos, P.: An Algebraic Framework for Modeling of Mobile Systems. IEICE Trans. Fund. E90-A(9), 1986–1999 (2007)
Mallya, A.P., Singh, M.P.: An algebra of commitment protocols. Journal of Autonomous Agents and Multi - Agent Systems 14(2), 143–163 (2007)
Singh, G.: A compositional approach for designing protocols. In: Proceedings of the International Conference on Network Protocols, San Francisco, CA, USA, pp. 98–107 (1993)
Sinha, P., Suri, N.: Modular Composition of Redundancy Management Protocols in Distributed Systems: An Outlook on Simplifying Protocol Level Formal Specification and Verification. In: Proceedings of ICDCS-21, pp. 255–263 (2001)
Garbinato, B., Felber, P., Guerraoui, R.: Modeling Protocols as Objects for Structuring Reliable Distributed Systems. In: Proceedings of the Communication Networks and Distributed Systems Modeling and Simulation Conference (CNDS 1997), Phoenix, Arizona, pp. 165–171 (1997)
Singh, G., Mao, Z.: Structured design of communication protocols. In: Proceedings of the IEEE International Conference on Distributed Computing Systems (1986)
Hagalisletto, A.M.: Protocol Algebra. In: Proceedings of the 11th IEEE Symposium on Computers and Communications (2006)
Mallya, A.U., Singh, M.: An algebra for commitment protocols. Autonomous Agents and Multiagent Systems 4(2), 143–163 (2007)
Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: Proceedings of the 12th ACM Symposium on Principles of Programming Languages, pp. 52–66. ACM (1985)
Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.-P.: Introducing OBJ. Technical report, SRI International, Computer Science Laboratory (1993)
Miranda, H., Pinto, A., Rodrigues, L.: Appia: A flexible protocol kernel supporting multiple coordinated channels. In: Proceedings of the 21st Int. Conf. on Distributed Computing Systems (ICDCS 2001), Washington - Brussels - Tokyo, pp. 707–710 (2001)
Wong, G., Hiltunen, M., Schlichting, R.: CTP: A configurable and extensible transport protocol. In: Proceedings of the 20th Annual Conference of IEEE Communications and Computer Societies (INFOCOM 2001), Anchorage, Alaska (2001)
Wojciechowski, P., Rütti, O., Schiper, A.: SAMOA: Framework for synchronization augmented microprotocol approach. In: Proceedings of Int. Parallel and Distributed Processing Symposium (IPDPS 2004), Santa Fe, US (2004)
Ogata, K., Futatsugi, K.: Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 596–615. Springer, Heidelberg (2006)
Ogata, K., Futatsugi, K.: Proof scores in the oTS/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Ouranos, I., Stefaneas, P. (2014). Towards a Protocol Algebra Based on Algebraic Specifications. In: Lee, R. (eds) Software Engineering Research, Management and Applications. Studies in Computational Intelligence, vol 496. Springer, Heidelberg. https://doi.org/10.1007/978-3-319-00948-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-00948-3_6
Publisher Name: Springer, Heidelberg
Print ISBN: 978-3-319-00947-6
Online ISBN: 978-3-319-00948-3
eBook Packages: EngineeringEngineering (R0)