Skip to main content
SpringerLink
Log in

An Adequate Logic for Full LOTOS

  • Conference paper
  • First Online:
FME 2001: Formal Methods for Increasing Software Productivity (FME 2001)

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

Included in the following conference series:

Abstract

We present a novel result for a logic for symbolic transition systems based on LOTOS processes. The logic is adequate with respect to bisimulation defined on symbolic transition systems.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D. Amyot, L. Char et al. Feature Description and Feature Interaction Analysis with Use Case Maps and LOTOS. In M. Calder and E. Magill, editors, Feature Interactions in Telecommunications and Software Systems VI. IOS Press, May 2000.

    Google Scholar 

  2. H. Becht, A. Bloesch et al. Ergo 4.1 Reference Manual. Technical Report 96-31, Software Verification Research Centre, University of Queensland, Australia, November 1996

    Google Scholar 

  3. M. Calder, S. Maharaj, and C. Shankland. A Modal Logic for Early Symbolic Transition Systems. The Computer Journal, 2001. To appear.

    Google Scholar 

  4. M. Calder and C. Shankland. A Symbolic Semantics and Bisimulation for Full LOTOS. To appear as a University of Stirling Technical Report, 2000.

    Google Scholar 

  5. M. Clavel, F. Duran et al. Maude: Specification and Programming in Rewriting Logic. Maude System documentation. Computer Science Laboratory, SRI, Menlo Park, California, March 1999.

    Google Scholar 

  6. J-C. Fernandez, H. Garavel et al. CADP (CAESAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In R. Alur and T.A. Henzinger, editors, Proceedings of CAV’96, number 1102 in Lecture Notes in Computer Science, pages 437–440. Springer-Verlag, 1996.

    Google Scholar 

  7. J.F. Groote and R. Mateescu. Verification of Temporal Properties of Processes in a Setting with Data. In Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology AMAST’98, Amazonia, Brazil, volume 1548 of Lecture Notes in Computer Science, pages 74–90, 1999.

    Google Scholar 

  8. J.F. Groote and A. Ponse. The Syntax and Semantics of µ-CRL. In Proceedings of Algebra of Communicating Processes, Utrecht 1994, Workshops in Computing. Springer-Verlag, 1995.

    Google Scholar 

  9. M. Hennessy and H. Lin. Symbolic Bisimulations. Theoretical Computer Science, 138:353–389, 1995.

    Google Scholar 

  10. M. Hennessy and X. Liu. A Modal Logic for Message Passing Processes. Acta Informatica, 32:375–393, 1995.

    MATH  MathSciNet  Google Scholar 

  11. M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of the Association for Computing Machinery, 32(1):137–161, 1985.

    MATH  MathSciNet  Google Scholar 

  12. International Organisation for Standardisation. Information Processing Systems–Open Systems Interconnection–LOTOS–A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, 1988.

    Google Scholar 

  13. C. Kirkwood. Specifying Properties of Basic LOTOS Processes Using Temporal Logic. In G. v Bochmann, R. Dssouli, and O. Rafiq, editors, Formal Description Techniques, VIII, IFIP. Chapman Hall, April 1996.

    Google Scholar 

  14. D. Kozen. Results on the Propositional µ-Calculus. Theoretical Computer Science, 27:333–354, 1983.

    Google Scholar 

  15. R. Mateescu and H. Garavel. XTL: A Meta-Language and Tool for Temporal Logic Model-Checking. In Proceedings of the International Workshop on Software Tools for Technology Transfer STTT’98 (Aalborg, Denmark), 1998.

    Google Scholar 

  16. C. Pecheur. Using LOTOS for specifying the CHORUS distributed operating system kernel. Computer Communications, 15(2):93–102, March 1992.

    Article  Google Scholar 

  17. M. Sighireanu and R. Mateescu.Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (FireWire): an Experiment with E-LOTOS. Springer International Journal on Software Tools for Technology Transfer (STTT), 2(1):68–88, Dec. 1998.

    MATH  Google Scholar 

  18. C. Stirling. Temporal Logics for CCS. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, pages 660–672. Springer-Verlag, 1989. REX School /Workshop, Noordwijkerhout, The Netherlands, May/June 1988.

    Google Scholar 

  19. M. Thomas. The Story of the Therac-25 in LOTOS. High Integrity Systems Journal, 1(1):3–15, 1994.

    Google Scholar 

  20. M. Thomas. Modelling and Analysing User Views of Telecommunications Services. In Feature Interactions in Telecommunications Systems, pages 168–183. IOS Press, 1997.

    Google Scholar 

  21. M. Thomas and B. Ormsby. On the Design of Side-Stick Controllers in Fly-by-Wire Aircraft. A.C.M. Applied Computing Review, 2(1):15–20, Spring 1994.

    Google Scholar 

  22. Kenneth J. Turner. An architectural description of intelligent network features and their interactions. Computer Networks, 30(15):1389–1419, September 1998.

    Google Scholar 

  23. A. Vogel. On ODP’s architectural semantics using LOTOS. In J. de Meer, B. Mahr, and O. Spaniol, editors, Proc. Int. Conf. on Open Distributed Processing, pages 340–345, September 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Glasgow, Glasgow, G12 8QQ, UK

    Muffy Calder

  2. Department of Computing Science and Mathematics, University of Stirling, Stirling, FK9 4LA, UK

    Savi Maharaj & Carron Shankland

Authors
  1. Muffy Calder
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Savi Maharaj
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Carron Shankland
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of Minho, Campus de Gualtar, 4700-320, Braga, Portugal

    José Nuno Oliveira

  2. AT&T Laboratories — Research, 180 Park Avenue, Florham Park, New Jersey, 07932, USA

    Pamela Zave

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Calder, M., Maharaj, S., Shankland, C. (2001). An Adequate Logic for Full LOTOS. In: Oliveira, J.N., Zave, P. (eds) FME 2001: Formal Methods for Increasing Software Productivity. FME 2001. Lecture Notes in Computer Science, vol 2021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45251-6_21

Download citation

  • DOI: https://doi.org/10.1007/3-540-45251-6_21

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41791-0

  • Online ISBN: 978-3-540-45251-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation