Skip to main content
SpringerLink
Log in

Validation of Control System Specifications with Abstract Plant Models

  • Conference paper
  • First Online:
Book cover Computer Safety, Reliability and Security (SAFECOMP 2000)

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

Included in the following conference series:

Abstract

Automatic procedures and manual procedures play important roles in the control of power plants. Their correctness is of great importance to the safe operation of power plants. Testing of such procedures is difficult, especially because of the problem of errors in specifications. By verifying high level specifications of automatic procedures andform alised specifications of manual procedures against an abstract plant model and a set of correctness requirements, this problem can be overcome to some extent. This paper describes the basic idea of such verification. It suggests using the verification approach as a complementary aid to traditional verification and validation which may involve different aspects including human factors.

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. E. M. Clarke and E. A. Emerson and A. P. Sistla. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications. Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages: 117–126, January 1983.

    Google Scholar 

  2. S. Collier and M. Green. Verification and Validation of Human Factors Issues in Control Room Design and Upgrades. OECD Halden Reactor Project Report: HWR-598, Institute for Energy Technology, Norway. 1999.

    Google Scholar 

  3. E. A. Emerson. Temporal and Model Logic. Handbook of theoretical computer science, Volume B: Formal Models and Semantics (ed. Jan van Leeuwen). Elsevier. 1990.

    Google Scholar 

  4. P. Godefroid and G. J. Holzmann. On the Verification of Temporal Properties. Protocol Specification, Testing and Verification, XIII (C-16). A. Dantine, G. Leduc and P. Walper (Eds). 1993.

    Google Scholar 

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

    Google Scholar 

  6. G. J. Holzmann. The Model Checker Spin. IEEE Transaction on Software Engineering 23(5): 279–295. 1997.

    Article  MathSciNet  Google Scholar 

  7. M. H. Lipner and S. P. Kerch. Operational Benefits of an Advanced Computerised Procedure System. 1994 IEEE Conference Record: Nuclear Science Symposium andMed ical Imaging Conference: 1068–1072. 1995.

    Google Scholar 

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

  9. H. Roth-Seefrid, J. Erdmann, L. Simon and M. Dull. SiROG: A Computer-based Manual for Situation Related Operator Guidance. Presentation at the Enlarged Halden Programme Group Meeting. Bolkesjø, Norway. October 1994.

    Google Scholar 

  10. T. Sivertsen and H. Valisuo. Algebraic Specification andT heorem Proving used in Formal Verification of Discrete Event Control Systems. OECD Halden Reactor Project Report: HWR-260, Institute for Energy Technology, Norway. 1989.

    Google Scholar 

  11. J. R. Taylor. Logical Validation of Safety and Control System Specifications Against Plant Models. Risø National Laboratory, Roskilde, Danmark. 1981.

    Google Scholar 

  12. J. Teigen and J. E. Hulsund. COPMA-III — Software Design andI mplementation Issues. OECD Halden Reactor Project Report: HWR-509, Institute for Energy Technology, Norway. 1998.

    Google Scholar 

  13. M. Y. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification. IEEE Symposium on Logic in Computer Science 1: 322–331, 1986.

    Google Scholar 

  14. W. Zhang. Model Checking Operator Procedures. Proceedings of the 6th International SPIN Workshop on Practical Aspects of Model Checking (Lecture Notes in Computer Science 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. Safety Science Group, TU Delft, Jaffalaan 5, 2628, BX Delft, The Netherlands

    Floor Koornneef

  2. SIMTECH, Max Euwelaan 60, 3062, MA Rotterdam, The Netherlands

    Meine van der Meulen

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhang, W. (2000). Validation of Control System Specifications with Abstract Plant Models. In: Koornneef, F., van der Meulen, M. (eds) Computer Safety, Reliability and Security. SAFECOMP 2000. Lecture Notes in Computer Science, vol 1943. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40891-6_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-40891-6_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41186-4

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation