Search

In this paper, we provide a review of Professor Powers’s and his students’ work on connecting fault analysis, discrete process control, human operating procedures, and symbolic model checking. In recent years, this type of research is placed under the banner of “cyber-physical systems research”. Some of the techniques and procedures Powers and his students developed can be found in the open literature and conference proceedings. However, they have not been published broadly due to the untimely passing of Professor Powers. A complete overview of the methods are not available, and the cap-stone results obtained in the two last Ph.D. theses have not been published.

This study focuses on the applications of model checking techniques in automatic synthesis for the reachability of process systems. Model checking is an automatic method used to verify if a circuit or a condition, expressed as a concurrent transition system, satisfies a set of properties. The strength of this method lies in its ability to synthesize a feasible sequence with a counterexample and to verify its correctness using temporal logics such as computation tree logic (CTL) simultaneously. These challengeable approaches are implemented in a commercial software package (UPPAAL) using graphical discrete modeling, automata theory, and CTL to automate the synthesis for the reachability of process systems. Three use cases of interest in computer-aided engineering due to the difficulty involved in synthesizing them manually are explored. In the first use case, the optimal operating procedure according to the objective function of a paper mill process is synthesized. In the second use case, a challengeable a...

This study focused on a novel approach for classifying hazardous chemicals to be used for chemical terrorism. We developed a novel algorithm to classify nationally customized chemicals of interest (COI) out of 325 COI in USA. The proposed COI classification algorithm aims to identify a key set of factors that reflect nation-wide uniqueness: intentional use, objectives, toxicity, related laws (CWC, ITF-25, CAA, etc.) and responsive counter-actions to terrorism. Although the U.S. has managed 325 COI to prevent terrorism, there are some nations in which the management and control of all the hazardous chemicals are beyond their capability. Based upon the outcome of this study the Ministry of the Environment of Korea has made appropriate revisions on relevant law. As a result, the Korean government has officially added a new set of 13 chemical species to the list of existing hazardous chemicals. This work is worthwhile to contribute to protecting the people’s lives and property from possible chemical accidents including terror by chemicals.

Bio-fuels represent promising candidates for renewable liquid fuels. One of the challenges for the emerging industry is the high level of uncertainty in supply amounts, market demands, market prices, and processing technologies. These uncertainties complicate the assessment of investment decisions. This paper presents a model for the optimal design of biomass supply chain networks under uncertainty. The uncertainties manifest themselves as a large number of stochastic model parameters that could impact the overall profitability and design. The supply chain network we study covers the Southeastern region of the United States and includes biomass supply locations and amounts, candidate sites and capacities for two kinds of fuel conversion processing, and the logistics of transportation from the locations of forestry resources to the conversion sites and then to the final markets. To reduce the design problem to a manageable size the impact of each uncertain parameter on the objective function is computed for each end of the parameter's range. The parameters that cause the most change in the profit over their range are then combined into scenarios that are used to find a design through a two stage mixed integer stochastic program. The first stage decisions are the capital investment decisions including the size and location of the processing plants. The second stage recourse decisions are the biomass and product flows in each scenario. The objective is the maximization of the expected profit over the different scenarios. The robustness and global sensitivity analysis of the nominal design (for a single nominal scenario) vs. the robust design (for multiple scenarios) are analyzed using Monte Carlo simulation over the hypercube formed from the parameter ranges.

This study focused on the automatic verification and validation of the safety and correctness of chemical process control logics. Discrete events, system behaviors, and control logic of chemical processes were formally modeled as automata. The symbolic model checking method was used to verify its safety and reliability. The strength of this method is synthesizing a feasible sequence through a counter-example and simultaneously verifying its correctness using computation tree logic (CTL). The model checking method was applied to determine the error-free design of the control operating sequence and automatically find the logical errors. An automatic technique is proposed to provide and modify the P&ID design of control logics for the chemical process industry. This Article addresses the model development of the control logics for industrial chemical processes and presents several case studies to show how a model checking approach can be used for the efficient verification of control logics.

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.

The study focuses on assessing the security risk of the terrorism in the chemical industry. This research modifies conventional risk assessment methods for including terrorism and sabotage scenarios. The objective of this risk assessment is to identify security hazards, threats and vulnerabilities facing each target facility, and to find the adequate countermeasures to protect the public, workers, national interest, environment, and companies. This study results in implementing software to analyze the possibility of terrorism and sabotage. This program includes five steps: asset characterization, threat assessment, vulnerability analysis, risk assessment and new countermeasures. It is a systematic, risk-based approach in which risk is a function of the severity of consequences of an undesired event, the likelihood of adversary attack, and the likelihood of adversary success in causing the undesired event. The reliability of this method is verified by the dock zone case. This study suggests an effective approach to chemical terrorism response management.

The main purpose of this study was to develop a computer automated tool for fault tree analysis (FTA) in order to minimize the flaws of manual FTA. The automated FTA system developed in this study consists of two steps: 1) automatic fault tree conversion from a digraph, and 2) calculation of the probability of the occurrence of the top event and finding a minimal cut set of the top event. For the first step, we propose a new algorithm for automatic conversion of a digraph to a fault tree. The new digraph-FT conversion algorithm has eight FT generation rules to transform node information that is based on the node characteristics. Failures and faults are classified into three types to easily synthesize fault trees and analyze fault trees precisely. The automatic FTA system was then applied the analysis of real chemical processes to illustrate the effectiveness of the system.

This study develops a modified method of TRIZ to improve safety in chemical process design. This method is modified by the theory of TRIZ, which is inventive problem solving theory, for retrofit design of chemical process considering safety. The original TRIZ is difficult to access to chemical process safety due to inapplicability and ambiguity of terminology in classification of these parameters. It is necessary to be modified TRIZ for chemical process safety. This study reorganized thirty-nine parameters of the TRIZ into six categories such as mechanic, operator, process upset, design, natural hazard and material. The modified TRIZ is tested to jacketed reactor and polyethylene reactor.

Automatic model checking is used to determine the error-free design of the SIS (Safety Instrumented System) and to find the logical errors in the chemical processes. It proposes an automatic technique to provide and to modify the P&ID design of SIS control logics. This method can be applied to verify its correctness of SIS and to find the logical errors by synthesizing a feasible sequence automatically. This study focuses on automatic verifying and synthesizing for the design, operability and reachability of SIS control logics in chemical processes.

This paper focuses on the development of a new approach for the synthesis of error-free operating schedules in batch processes. The synthesis of error-free operating procedures for batch processes becomes an important issue in the safe operation of industrial plant. It spends considerable amount of time and effort in scheduling and verifying operating procedures for correctness and completeness. In this study, we adopted SMV (Symbolic Model Verifier), an automatic error finding system, which is applied to various batch processes to test their safety and feasibility. The strength of this method is to minimize safety hazard and operability errors, and adjust process and recipe changes during the planning of operating procedure. The proposed approach identifies embedded errors and finds a minimum makespan and synthesizes an error-free operating sequence at the same time. Several examples are presented to illustrate the effectiveness of the proposed approaches.

This study focuses on automatic searching and verifying methods for the reachability, transition logics and hierarchical structure in all possible paths of biological processes using model checking. The automatic search and verification for alternative paths within complex and large networks in biological process can provide a considerable amount of solutions, which is difficult to handle manually. Model checking is an automatic method for verifying if a circuit or a condition, expressed as a concurrent transition system, satisfies a set of properties expressed in a temporal logic, such as computational tree logic (CTL). This article represents that model checking is feasible in biochemical network verification and it shows certain advantages over simulation for querying and searching of special behavioral properties in biochemical processes.

Three types of unsaturated polyester resins were synthesized from the glycolysis of polyethylene terephthalate (PET) plastic waste, considering environment, cost and properties for their applications. These synthesized unsaturated polyester resins could be used for various construction processes and materials such as no dig pipelining (NDR-1), pultrusion (PLR-1) and polymer concrete (PCR-1). PET was taken from common soft-drink bottles, and ethylene glycol (EG), diethylene glycol (DEG) and MPdiol glycol mixtures were used for the depolymerization at molar ratios. The glycolyzed PET 1st products (oligomers) were reacted with maleic anhydride, phthalic anhydride and dicyclopentadiene (DCPD) (especially for polymer concrete) to form unsaturated polyester resins with mixed styrene. The lab scale (1–5 kg) and pilot plant scale-up tests (200 kg) were experimented to evaluate the processing characteristics, viscosity, acid number and curing behaviors. The main properties such as hardness, flexural strength, tensile strength, heat distortion temperature, elongation, and chemical resistance were determined based on the various uses of the three resins. Furthermore, the applicability and the properties of these developed resins were verified through many real application tests.

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.

The safety verification of chemical processing systems becomes more difficult due to their complexity. Current search methods suffer from the state explosion problem, mainly because the verification problem itself is inherently complex considering numerous units (reactor, distillation column, storage tank), instruments (valve, pump), control software and many other components, and more importantly considering time. This paper focuses on methods of improving the search algorithm in its efficiency. The algorithm enables to prune out the state transition paths that cannot happen in the behavior of process equipment and operating procedures in system modeling. The state transition structure constructed by this algorithm becomes enormously smaller in its search space. Computing time is also reduced and safety verifications of more complex processes and operating procedures become possible.