Skip to main content
SpringerLink
Log in
Book cover

Specification, Algebra, and Software pp 541–559Cite as

Some Engineering Applications of the OTS/CafeOBJ Method

  • Chapter

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8373))

Abstract

In this paper we present briefly some of the engineering applications of the OTS/CafeOBJ method, conducted by researchers of the National Technical University of Athens in recent years. Such domains of applications include reactive rule-based systems, context-aware adaptive systems and the design by contract paradigm. Other case studies conducted include modeling and verification of Social Networks, Semantic Web and Mobile Digital Rights Management Systems.Finally, we present a summary of the lessons learned from these applications.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Autexier, S., Mossakowski, T.: Integrating HOL-CASL into the Development Graph Manager MAYA. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 2–17. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Barlas, K., Koletsos, G., Ouranos, I., Stefaneas, P.: From ASN.1 into CafeOBJ: Some first steps. In: Fourth SEE Workshop on Formal Methods, pp. 66–72. IEEE Computer Society CPS (2009)

    Google Scholar 

  3. Barlas, K., Koletsos, G., Stefaneas, P., Ouranos, I.: Towards a correct Translation from ASN.1 into CafeOBJ. Special Issue on Innovations in Intelligent Systems and Applications of the International Journal of Reasoning-based Intelligent Systems (IJRIS) 2(3-4), 300–309 (2010)

    Google Scholar 

  4. Barlas, K., Koletsos, G., Stefaneas, P.: Extending Standards with Formal Methods: Open Document Architecture. In: Proc. Innovations in Intelligent Systems and Applications (INISTA), 2012 International Symposium on Innovations in Intelligent Systems and Applications (INISTA), pp. 1–5 (2012)

    Google Scholar 

  5. Barth, A., Mitchell, J.C.: Managing digital rights using linear logic. In: 21st Annual IEEE Symposium on Logic in Computer Science, pp. 127–136. IEEE press, Seattle (2006)

    Chapter  Google Scholar 

  6. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS, vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  7. Dey, A.K., Abowd, G.D.: Towards a Better Understanding of Context and Context-Awareness. In: The First International Symposium on Handheld and Ubiquitous Computing (HUC), Karlsruhe, Germany (1999)

    Google Scholar 

  8. Diaconescu, R.: Behavioural specification for hierarchical object composition. Theoretical Computer Science 343(3), 305–331 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  9. Diaconescu, R., Futatsugi, K., Iida, S.: CafeOBJ Jewels. In: Futatsugi, K., Nakagawa, A.T., Tamai, T. (eds.) CAFE: An Industiral-Strength Algebraic Formal Method, pp. 33–60. Elsevier (2000)

    Google Scholar 

  10. Digital Rights Management 2.1. Technical Report, Open Mobile Alliance (2008)

    Google Scholar 

  11. Doungsaard, C., Suwannasart, T.: A Semantic Part Generated Java Statement from a CafeOBJ Specification. In: IEEE International Conference on Electro/Information Technology (2006)

    Google Scholar 

  12. Doungsaard, C., Suwannasart, T.: An Automatic Approach to Transform CafeOBJ Specifications to Java Template Code. In: International Conference on Software Engineering Research and Practice, SERP 2003, Las Vegas, Nevada, USA, June 23-26, vol. 1 (2003)

    Google Scholar 

  13. DRM Rights Expression Language 2.1. Technical Report, Open Mobile Alliance (2010)

    Google Scholar 

  14. Dulaj, I.: Specification of Security policies by JML (2010), http://www.divaport-al.org/smash/get/diva2:353056/FULLTEXT01.pdf

  15. Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, AMAST Series (1998)

    Google Scholar 

  16. Futatsugi, K., Goguen, J.A., Ogata, K.: Verifying Design with Proof Scores. In: Meyer, B., Woodcock, J. (eds.) Verified Software. LNCS, vol. 4171, pp. 277–290. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. http://www.proofcentral.org/athena/

  18. http://www.informatik.uni-bremen.de/cofi/wiki/index.php/CASL

  19. http://maude.cs.uiuc.edu/

  20. Iftikhar, M.U., Weyns, D.: A Case Study on Formal Verification of Self-Adaptive Behaviors in a Decentralized System. In: 11th International Workshop on Foundations of Coordination Languages and Self-Adaptation (FOCLASA), Newcastle, UK (2012)

    Google Scholar 

  21. Ksystra, K., Stefaneas, P., Frangos, P.: An Algebraic Framework for Modeling of Reactive rule-based Intelligent Agents. In: Geffert, V., Preneel, B., Rovan, B., Štuller, J., Tjoa, A.M. (eds.) SOFSEM 2014. LNCS, vol. 8327, pp. 407–418. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  22. Ksystra, K., Triantafyllou, N., Barlas, K., Stefaneas, P.S.: An Algebraic Specification of Social Networks. In: BCS Quality SG SQM/INSPIRE Conference, Tampere, Finland (2012)

    Google Scholar 

  23. Ksystra, K., Stefaneas, P.S., Frangos, P.: A behavioral framework for context aware adaptive systems (submitted for publication 2014)

    Google Scholar 

  24. Ksystra, K., Triantafyllou, N., Stefaneas, P.: On the Algebraic Semantics of Reactive Rules. In: Bikakis, A., Giurca, A. (eds.) RuleML 2012. LNCS, vol. 7438, pp. 136–150. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  25. Ksystra, K., Stefaneas, P., Ouranos, P., Frangos, P.: A Parallel Version of the MPEG-2 Encoding Algorithm Formally Analyzed using Algebraic Specifications. In: International Conference on Signal Processing and Multimedia Applications (SIGMAP), pp. 35–38 (2010)

    Google Scholar 

  26. Ksystra, K., Stefaneas, P., Triantafyllou, N., Ouranos, I.: An Algebraic Specification for the MPEG-2 Encoding Algorithm. In: Fourth South-East European Workshop on Formal Methods (SEEFM), pp. 46–52 (2009)

    Google Scholar 

  27. Ksystra, K., Triantafyllou, N., Stefaneas, P.S., Frangos, P.: Semantic Web and Algebraic Reasoning: Some First Applications Using Behavioral Specifications. In: Seventh International Workshop on Semantic and Social Media Adaptation and Personalization, Luxembourg, pp. 81–86 (2012)

    Google Scholar 

  28. Liua, J., Zhangb, J., Hub, J.: A case study of an inter-enterprise workflow-supported supply chain management system. Information and Management 42, 441–454 (2005)

    Article  Google Scholar 

  29. Ogata, K., Futatsugi, K.: Some Tips on Writing Proof Scores in the OTS/CafeOBJ method. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Goguen Festschrift. LNCS, vol. 4060, pp. 596–615. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  30. Ouranos, I., Stefaneas, P., Frangos, P.: An Algebraic Framework for Modeling of Mobile Systems. IEICE Trans. Fund. E90-A(9), 1986–1999 (2007)

    Article  Google Scholar 

  31. Ouranos, I., Stefaneas, P., Frangos, P.: An Algebraic Specification of Mobile IPv6 Protocol. In: 1st Conf. Principles of Software Engineering (PRISE), Buenos Aires, Argentina (2004)

    Google Scholar 

  32. Ouranos, I., Stefaneas, P., Frangos, P.: A Formal Specification Framework for Ad Hoc Mobile Communication Networks. In: SOFSEM 2007, pp. 91–102 (2007)

    Google Scholar 

  33. Ouranos, I., Ogata, K., Stefaneas, P.: Formal Analysis of TESLA protocol in the Timed OTS/CafeOBJ method. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 126–142. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  34. Ouranos, I., Stefaneas, P., Ogata, K.: Formal Modeling and Verification of Sensor Network Encryption Protocol in the OTS/CafeOBJ Method. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part I. LNCS, vol. 6415, pp. 75–89. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  35. Ouranos, I., Stefaneas, P.: Verifying Security Protocols for Sensor Networks using Algebraic Specification Techniques. In: Bozapalidis, S., Rahonis, G. (eds.) CAI 2007. LNCS, vol. 4728, pp. 247–259. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  36. Ouranos, I., Stefaneas, P.: Towards a Protocol Algebra Based on Algebraic Specifications. In: Lee, R. (ed.) SERA 2013. SCI, vol. 496, pp. 85–98. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  37. Ouranos, I., Ogata, K., Stefaneas, P.: TESLA source authentication protocol verification experiment in the Timed OTS/CafeOBJ method: Experiences and Lessons Learned (2013) (submitted for publication)

    Google Scholar 

  38. Pavlova, M., Barthe, G., Burdy, L., Huisman, M., Lanet, J.L.: Enforcing High-Level Security Properties for Applets. In: Sixth Smart Card Research and Advanced Application IFIP Conference, pp. 1–16 (2003)

    Google Scholar 

  39. Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  40. Iida, S., Matsumoto, M., Diaconescu, R., Futatsugi, K., Lucanu, D.: Concurrent Object Composition in CafeOBJ. Technical Report IS-RR-98-0009S, Japan Advanced Institute of Science and Technology, JAIST (1998)

    Google Scholar 

  41. Triantafyllou, N., Ouranos, I., Stefaneas, P.: Algebraic Specifications for OMA REL Licenses. In: IEEE International Conference on Wireless and Mobile Computing, Networking and Communications, pp. 376–381. IEEE Press, Marrakech (2009)

    Google Scholar 

  42. Triantafyllou, N., Stefaneas, P., Frangos, P.: An Algorithm for Allocating User Requests to Licenses in the OMA DRM System. IEICE Transactions on Information and Systems E96-D(6), 1258–1267 (2013)

    Article  Google Scholar 

  43. Triantafyllou, N., Ksystra, K., Stefaneas, P., Frangos, P.: Applying Algebraic Specifications on Digital Right Management Systems. In: Imperial College Computing Student Workshop, ICCSW 2011, pp. 94–100 (2011)

    Google Scholar 

  44. Triantafyllou, N., Ksystra, K., Stefaneas, P., Frangos, P.: Proof Carrying Code using Algebraic Specifications. Journal of Applied Mathematics & Bioinformatics 3(1), 43–56 (2013)

    MATH  Google Scholar 

  45. Triantafyllou, N., Stefaneas, P., Frangos, P.: OTS/CafeOBJ2JML: An attempt to combine Design By Contract with Behavioral Specifications. Technical report (2012)

    Google Scholar 

  46. Triantafyllou, N., Ouranos, I., Stefaneas, P., Frangos, P.: Formal Specification and Verification of the OMA License Choice Algorithm in the OTS/CafeOBJ Method. In: ICETE the International Joint Conference on e-Business and Telecommunications (WINSYS), pp. 173–180. SciTe Press, Athens (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. National Technical University of Athens, Greece

    Petros Stefaneas, Iakovos Ouranos, Nikolaos Triantafyllou & Katerina Ksystra

Authors
  1. Petros Stefaneas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Iakovos Ouranos
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nikolaos Triantafyllou
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Katerina Ksystra
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Network and Information, Senshu University, 2-1-1 Higashi-mita, Tama-ku, 214-8580, Kawasaki, Kanagawa, Japan

    Shusaku Iida

  2. Department of Computer Science, Thomas M. Siebel Center for Computer Science, University of Illinois at Urbana-Champaign (UIUC), 201 N. Goodwin Avenue, MC 258, 61801, Urbana, IL, USA

    José Meseguer

  3. School of Information Science, Advanced Institute of Science and Technology (JAIST), 1-1 Asahidai, 923-1292, Nomi, Ishikawa, Japan

    Kazuhiro Ogata

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Stefaneas, P., Ouranos, I., Triantafyllou, N., Ksystra, K. (2014). Some Engineering Applications of the OTS/CafeOBJ Method. In: Iida, S., Meseguer, J., Ogata, K. (eds) Specification, Algebra, and Software. Lecture Notes in Computer Science, vol 8373. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54624-2_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-54624-2_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-54623-5

  • Online ISBN: 978-3-642-54624-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation