Verification of a logically controlled, solids transport system using symbolic model checking

Scott T. Probst; Gary J. Powers; D. E. Long; I. Moon

doi:10.1016/0098-1354(95)00265-0

Verification of a logically controlled, solids transport system using symbolic model checking

Scott T. Probst, Gary J. Powers, D. E. Long, I. Moon

Department of Chemical and Biomolecular Engineering

Research output: Contribution to journal › Article › peer-review

22 Citations (Scopus)

Abstract

Symbolic model checking has been used to formally verify safety and operability specifications on an industrial solids handling process. The fundamental principles behind symbolic model checking are presented along with techniques used to model process hardware, relay ladder logic control instructions, and human operating procedures for verification purposes. The computational resources required to check the example process are presented, and faults detected in this process through symbolic verification are documented.

Original language	English
Pages (from-to)	417-429
Number of pages	13
Journal	Computers and Chemical Engineering
Volume	21
Issue number	4
DOIs	https://doi.org/10.1016/0098-1354(95)00265-0
Publication status	Published - 1997

Bibliographical note

Funding Information:
Acknowledgements--This research has been supported by the National Science Foundation (grant DMC-6816889). We also thank Sergio Campos, a graduate student in Carnegie Mellon's School of Computer Science, for his help in interpreting SMV output.

All Science Journal Classification (ASJC) codes

Chemical Engineering(all)
Computer Science Applications

Access to Document

10.1016/0098-1354(95)00265-0

Cite this

@article{634995e3a4d340feafdc51689e58b866,

title = "Verification of a logically controlled, solids transport system using symbolic model checking",

abstract = "Symbolic model checking has been used to formally verify safety and operability specifications on an industrial solids handling process. The fundamental principles behind symbolic model checking are presented along with techniques used to model process hardware, relay ladder logic control instructions, and human operating procedures for verification purposes. The computational resources required to check the example process are presented, and faults detected in this process through symbolic verification are documented.",

author = "Probst, {Scott T.} and Powers, {Gary J.} and Long, {D. E.} and I. Moon",

note = "Funding Information: Acknowledgements--This research has been supported by the National Science Foundation (grant DMC-6816889). We also thank Sergio Campos, a graduate student in Carnegie Mellon's School of Computer Science, for his help in interpreting SMV output.",

year = "1997",

doi = "10.1016/0098-1354(95)00265-0",

language = "English",

volume = "21",

pages = "417--429",

journal = "Computers and Chemical Engineering",

issn = "0098-1354",

publisher = "Elsevier BV",

number = "4",

}

TY - JOUR

T1 - Verification of a logically controlled, solids transport system using symbolic model checking

AU - Probst, Scott T.

AU - Powers, Gary J.

AU - Long, D. E.

AU - Moon, I.

N1 - Funding Information: Acknowledgements--This research has been supported by the National Science Foundation (grant DMC-6816889). We also thank Sergio Campos, a graduate student in Carnegie Mellon's School of Computer Science, for his help in interpreting SMV output.

PY - 1997

Y1 - 1997

N2 - Symbolic model checking has been used to formally verify safety and operability specifications on an industrial solids handling process. The fundamental principles behind symbolic model checking are presented along with techniques used to model process hardware, relay ladder logic control instructions, and human operating procedures for verification purposes. The computational resources required to check the example process are presented, and faults detected in this process through symbolic verification are documented.

AB - Symbolic model checking has been used to formally verify safety and operability specifications on an industrial solids handling process. The fundamental principles behind symbolic model checking are presented along with techniques used to model process hardware, relay ladder logic control instructions, and human operating procedures for verification purposes. The computational resources required to check the example process are presented, and faults detected in this process through symbolic verification are documented.

UR - http://www.scopus.com/inward/record.url?scp=0030736966&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0030736966&partnerID=8YFLogxK

U2 - 10.1016/0098-1354(95)00265-0

DO - 10.1016/0098-1354(95)00265-0

M3 - Article

AN - SCOPUS:0030736966

SN - 0098-1354

VL - 21

SP - 417

EP - 429

JO - Computers and Chemical Engineering

JF - Computers and Chemical Engineering

IS - 4

ER -

Verification of a logically controlled, solids transport system using symbolic model checking

Abstract

Bibliographical note

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this