在批次工廠的操作過程中，不免會發生硬體設備的故障，倘若依據既有線上測量數據無法有效率地診斷出可能的失誤根源，輕則影響產能，重則造成財產損失及人員傷亡。一般而言，提高診斷效率的方式有二，除了增設額外感測器之外，執行測試步驟也是可以達到此一目的的手段。在過去的研究中，Kang與Chang (2014)曾以非時間自動機模式為基礎提出有效合成測試計畫的方法，但對於製程的描述以及失誤的判斷缺乏時間因素的考量。在本研究中，我們以時間自動機(timed automata)為基礎並且利用模型驗證工具UPPAAL (Behrmann et al., 2006)，系統化的產生出診斷測試步驟。具體的工作項目有三，即(1)建構批次製程中所有設備元件的時間自動機模式、(2)利用模型驗證工具搜尋失誤可視事件串與(3)依據失誤可視事件串合成最適測試步驟。在本論文中我們以三個案例來展現此方式的可行性及正確性。

Hardware failures are inevitable but random events in the useful life of a batch chemical plant. If these fault origins are not efficiently diagnosed, their consequences can be very serious and even catastrophic. In general, two remedial measures should be considered to enhance diagnostic performance of a given batch process, i.e., adding online sensors and/or implementing test operations. Since the former option has already been discussed extensively in the literature, the present study focuses only upon the latter. In a recent paper, Kang and Chang (2014) presented an effective method to generate diagnostic test plans on the basis of untimed automata. However, the failure-induced abnormal system behaviors cannot always be characterized adequately due to the lack of time-tracking mechanisms in their models. A systematic procedure synthesis strategy is therefore developed in the present work to address this issue by making use of timed automata and the model-checking capabilities of existing software UPPAAL (Behrmann et al., 2006). Three specific tasks are required to be performed in sequence:
(1) All embedded components in the given process are first described with timed automata according to a set of systematic model-building rules;
(2) All fault propagation scenarios and the corresponding observable event traces (OETs) are identified next with the above models and the model-checking tools in UPPAAL;
(3) The optimal test plan for every OET is then established with the same models and tools.
Extensive case studies have been carried out in this work to confirm the validity and effectiveness of the proposed approach.

Alur, R., Dill, D. L., 1994. A theory of timed automata. Theoretical Computer Sci. 126, 183-235.

Baroni, P., Lamperti, G., Pogliano, P., Zanella, M., 1999. “Diagnosis of large active systems.” Artif. Intell. 110 (1), 135–183.

Baroni, P., Lamperti, G., Pogliano, P., Zanella, M., 2000. Diagnosis of a class of distributed discrete-event systems. IEEE Trans. Syst. Man Cybern. Part A: Syst. Hum. 30 (6), 731–752.

Bauer, N., Engell, S., Huuck, R., Lohmann, S., Lukoschus, B., Remelhe, M., Stursberg, O., 2004. Verification of PLC programs given as sequential function charts. In Integration of software specification techniques for applications in Engineering, 517-540, Springer Berlin Heidelberg.

Behrmann, G., David, A., Larsen, K.G., 2006. A Tutorial on UPPAAL 4.0., Department of Computer Science. Aalborg University, Denmark.

Benveniste, A., Fabre, E., Haar, S., Jard, C., 2003. Diagnosis of asynchronous discrete-event systems: a net unfolding approach. IEEE Trans. Autom. Control 48 (5), 714–727.

Cassandras, C.G., Lafortune, S., 1999. Introduction to Discrete Event Systems. Kluwer Academic Publisher, Boston.

Chen, Y.C., Yeh, M.L., Hong, C.L., Chang, C.T., 2010. Petri-net based approach to configure online fault diagnosis systems for batch processes. Ind. Eng. Chem. Res. 49 (9), 4249-4268.

Clarke, E.M., Emerson, A., Sistla, K.L., 1986. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Lang. and Sys. 8, 244-263.

Debouk, R., Lafortune, S., Teneketzis, D., 2000. Coordinated decentralized protocols for failure diagnosis of discrete event systems. Discret. Event Dyn. Syst. Theory Appl. 10 (1–2), 33–86.

Kang, A., Chang, C. T., 2014. Automata generated test plans for fault diagnosis in sequential material-and energy-transfer operations. Chem. Eng. Sci. 113, 101-115.

Kim, J., Moon, Il., 2009. Automatic verification of control logics in safety instrumented system design for chemical process industry. Journal of Loss Prevention in the Process Industries 22, 975-980.

Kim, J., Moon, Il., 2011. Model Checking for Automatic Verification of Control Logics in Chemical Process. Ind. Eng. Chem. Res. 50, 905-915.

Kourti, T., Macgregor, J.F., 1995. Process analysis, monitoring and diagnosis, using multivariate projection methods. Chemometrics and Intelligent Laboratory Systems 28 (1), 3-21.

Kourti, T., Nomikos, P., Macgregor, J.F., 1995. Analysis monitoring and fault-diagnosis of batch processes using multiblock and multiway PLS. Journal of Process Control 5 (4), 277-284.

Lahtinen, J., Valkonen, J., Björkman, K., Frits, J., Niemelä, I., Heljanko, K., 2012. Model checking of safety-critical software in the nuclear engineering domain. Reliability Engineering & System Safety 105, 104-113.

Lee, J.M., Yoo, C.K., Lee, I.B., 2004. Fault detection of batch processes using multiway kernel principal component analysis. Computers & Chemical Engineering 28 (9), 1837-1847.

Li, J. H., Chang, C. T., Jiang, D., 2014. Systematic generation of cyclic operating procedures based on timed automata. Chem. Eng. Res. & Des., 92(1), 139-15.

Lohmann, S., Stursberg, O., Engell, S., 2006. Systematic design of logic controllers for processing plants starting from informal specifications. Computer Aided Chemical Engineering 21, 1317-1322.

Nomikos, P., MacGregor, J.F., 1994. Monitoring batch processes using multiway principal component analysis. AIChE J. 40 (8), 1361-1375.

Nomikos, P., MacGregor, J.F., 1995. Multivariate SPC charts for monitoring batch processes. Technometrics 37 (1), 41-59.

Nozari, H. A., Banadaki, H. D., Shoorehdeli, M. A., Simani, S., 2011. Model-based fault detection and isolation using neural networks: An industrial gas turbine case study. In Systems Engineering (ICSEng), 2011 21st International Conference on IEEE, 26-31.

Qiu, W.B., Kumar, R., 2006. Decentralized failure diagnosis of discrete event system. IEEE Trans. Syst. Man Cybern. Part A: Syst. Hum. 36 (3), 384-395.

Sampath, M., Lafortune, S., Teneketzis, D., 1998. Active diagnosis of discrete-event systems. IEEE Trans. Autom. Control 43 (7), 908-929.

Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D., 1995. Diagnosability of discrete-event systems. IEEE Trans. Autom. Control 40 (9), 1555-1575.

Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.C., 1996. Failure diagnosis using discrete-event models. IEEE Trans. Control Syst. Technol. 4 (2), 105-124.

Simeu-Abazi, Z., Di Mascolo, M., Knotek, M., 2007. Diagnosis of discrete event systems using timed automata. Proceedings of the IFAC-CEA conference.

Subbiah, S., Panek, S., Engell, S., Stursberg, O., 2007. Scheduling of multi-product batch plants using reachability analysis of timed automata models. INSTICC Press ICINCO-ICSO, 141-148.

Tan, W. L., Nor, N. M., Abu Bakar, M. Z., Ahmad, Z., Sata, S. A., 2012. Optimum parameters for fault detection and diagnosis system of batch reaction using multiple neural networks. Journal of Loss Prevention in the Process Industries, 25(1), 138-141.

Undey, C., Ertunc, S., Cinar, A., 2003. Online batch fed-batch process performance monitoring, quality prediction, and variable contribution analysis for diagnosis. Ind. Eng. Chem. Res. 42 (20), 4645-4658.

Yeh, M.L., Chang, C.T., 2011. An Automaton-Based Approach to Evaluate and Improve Online Diagnostic Schemes for Multi-Failure Scenarios in Batch Processes. Chem. Eng. Res. Des 89, 2652-2666.

Yeh, M.L., Chang, C.T., 2012. An automata-based approach to synthesize untimed operating procedures in batch chemical processes. Korean J. Chem. Eng. 29, 583-594.

Zad, S.H., Kwong, R.H., Wonham, W.M., 2003. Fault diagnosis in discrete-event systems: framework and model reduction. IEEE Trans. Autom. Control 48 (7), 1199-1204.

Zhao, C., 2014. Quality-relevant fault diagnosis with concurrent phase partition and analysis of relative changes for multiphase batch processes. AIChE Journal 60(6), 2048-2062.