Automatic verification of operating schedules for batch processes using symbolic model checking: Latch model vs. real-time

Jinkyung Kim, Il Moon

Research output: Contribution to journalArticle

Abstract

This study proposes two models for reading Gantt charts and finding embedded errors in the operating schedules of batch processes. Two automatic techniques for finding errors, a real-time model and a latch model, are developed using the symbolic model verifier (SMV) and are compared to verify that the schedules are error free and to represent the scheduling information and policies. These models are designed to automatically detect embedded errors relating to unavailability, superimpositions, and violation of intermediate storage policies in batch processes with various intermediate storage policies.

Original languageEnglish
Pages (from-to)1654-1661
Number of pages8
JournalKorean Journal of Chemical Engineering
Volume27
Issue number6
DOIs
Publication statusPublished - 2010 Oct 18

Fingerprint

Model checking
Scheduling

All Science Journal Classification (ASJC) codes

  • Chemistry(all)
  • Chemical Engineering(all)

Cite this

@article{114fabad9ba8472c831bfeaa1373d5eb,
title = "Automatic verification of operating schedules for batch processes using symbolic model checking: Latch model vs. real-time",
abstract = "This study proposes two models for reading Gantt charts and finding embedded errors in the operating schedules of batch processes. Two automatic techniques for finding errors, a real-time model and a latch model, are developed using the symbolic model verifier (SMV) and are compared to verify that the schedules are error free and to represent the scheduling information and policies. These models are designed to automatically detect embedded errors relating to unavailability, superimpositions, and violation of intermediate storage policies in batch processes with various intermediate storage policies.",
author = "Jinkyung Kim and Il Moon",
year = "2010",
month = "10",
day = "18",
doi = "10.1007/s11814-010-0272-x",
language = "English",
volume = "27",
pages = "1654--1661",
journal = "Korean Journal of Chemical Engineering",
issn = "0256-1115",
publisher = "Springer New York",
number = "6",

}

Automatic verification of operating schedules for batch processes using symbolic model checking : Latch model vs. real-time. / Kim, Jinkyung; Moon, Il.

In: Korean Journal of Chemical Engineering, Vol. 27, No. 6, 18.10.2010, p. 1654-1661.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Automatic verification of operating schedules for batch processes using symbolic model checking

T2 - Latch model vs. real-time

AU - Kim, Jinkyung

AU - Moon, Il

PY - 2010/10/18

Y1 - 2010/10/18

N2 - This study proposes two models for reading Gantt charts and finding embedded errors in the operating schedules of batch processes. Two automatic techniques for finding errors, a real-time model and a latch model, are developed using the symbolic model verifier (SMV) and are compared to verify that the schedules are error free and to represent the scheduling information and policies. These models are designed to automatically detect embedded errors relating to unavailability, superimpositions, and violation of intermediate storage policies in batch processes with various intermediate storage policies.

AB - This study proposes two models for reading Gantt charts and finding embedded errors in the operating schedules of batch processes. Two automatic techniques for finding errors, a real-time model and a latch model, are developed using the symbolic model verifier (SMV) and are compared to verify that the schedules are error free and to represent the scheduling information and policies. These models are designed to automatically detect embedded errors relating to unavailability, superimpositions, and violation of intermediate storage policies in batch processes with various intermediate storage policies.

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

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

U2 - 10.1007/s11814-010-0272-x

DO - 10.1007/s11814-010-0272-x

M3 - Article

AN - SCOPUS:84856365098

VL - 27

SP - 1654

EP - 1661

JO - Korean Journal of Chemical Engineering

JF - Korean Journal of Chemical Engineering

SN - 0256-1115

IS - 6

ER -