Abstract
The application of Symbolic Model Verification, SMV, to the fault analysis of chemical processing systems was investigated. The objective was to measure the ability of the modeling language, employed by SMV, to capture significant logical and dynamic behaviors present in the processing systems. These behaviors originated from continuous dynamic chemical processing equipment, failure prone human operators, and control systems that are composed of relay ladder logic executed by programmable logic controllers. Also, the study measured the time and effort required to build models of the processing systems, assemble appropriate specifications for these systems, verify the system models, interpret the results, and revise the system model or original process design. We have verified systems for the transportation of multi-component solids in a conveying process for the manufacture of aluminum, leak testing of a fuel gas piping network, and batch reaction to produce fertilizer. Verification of each of these systems revealed numerous faults that lead to improved designs.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
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.
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.
C. Chiu, and B. J. Kuipers, Comparative Analysis and Qualitative Integral Representations. Presented at the Third Qualitative Physics Workshops, Stanford, CA, August 1989.
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.
A. Falcione and B. H. Krogh, Design Recovery for Relay Ladder Logic. IEEE Control Systems Magazine, 13(2), April 1993.
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.
B. J. Kuipers, Qualitative Simulation using Time-Scale Abstraction. Int. J. Artificial Intelligence in Engineering, 3(4), 185–191, 1988
B. J. Kuipers, Reasoning with Qualitative Models. Artificial Intelligence, 59, 125–132, 1993
B. J. Kuipers, and B. Shultz, Reasoning in Logic about Continuous Systems. Principles of Knowledge Representation and Reasoning: Proceedings of the Fourth Annual International Conference, Ed. J. Doyle, E. Sandewall, and P. Torasso, Morgan Kaufmann, San Mateo, CA, 1994
D. E. Long, Model Checking Abstraction and Compositional Verification, Ph.D. Thesis, Carnegie Mellon University, 1993.
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 real time chemical processing systems. In: Maler, O. (eds) Hybrid and Real-Time Systems. HART 1997. Lecture Notes in Computer Science, vol 1201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014731
Download citation
DOI: https://doi.org/10.1007/BFb0014731
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62600-8
Online ISBN: 978-3-540-68330-8
eBook Packages: Springer Book Archive