[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Towards an implementation-oriented specification of TP protocol in LOTOS

  • Industrial Usage Reports
  • Conference paper
  • First Online:
FME '93: Industrial-Strength Formal Methods (FME 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 670))

Included in the following conference series:

  • 132 Accesses

Abstract

This paper presents an exercise in the specification and implementation design of a realistic OSI Application-layer protocol in accordance with the LotoSphere methodology. It also reports some of the experiences acquired during the design process. The main motivation of the work presented is the need to have a genuine assessment of the design methodology for its industrial applicability.

The OSI Transaction Processing protocol is selected as a design example due to its distributed nature and its entangled compositional structure, comprising of OSI common application service elements, i.e. AC-SE and CCR-SE, and TP specific elements. This paper focusses on the design trajectory of the TP specific parts.

The design process starts with an informal protocol description and after several design steps ends with an implementation specified in LOTOS. This process is globally constrained by realizability and open-endedness requirements. The derived implementation is expressed in a state(-machine) oriented way and is in a design sense close to a realization. UNIX workstations with a running ISODE are selected as realization environment. An alternative design approach which suitably fits ISODE is exposed but not elaborated. A second design cycle has been undertaken to enable some evaluation of the open-endedness of the specification.

This work has been supported by the CEC under the ESPRIT II program in project 2304.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. C. A. Vissers, J. v.d. Lagemaat ”Report on LotoSphere” Proc.ESPRIT Technical Week, Brussels, Nov. 1989

    Google Scholar 

  2. J.Navarro and P.San Martin, ”Experience in the Development of an ISDN Layer 3 Service in LOTOS”, in J. Quemada et.al. (eds), Formal Description Techniques III, North Holland, 1991 pages 327–336.

    Google Scholar 

  3. R. E. Booth, V. M. Jones, R. J. Clark, F. Juillot, G-J. van der Heijden, and I. Widya, ”A formal development trajectory for OSI application layer protocols”, Proc. of the 5th International Conference on Putting into Practice Methods and Tools for Information System Design, Nantes, Sept. 1992.

    Google Scholar 

  4. ”LOTOS Industrial Application: Mini-Mail”, E.Wiedmer, LotoSphere Project ES-PRIT II 2304, Final Deliverable, Lo/WP3/T3.2/N0068, 1992

    Google Scholar 

  5. ISO/DIS 10026-3 Information Processing Systems — Open Systems Interconnection — Distributed Transaction Processing — Part 3: Protocol Specification, 1990.

    Google Scholar 

  6. ISO, ”Protocol Specification for the Association Control Service Element”, ISO/IS 8650, 1988.

    Google Scholar 

  7. ISO, ”Protocol Specification for the Commitment, Concurrency and Recovery Service Element” ISO/IS 9805.3.

    Google Scholar 

  8. M. T. Rose, ”The ISO Development Environment: User's Manual”, ISODE 6.0, Performance Systems Int. Inc., Jan. 1990.

    Google Scholar 

  9. A. M. Fletcher, ”An Overview of the OSI Transaction Processing Standard”, Proc. Int. Open Systems '89, Online Publ., 1989, page 153–162.

    Google Scholar 

  10. L. F. Pires and C. A. Vissers, ”Overview of the LotoSphere Design Methodology”, ESPRIT Conf. 1990, Brussels Nov. 12–15, 1990.

    Google Scholar 

  11. ISO, ”LOTOS — a Formal Description Technique Based on the Temporal Ordering of Observational Behaviour”, ISO/IS 8807, 1988.

    Google Scholar 

  12. C. A. Vissers, G.Scollo and M.van Sinderen, ”Architecture and Specification Style in Formal Descriptions of Distributed Systems”, Proc. IFIP WG6.1, PSTV VIII, North Holland, 1989, page 189–204.

    Google Scholar 

  13. ISO, ”Guidelines for the Application Estelle, LOTOS and SDS, ISO-IEC/TR 10167, 1990.

    Google Scholar 

  14. ISO, ”Application Layer Structure”, ISO/IS 9545, 1989.

    Google Scholar 

  15. M. van Sinderen and I. Widya, ”On the Design and Formal Specification of a Transac-tion Processing Protocol”, In J. Quemada et.al. (eds), Formal Description Technique III, North Holland, 1991, pages 411–426.

    Google Scholar 

  16. ”The Lotosphere Design Methodology: Guidelines”, LotoSphere Project ESPRIT II 2304, Lo/WP1/T1.1/N0044/V04, March 1992.

    Google Scholar 

  17. ”LOTOS Specification of the OSI OCR Protocol: Architecture”, Val. Jones and Robert Clark, LotoSphere Project ESPRIT II 2304, Lo/WP3/T3.1/UST/N0003.

    Google Scholar 

  18. H. Eertink and D. Wolz, ”Symbolic Execution of LOTOS Specification”, Proceeding of the 5th International Conference on Formal Description Techniques, ed. M. Diaz and R. Groz, Lannion, France, Oct. 1992, pp. 289–304.

    Google Scholar 

  19. ”Implementation of the OSI Association Control Service Element Using C-ex”, R. Levy, Computer Networks Laboratory, EPF-Lausanne, Switzerland, 1991

    Google Scholar 

  20. ”Detailed Design Document: COLOS”, E. Dubuis and K. Warkentyne, LotoSphere Project ESPRIT II 2304, Lo/WP2/T2.2/ASCOM/N0024, 1992.

    Google Scholar 

  21. ”On the Use of Pre-Defined Implementation Constructs in Distributed Systems Design”, L. F. Pires, M. van Sinderen and C. A. Vissers, Third Workshop on Future Trends of Distributed Computing Systems in the 1990's, Taipei, April 1992

    Google Scholar 

  22. ”TP Protocol Version 3.0: a cycle 2 version”, E. van der Burg, and I. Widya, LotoSphere Project ESPRIT II 2304, Lo/WP3/T3.1/UT/N0020/V2, 1992.

    Google Scholar 

  23. M. Caneve and E. Salvatori (eds), ”Lite User Manual”, ESPRIT II 2304 internal report Lo/WP2/N0034, April, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Twente, P. O. Box 217, 7500, AE Enschede, The Netherlands

    Ing Widya

  2. Océ Nederland B.V., P.O.Box 101, 5900, MA Venlo, The Netherlands

    Gert-Jan van der Heijden

Authors
  1. Ing Widya
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gert-Jan van der Heijden
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

James C. P. Woodcock Peter G. Larsen

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Widya, I., van der Heijden, GJ. (1993). Towards an implementation-oriented specification of TP protocol in LOTOS. In: Woodcock, J.C.P., Larsen, P.G. (eds) FME '93: Industrial-Strength Formal Methods. FME 1993. Lecture Notes in Computer Science, vol 670. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024641

Download citation

  • DOI: https://doi.org/10.1007/BFb0024641

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56662-5

  • Online ISBN: 978-3-540-47623-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation