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

All Science Journal Classification (ASJC) codes

  • Chemical Engineering(all)
  • Computer Science Applications

Cite this