Advertisement

Composition of LOTOS specifications

  • M. W. A. Steen
  • H. Bowman
  • J. Derrick
Chapter
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)

Abstract

Usually formal methods adopt the traditional waterfall model of system design. New design methodologies, such as Open Distributed Processing and Object Oriented Design, allow for incremental and partial specification. In order to support such design methods, the issues of consistency between specifications and composition of (partial) specification become vital. This paper presents a general framework for dealing with partial specification, which is instantiated for the specification language LOTOS. Necessary and sufficient conditions for consistency to hold between LOTOS specifications are given, and an operational semantics for composition is proposed.

Keywords

LOTOS formal methods consistency composition incremental specification refinement. 

References

  1. [BB88]
    T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, 14 (1): 25–29, 1988.CrossRefGoogle Scholar
  2. [BBDS95]
    E. A. Boiten, H. Bowman, J Derrick, and M. W. A. Steen. Cross viewpoint consistency in open distributed processing (intra language consistency). Technical Report 8–95, Computing Laboratory, University of Kent, Canterbury, Kent, UK, 1995.Google Scholar
  3. [BDS95]
    H. Bowman, J. Derrick, and M. Steen. Some results on cross viewpoint consistency checking. In Open Distributed Processing III. Chapman 8z Hall, 1995.Google Scholar
  4. [Bo192]
    T. Bolognesi, editor. Catalogue of LOTOS Correctness Preserving Transformations. Lotosphere (ESPRIT #2304), 1992. Final deliverable.Google Scholar
  5. [Bri88]
    H. Brinksma. On the design of Extended LOTOS. PhD thesis, University of Twente, Enschede, Netherlands, 1988.Google Scholar
  6. [BSS87]
    E. Brinksma, G. Scollo, and C. Steenbergen. LOTOS specifications, their implementations and their tests. In G. von Bochmann and B. Sarikaya, editors, Protocol Specification, Testing and Verification VI, pages 349–360. North-Holland, 1987.Google Scholar
  7. [DBS95]
    J. Derrick, H. Bowman, and M. Steen. Maintaining cross viewpoint consistency using Z. In Open Distributed Processing III. Chapman & Hall, 1995.Google Scholar
  8. [Gro90]
    J. F. Groote. Transition system specifications with negative premises. In J. C. M. Baeten and J. W. Klop, editors, CONCUR 90, pages 332–341. Springer-Verlag, 1990.Google Scholar
  9. [IS089a]
    ISO. LOTOS - A formal description technique based on the temporal ordering of observational behaviour, 1989. IS 8807.Google Scholar
  10. [IS089b]
    ISO. Open Systems Interconnection, Basic Reference Model, 1989. IS 7498.Google Scholar
  11. [ITU95]
    ITU Recommendation X.901–904 ISO/IEC 10746 1–4. Open Distributed Processing - Reference Model-Parts 1–4, July 1995.Google Scholar
  12. [IYK90]
    H. Ichikawa, K. Yamanaka, and J. Kato. Incremental Specification in LOTOS. In L. Logrippo, R. L. Probert, and H. Ural, editors, Protocol Specification, Testing and Verification X, pages 183–196, Ottawa, Canada, 1990.Google Scholar
  13. [KvB93]
    F. Khendek and G. von Bochmann. Merging specification behaviours. Technical Report 856, Département d’IRO, Université de Montréal, 1993.Google Scholar
  14. [KvBG92]
    F. Khendek, G. v. Bochmann, and R. Gotzhein. Multiple inheritance in the form of reduction. Technical report, Département d’IRO, Université de Montréal, 1992.Google Scholar
  15. [Led91]
    G. Leduc. On the Role of Implementation Relations in the Design of Distributed Systems using LOTOS. PhD thesis, University of Liège, Liège, Belgium, June 1991.Google Scholar
  16. [Lin92]
    P. F. Linington. Introduction to the Open Distributed Processing Basic Reference Model. In J. de Meer. V. Heymer, and R. Roth, editors, IFIP Transactions C’, Special Issue on Open Distributed Processing, pages 3–13, 1992.Google Scholar
  17. [LOT92]
    The Lotosphere Design Methodology: Guidelines. Number Lo/WP1/T1.1/N0044. Lotosphere Consortium (ESPRIT #2304), March 1992. Final deliverable.Google Scholar
  18. [VSvSB91]
    C. A. Vissers, G. Scollo, M. van Sinderen, and E. Brinksma. On the use of specification styles in the design of distributed systems. Theoretical Computer Science, 89 (1): 179–206, October 1991.CrossRefzbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • M. W. A. Steen
    • 1
  • H. Bowman
    • 1
  • J. Derrick
    • 1
  1. 1.Computing LaboratoryUniversity of KentCanterburyUK

Personalised recommendations