Synthesis of safe operating procedure for multi-purpose batch processes using SMV

Jinkyung Kim, il Moon

Research output: Contribution to journalConference article

21 Citations (Scopus)

Abstract

Symbolic model verifier (SMV), an automatic error finding system, is developed and applied to various chemical processing systems to test their safety and feasibility. In this paper, we adopted SMV to synthesize error-free operating schedules in multi-purpose batch processes. The strength of this method is to synthesize a feasible sequence and to verify its safety simultaneously. Here, we propose two algorithms. One is to find embedded errors in operating sequences such as violating intermediate storage tank policies and unavailability due to sudden operating condition changes or insufficient production recipes. The other is the completion time algorithm to make sure that a makespan and a final operating sequence are obtained without errors. The proposed algorithm identifies errors and finds a minimum makespan and an operating sequence. Computation tree logic (CTL) embedded in SMV is extensively used to describe the situation of unsafe conditions and time related conditions for the final makespan. As a result of applying the algorithms to multi-purpose chemical processes, this approach finds a makespan and error, free operating schedules successfully. This combined synthesis and verification method also reduces the computation time and verifies operating schedules efficiently compared with the previously published algorithms. (C) 2000 Elsevier Science Ltd.

Original languageEnglish
Pages (from-to)385-392
Number of pages8
JournalComputers and Chemical Engineering
Volume24
Issue number2-7
DOIs
Publication statusPublished - 2000 Jul 15
Event7th International Symposium on Process Systems Engineering - Keystone, CO, USA
Duration: 2000 Jul 162000 Jul 21

Fingerprint

Processing

All Science Journal Classification (ASJC) codes

  • Chemical Engineering(all)
  • Control and Systems Engineering

Cite this

@article{8db59a9f00fd4d83bd2d8a8fc89bf979,
title = "Synthesis of safe operating procedure for multi-purpose batch processes using SMV",
abstract = "Symbolic model verifier (SMV), an automatic error finding system, is developed and applied to various chemical processing systems to test their safety and feasibility. In this paper, we adopted SMV to synthesize error-free operating schedules in multi-purpose batch processes. The strength of this method is to synthesize a feasible sequence and to verify its safety simultaneously. Here, we propose two algorithms. One is to find embedded errors in operating sequences such as violating intermediate storage tank policies and unavailability due to sudden operating condition changes or insufficient production recipes. The other is the completion time algorithm to make sure that a makespan and a final operating sequence are obtained without errors. The proposed algorithm identifies errors and finds a minimum makespan and an operating sequence. Computation tree logic (CTL) embedded in SMV is extensively used to describe the situation of unsafe conditions and time related conditions for the final makespan. As a result of applying the algorithms to multi-purpose chemical processes, this approach finds a makespan and error, free operating schedules successfully. This combined synthesis and verification method also reduces the computation time and verifies operating schedules efficiently compared with the previously published algorithms. (C) 2000 Elsevier Science Ltd.",
author = "Jinkyung Kim and il Moon",
year = "2000",
month = "7",
day = "15",
doi = "10.1016/S0098-1354(00)00485-3",
language = "English",
volume = "24",
pages = "385--392",
journal = "Computers and Chemical Engineering",
issn = "0098-1354",
publisher = "Elsevier BV",
number = "2-7",

}

Synthesis of safe operating procedure for multi-purpose batch processes using SMV. / Kim, Jinkyung; Moon, il.

In: Computers and Chemical Engineering, Vol. 24, No. 2-7, 15.07.2000, p. 385-392.

Research output: Contribution to journalConference article

TY - JOUR

T1 - Synthesis of safe operating procedure for multi-purpose batch processes using SMV

AU - Kim, Jinkyung

AU - Moon, il

PY - 2000/7/15

Y1 - 2000/7/15

N2 - Symbolic model verifier (SMV), an automatic error finding system, is developed and applied to various chemical processing systems to test their safety and feasibility. In this paper, we adopted SMV to synthesize error-free operating schedules in multi-purpose batch processes. The strength of this method is to synthesize a feasible sequence and to verify its safety simultaneously. Here, we propose two algorithms. One is to find embedded errors in operating sequences such as violating intermediate storage tank policies and unavailability due to sudden operating condition changes or insufficient production recipes. The other is the completion time algorithm to make sure that a makespan and a final operating sequence are obtained without errors. The proposed algorithm identifies errors and finds a minimum makespan and an operating sequence. Computation tree logic (CTL) embedded in SMV is extensively used to describe the situation of unsafe conditions and time related conditions for the final makespan. As a result of applying the algorithms to multi-purpose chemical processes, this approach finds a makespan and error, free operating schedules successfully. This combined synthesis and verification method also reduces the computation time and verifies operating schedules efficiently compared with the previously published algorithms. (C) 2000 Elsevier Science Ltd.

AB - Symbolic model verifier (SMV), an automatic error finding system, is developed and applied to various chemical processing systems to test their safety and feasibility. In this paper, we adopted SMV to synthesize error-free operating schedules in multi-purpose batch processes. The strength of this method is to synthesize a feasible sequence and to verify its safety simultaneously. Here, we propose two algorithms. One is to find embedded errors in operating sequences such as violating intermediate storage tank policies and unavailability due to sudden operating condition changes or insufficient production recipes. The other is the completion time algorithm to make sure that a makespan and a final operating sequence are obtained without errors. The proposed algorithm identifies errors and finds a minimum makespan and an operating sequence. Computation tree logic (CTL) embedded in SMV is extensively used to describe the situation of unsafe conditions and time related conditions for the final makespan. As a result of applying the algorithms to multi-purpose chemical processes, this approach finds a makespan and error, free operating schedules successfully. This combined synthesis and verification method also reduces the computation time and verifies operating schedules efficiently compared with the previously published algorithms. (C) 2000 Elsevier Science Ltd.

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

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

U2 - 10.1016/S0098-1354(00)00485-3

DO - 10.1016/S0098-1354(00)00485-3

M3 - Conference article

VL - 24

SP - 385

EP - 392

JO - Computers and Chemical Engineering

JF - Computers and Chemical Engineering

SN - 0098-1354

IS - 2-7

ER -