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

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

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)417-429
Number of pages13
JournalComputers and Chemical Engineering
Volume21
Issue number4
DOIs
Publication statusPublished - 1997 Jan 1

Fingerprint

Model checking
Ladders
Specifications
Hardware

All Science Journal Classification (ASJC) codes

  • Chemical Engineering(all)
  • Computer Science Applications

Cite this

Probst, Scott T. ; Powers, Gary J. ; Long, D. E. ; Moon, il. / Verification of a logically controlled, solids transport system using symbolic model checking. In: Computers and Chemical Engineering. 1997 ; Vol. 21, No. 4. pp. 417-429.
@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 il Moon",
year = "1997",
month = "1",
day = "1",
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",

}

Verification of a logically controlled, solids transport system using symbolic model checking. / Probst, Scott T.; Powers, Gary J.; Long, D. E.; Moon, il.

In: Computers and Chemical Engineering, Vol. 21, No. 4, 01.01.1997, p. 417-429.

Research output: Contribution to journalArticle

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, il

PY - 1997/1/1

Y1 - 1997/1/1

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

VL - 21

SP - 417

EP - 429

JO - Computers and Chemical Engineering

JF - Computers and Chemical Engineering

SN - 0098-1354

IS - 4

ER -