Skip to main content
SpringerLink
Log in

Verification techniques for LOTOS

  • Conference paper
  • First Online:
FME '94: Industrial Benefit of Formal Methods (FME 1994)

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

Included in the following conference series:

Abstract

We report on the results of a project which applied LOTOS to safety-critical case studies, determined the verification needs of real life applications, and developed tools for ASN.1 to LOTOS translation and equational reasoning.

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. J.C. Bicarregui, Algorithm Refinement with Read and Write Frames, Proceeding of Formal Methods Europe '93 Symposium, Odense, April 1993, LNCS 670, Springer-Verlag.

    Google Scholar 

  2. D.W. Bustard, M.T.Norris, R.A. Orr, and A.C. Winstanley, An Exercise in Formalizing the Description of a Concurrent System, Software practice and experience, 22 (1992).

    Google Scholar 

  3. P. Curran and K.J. Norrie, An approach to verifying concurrent systems — a medical information bus (MIB) case study, in Proceedings of the 5th annual IEEE symposium on computer-based medical systems, Durham, North Carolina, 74–83, 1992.

    Google Scholar 

  4. A. J. J. Dick and J. R. Kalmus, ERIL Users manual, Rutherford Appleton Laboratory 1988, RAL-88-055

    Google Scholar 

  5. A. J. J. Dick and P. Watson, Order-Sorted Term Rewriting, Computer Journal, 34 (1991) 16–19

    Google Scholar 

  6. D.A. Duce and F. Paterno, A Formal Specification of a Graphics System in the Framework of the Computer Graphics Reference Model, Computer Graphics Forum, 12 (1993) 123–130.

    Google Scholar 

  7. D.A. Duce and L. Damnjanovic, Formal Specification in the Revision of GKS: An Illustrative Example, Computer Graphics Forum, 11 (1992) 17–30

    Google Scholar 

  8. C. Kirkwood, Automating (Specification = Implementation) using Equational Reasoning and LOTOS, in TAPSOFT'93: Theory and Practice of Software Development, Springer Lecture Notes in Computer Science 668, (1993) 544–558

    Google Scholar 

  9. C. Kirkwood, Verification of LOTOS Specifications Using Term Rewriting Techniques, Ph.D. thesis, University of Glasgow, 1994.

    Google Scholar 

  10. U. Martin, A geometrical approach to multiset orderings, Theoretical computer Science 67 (1989) 37–54

    Google Scholar 

  11. U. Martin, Linear interpretations by counting patterns, in Springer Lecture Notes in Computer Science 690, 5th International Conference on Rewriting Techniques and Applications, Montreal, 1993

    Google Scholar 

  12. U. H. Martin and T. Nipkow, Ordered Rewriting and Confluence in Proceedings of the 10th International conference on Computer Aided Deduction, Lecture Notes in Computer Science 607, 1990.

    Google Scholar 

  13. U. H. Martin and M. K. F. Lai, Some experiments with a completion theorem prover, Journal of Symbolic Computation (1992) 13, 81–100

    Google Scholar 

  14. Ursula Martin and Elizabeth Scott, The order types of termination orderings on terms, strings and multisets, in Proceedings of the Eighth IEEE Conference on Logic in Computer Science, Montreal, 1993

    Google Scholar 

  15. U.H. Martin and J. Wing (editors), Proceedings of the First International Workshop on Larch, Workshops in Computer Science Series, Springer Verlag, 1993.

    Google Scholar 

  16. B.M. Matthews, MERILL: An Equational Reasoning System in Standard ML: A User Guide RAL technical report, RAL-93-026, April 1993.

    Google Scholar 

  17. B.M. Matthews, MERILL: An Equational Reasoning System in Standard ML, in Springer Lecture Notes in Computer Science 690, 5th International Conference on Rewriting Techniques and Applications, Montreal, June 1993

    Google Scholar 

  18. E.A.Scott, An automated proof of the correctness of compiling specification, in M. Nivat, T. Rus, G. Scollo editors, Proceedings of AMAST: Algebraic Methodology and Software Technology, Workshops in Computing, Springer Verlag, 1993.

    Google Scholar 

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

    Google Scholar 

  20. M. Thomas, A Proof of Incorrectness using the LP Theorem Prover: The Editing Problem in the Therac-25. High Integrity Systems Journal, 1 (1994) 35–48

    Google Scholar 

  21. M. Thomas, A Translator Tool for ASN.1 into LOTOS, in M. Diaz, Ro. Groz, editors, Formal Description Techniques, V. pp. 37–52, Elsevier Science Publishers B.V. (North-Holland), 1993.

    Google Scholar 

  22. M. Thomas, A Note on An Exercise in the Formalization of a Concurrent System, manuscript, 1993.

    Google Scholar 

  23. M. Thomas and P. Watson, Solving Divergence in Knuth-Bendix Completion by Enriching Signatures. Theoretical Computer Science, 112, (1993) 145–185

    Google Scholar 

  24. M. Thomas and P. Watson, Solving Divergence in Knuth-Bendix Completion by Enriching Signatures. Extended abstract, in M. Nivat, T. Rus, G. Scollo editors, Proceedings of AMAST: Algebraic Methodology and Software Technology, Workshops in Computing, Springer Verlag, 1993.

    Google Scholar 

  25. D. Craigen, S. Gerhart and T. Ralston, An International Survey of Industrial Formal Methods. Report NISTGCR 93/626 from US Department of Commerce, National Institute for Standards and Technology, March 1993.

    Google Scholar 

  26. ISO [ISO:8807] Information Processing Systems: Open Systems Interconnection: LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour, 1988.

    Google Scholar 

  27. D. Kapur and H. Zhang, RRL: Rewrite Rule Laboratory User's Manual, 1987.

    Google Scholar 

  28. H. Lin, PAM: A Process Algebra Manipulator, University of Sussex, Computer Science Technical Report, 2/91.

    Google Scholar 

  29. J. Quemada, S. Pavón, A. Fernandez, Transforming LOTOS specifications with LOLA — The Parameterised Expansion, in Formal Description Techniques I, K. Turner (ed.), North-Holland, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of St. Andrews, Scotland, UK

    U. Martin

  2. University of Glasgow, Scotland, UK

    M. Thomas

Authors
  1. U. Martin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. M. Thomas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Maurice Naftalin Tim Denvir Miquel Bertran

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Martin, U., Thomas, M. (1994). Verification techniques for LOTOS. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_89

Download citation

  • DOI: https://doi.org/10.1007/3-540-58555-9_89

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58555-8

  • Online ISBN: 978-3-540-49031-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation