Formal Support for the Safety Analysis of Requirement Models

  • Ken Chan
  • Clive Fencott
  • Barry Hebbron
Conference paper


This paper demonstrates the use of an established integrated method (that is Hazard and Operability Studies, Ward and Mellor Essential Models and the Synchronous Calculus of Communicating Systems) to model and analyse control systems. In particular, we discuss the interplay between traditional hazard analysis techniques and formal methods and their associated analyses in the context of an integrated model. Also a process model with tool supports is proposed for developing of a safety-critical software for real-time control systems. Our approach is illustrated by a small but realistic industrial case study.


Formal Method Temporal Logic Safety Property Formal Verification Proof Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Cha94]
    K. Chan. The investigation into proof tree analysis for concurrent systems and its practical applications. Master’s thesis, University of Teesside, Middlesbrough, 1994Google Scholar
  2. [CIS77]
    CISHEC. A guide to Hazard and Operability Studies. Technical report, The Chemical Industry Safety and Health Council of the Chemical Industries Association Ltd., 1977Google Scholar
  3. [CPS89]
    R. Cleaveland, J. Parrow, and B. Steffen. The concurency workbench: A semantics based tool for verification of concurrent systems. Technical report, University of Edinburgh, 1989Google Scholar
  4. [ES89]
    E. Emmerson and J. Srinivasan. Branching time temporal logic. Lecture Notes in Computer Science, 354, 1989Google Scholar
  5. [Fenng]
    P.C. Fencott. Formal Methods for Concurrency. Chapman and Hall, 1995 ForthcomingGoogle Scholar
  6. [FGL+94]
    P. C. Fencott, A. J. Galloway, M. A. Lockyer, S. J. O’Brien, and S. Pearson. Formalising the semantics of ward-mellor sa/rt essential model using a process algebra. Lecture Notes in Computer Science, 873, 1994Google Scholar
  7. [FH94a]
    C. Fencott and B. Hebbron. The application of HAZOP studies to integrated requirements models for control systems. In Proceedings of SAFECOMP 94, pages 83–92, Anaheim, USA, 1994Google Scholar
  8. [FH94b]
    C. P. Fenelon and B. D. Hebbron. Applying HAZOP to software engineering model. In Risk Management and Critical Protective Systems, Altrincham, UK, 1994Google Scholar
  9. [FKV94]
    M. D. Fraser, K. Kumar, and V. K. Vaishnavi; Strategies for incorporating formal specification. Communication of the ACM, 37 No.10:74–86, 1994CrossRefGoogle Scholar
  10. [Heb95]
    B. Hebbron. Applying HAZOP to a Ward and Mellor essential models. Technical Report TEES-BDH-001, University of Teesside, 1995Google Scholar
  11. [Kro93]
    K. Kronlof. Methods Integration: Concepts and case studies. John Wiley and sons, Nokia Research Center, Finland, 1993Google Scholar
  12. [Lap89]
    J. C. Laprie. Dependability: A unifying concept for reliable computing and fault tolerance, LAAS report (1986). In T. Anderson, editor, Dependability of resilient computers, chapter 1, pages 1–28. BSP Professional Books, 1989Google Scholar
  13. [LFT92]
    M. Lockyer, P.C. Fencott, and P. Taylor. The integration of structured and formal methods for real-time systems specification. In 5th Conference on Putting into Paractice Methods and Tools for Information Systems Design. University of Nantes, 1992Google Scholar
  14. [LG95]
    M. Lockyer and G. Griffiths. ASCENT: Automated Strict CASE Environment at Teesside. University of Teesside, Cleveland, England, 1995. Technical ManualGoogle Scholar
  15. [McD90]
    J. A. McDermid. Issues in Developing Software for Safety Critical Systems. Technical report, University of York, England, 1990Google Scholar
  16. [Mil89]
    R. Milner. Communication and Concurrency. Prentice-Hall, Hemel Hempstead, 1989MATHGoogle Scholar
  17. [Mol92]
    Faron Moller. The Edinburgh Concurrency Workbench (version 6.1). Technical report, University of Edinburgh, 1992Google Scholar
  18. [SFD92]
    L. T. Semmens, R. B. France, and T. W. G. Docker. Integrated structured analysis and formal specification techniques. The Computer Journal, 35(6):600–610, 1992CrossRefGoogle Scholar
  19. [Sti91]
    C. Stirling. An introduction to modal and temporal logics for CCS. Lecture Notes in Computer Science, 491, 1991Google Scholar
  20. [SW89]
    C. Stirling and D. J. Walker. Local model checking in the modal mu-calculus. Lecture Notes in Computer Science, 351:369–382, 1989MathSciNetCrossRefGoogle Scholar
  21. [WM85]
    P.T. Ward and S.J. Mellor. Structured Development for Real-Time Systems, volume 1,2,3. Prentice-Hall, 1985Google Scholar

Copyright information

© Springer-Verlag London 1995

Authors and Affiliations

  • Ken Chan
    • 1
  • Clive Fencott
    • 1
  • Barry Hebbron
    • 1
  1. 1.Centre for Modelling and SimulationUniversity of TeessideMiddlesbrough, ClevelandUK

Personalised recommendations