Abstract
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
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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.
Bryant, R. E., “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Tans. on Computers, 35(8), 677–691, 1986.
Bryant, R. E., “Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams”, Computing Surveys, 24(3), 298–318, 1992.
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.
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.
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.
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.
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.
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.
M. Jackson, Software Requirements and Specifications, ACM and Addison-Wesley, New York, 1995.
K. L. McMillan, Symbolic Model Checking — An Approach to the State Explosion Problem, Ph.D. Thesis, Carnegie Mellon University, 1992.
I. Moon, Automatic Verification of Discrete Chemical Process Control Systems, Ph.D. Thesis, Carnegie Mellon University, 1992.
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.
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.
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.
S. T. Probst, Chemical Process Safety and Operability Analysis using Symbolic Model Checking, Ph.D. Thesis, Carnegie Mellon University, 1996.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Turk, A.L., Probst, S.T., Powers, G.J. (1997). Verification of a chemical process leak test procedure. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_11
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive