Verification of a chemical process leak test procedure

  • Adam L. Turk
  • Scott T. Probst
  • Gary J. Powers
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


A leak test procedure for a combustion system which is used in the chemical industry was verified. This procedure is important since it reduces the probability of explosions. Both government and internal company standards where employed in creating the initial leak test procedure. Several major faults were discovered by the verification of a logic model of the procedure and equipment using SMV. This paper describes the leak test procedure with its corresponding combustion system pipe network, the approach employed in modeling the process, failure modes included in the process model, computational challenges, and verification results. This study indicates that the formal method, SMV, is an appropriate tool for verification of industrial processes of modest complexity


Failure Mode Model Check Transition Relation Combustion System Binary Decision Diagram 
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.


  1. [1]
    R. Anderson, P. Beame, S. Burns, W. Chan, F. Modugno, D Notkin, and J. Reese, Model Checking Large Software Specifications. Proceedings of the Fourth ACM Symposium on the Foundation of Software Engineering: 156, 166, October, 1996.Google Scholar
  2. [2]
    Bryant, R. E., “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Tans. on Computers, 35(8), 677–691, 1986.Google Scholar
  3. [3]
    Bryant, R. E., “Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams”, Computing Surveys, 24(3), 298–318, 1992.Google Scholar
  4. [4]
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hawng, Symbolic Model Checking: 1020 states and Beyond. Information and Computation, 98(2): 142–170, June 1992.Google Scholar
  5. [5]
    J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan and D. L. Dill, Symbolic Model Checking for Sequential Circuit Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13, 401–424, 1994.Google Scholar
  6. [6]
    E. M. Clarke, A. Emerson and A. P. Sistla, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8 (2), 244–263, 1986.Google Scholar
  7. [7]
    E. M. Clarke, T. Filkorn, and S. Jha, Exploiting Symmetry in Temporal Logic Model Checking. Proceedings of the Fifth Workshop on Computer-Aided Verification, Ed. C. Courcoubetis. June/July 1993.Google Scholar
  8. [8]
    E. M. Clarke, O. Grumberg, K. L. McMillan, and X. Zhao, Effective Generation of Counterexamples and Witnesses in Symbolic Model Checking. Technical Report No. CMU-CS-94-204, Carnegie Mellon University, PA, 1994.Google Scholar
  9. [9]
    V. Hartonas-Garmhausen, T. Kurfess, E. M. Clarke, and D. E. Long, Automatic Verification of Industrial Designs. Proceedings of the 1995 IEEE Workshop on Industrial-Strength Formal Specification Techniques. 88–96. IEEE Comput. Soc. Press, April 1995.Google Scholar
  10. [10]
    M. Jackson, Software Requirements and Specifications, ACM and Addison-Wesley, New York, 1995.Google Scholar
  11. [11]
    K. L. McMillan, Symbolic Model Checking — An Approach to the State Explosion Problem, Ph.D. Thesis, Carnegie Mellon University, 1992.Google Scholar
  12. [12]
    I. Moon, Automatic Verification of Discrete Chemical Process Control Systems, Ph.D. Thesis, Carnegie Mellon University, 1992.Google Scholar
  13. [13]
    S. T. Probst, G. J. Powers, D. E. Long, and I. Moon, Verification of a Logically Controlled Solids Transport System using Symbolic Model Checking. Submitted for publication in Computers and Chemical Engineering, 1994.Google Scholar
  14. [14]
    S. T. Probst, and G. J. Powers, Automatic Verification of Control Logic in the Presence of Process Faults. Presented at the Annual AIChE Conference, San Francisco, CA, November 1994.Google Scholar
  15. [15]
    S. T. Probst, A. L. Turk, and G. J. Powers, Formal Verification of a Furnace System Standard. Presented at the Annual AIChE Conference, Miami Beach, FL, November 1995.Google Scholar
  16. [16]
    S. T. Probst, Chemical Process Safety and Operability Analysis using Symbolic Model Checking, Ph.D. Thesis, Carnegie Mellon University, 1996.Google Scholar
  17. [17]
    T. Sreemani and J. Atlee, Feasibility of Model Checking Software Requirements: A Case Study. Technical Report CS96-05, Department of Computer Science, University of Waterloo, January, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Adam L. Turk
    • 1
  • Scott T. Probst
    • 1
  • Gary J. Powers
    • 1
  1. 1.Department of Chemical EngineeringCarnegie Mellon UniversityUSA

Personalised recommendations