Skip to main content
SpringerLink
Log in

Applying SDL Specifications and Tools to the Verification of Procedures

  • Conference paper
  • First Online:
SDL 2001: Meeting UML (SDL 2001)

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

Included in the following conference series:

Abstract

Verification of operating procedures (that is, specifications of manual control actions) by model checking has been discussed in [16]. The modelling language Promela and the model checker Spin were used in that report. In order to be able to apply model checking in a wider scope, modelling languages with graphical interface and verification tools usedin industrial context are preferable (for example, to facilitate collaboration with process experts). In this paper, we discuss how to use SDL to model systems consisting of operating procedures and the controlled processes. Verification of procedures against correctness specifications is done by using the tool SDT. We conclude the paper with a short discussion of the integration of formal verification with the procedure design process.

The research describedin this paper was carriedout at the OECD Halden Reactor Project at the Institute for Energy Technology, Norway. The author thanks G. Dahll, T. Sivertsen andK. Stølen for their helpful suggestions andcommen ts. The author also thanks anonymous referees for their constructive criticisms that helpedin improving this paper.

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F. Bakkehøi. Assosiasjon av prosedyrelle aksjoner til XML baserte dokumenter. M.Sc. Thesis (in Norwegian). Institute of Informatics, University of Oslo. 2000.

    Google Scholar 

  2. R. Bræk and A. Sarma (editors). Proceedings of the 7th SDL Forum (SDL’95), North-Holland, 1995.

    Google Scholar 

  3. Anders Ek, Jens Grabowski, Dieter Hogrefe, Richard Jerome, Beat Koch and Michael Schmitt. Towards the Industrial Use of Validation Techniques and Automatic Test Generation Methods for SDL Specifications. Proceedings of the 8th SDL Forum (SDL’97)245–259, North-Holland, 1997.

    Google Scholar 

  4. J. Ellsberger, D. Hogrefe and A. Sarma. SDL-Formal Object-orientedLanguage for Communicating Systems. Prentice Hall Europe, 1997, ISBN 0-13-621384-7.

    Google Scholar 

  5. E. A. Emerson. Temporal and Modal Logic. Handbook of Theoretical Computer Science (B): 997–1072. 1990.

    Google Scholar 

  6. F. Handelsby, E. Ness and J. Teigen. OECD Halden Reactor Project: COPMA II On-Line Functional Specifications. Report: HWR-319, Institute for Energy Technology, Norway. 1992.

    Google Scholar 

  7. D. G. Hoecker, K. M. Corker, E. M. Roth, M. H. Lipner and M. S. Bunzo. Man-Machine Design and Analysis System (MIDAS) Appliedto a Computer-Based Procedure-Aiding System. Proceedings of the Human Factors and Ergonomics Society 38th Annual Meeting 1: 195–199. 1994.

    Google Scholar 

  8. G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, New Jersey, 1991.

    Google Scholar 

  9. G. J. Holzmann. The model checker Spin. IEEE Transactions on Software Engineering 23(5): 279–295. May 1997.

    Article  MathSciNet  Google Scholar 

  10. M. H. Lipner and S. P. Kerch. Operational Benefits of an Advanced Computerised Procedure System. 1994 IEEE Conference Record: Nuclear Science Symposium And Medical Imaging Conference:(1068–1072). 1995.

    Google Scholar 

  11. C. H. Nguyen. Modellering av operatør prosedyrer. M.Sc. Thesis (in Norwegian). Institute of Informatics, University of Oslo. 2000.

    Google Scholar 

  12. S. Nilsen and W. Zhang. XML Tagging Support in Procedure V&V. Institute for Energy Technology, Halden, Norway. Presented at the Workshop on Computerised Procedures, Halden, Norway. Nov. 30 and Dec. 1, 2000.

    Google Scholar 

  13. L. Reynes and G. Beltranda. A Computerised Control Room to Improve Nuclear Power Plant Operation and Safety. Nuclear Safety 31(4):504–511. 1990.

    Google Scholar 

  14. T. Sivertsen and H. Valisuo. Algebraic Specification andTheorem Proving usedin Formal Verification of Discrete Event Control Systems. Report: HWR-260, Institute for Energy Technology, Norway. 1989.

    Google Scholar 

  15. K. Ylikoski and G. Dahll. Verification of Procedures. Report: HWR-318, Institute for Energy Technology, Norway. 1992.

    Google Scholar 

  16. W. Zhang. Model Checking Operator Procedures. Proceedings of the 6th International SPIN Workshop on Practical Aspects of Model Checking. (Springer LNCS 1680: 200–215). Toulouse, France. 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for Energy Technology, P.O.Box 173, N-1751, Halden, Norway

    Wenhui Zhang

Authors
  1. Wenhui Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Telecommunications Software Engineering Ltd., 13Weston House, 18-22 Church Street, Lutterworth, Leicestershire, LE17 4AW, UK

    Rick Reed  & Jeanne Reed  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhang, W. (2001). Applying SDL Specifications and Tools to the Verification of Procedures. In: Reed, R., Reed, J. (eds) SDL 2001: Meeting UML. SDL 2001. Lecture Notes in Computer Science, vol 2078. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48213-X_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-48213-X_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-48213-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation