臺灣博碩士論文加值系統

隨著工業物聯網IIoT（Industrial IoT）的發展，工廠的自主系統變得更加開放、動態、彈性、適應性及複雜化。這些系統中，最基本安全的要求應該意識到環境的變化，對於會產生負面影響的變化，在實施反饋閉環中不斷地調整系統的行為。為了確保自主系統在IIoT環境中的安全性，應將安全驗證移至運行時。在本論文中，為了處理安全運行時監控，我們通過使用Event-B的描述和反應代理模型，提出了安全規則的模型驅動方法。該方法將監控系統的安全規範轉換到在Event-B語法的描述中，透過使用Event-B的設計，進而將中間轉換過程的安全規範轉換成安全監控代理的規則。另外，我們還提出了監控架構，並使用參考AGV工業安全標準的案例來測試監控系統的表現。

With the development of IIoT (Industrial IoT), the autonomous system of the factory becomes more open, dynamic, flexible, adaptable and complex. The fundamental safety requirement of those systems should be aware of the changes in the environment that affect negatively and be implemented the feedback closed loop that continuously adjust the behavior of systems. To ensure safety of the autonomous system in IIoT environment, it is desirable to shift safety verification to runtime. In this thesis, to deal with the safety runtime monitoring, we proposed the model-driven approach of the safety rules by using the Event-B specification and reactive agent model. This approach transforms from specifying the safety rule for the monitored system to the design method in Event-B specification, using the design of Event-B to support the intermediate transformation process from the safety rule to the rule of the safety monitoring agent. We also proposed our monitoring architecture and use a case study in reference to AGV industrial safety standard to test the monitoring system.

口試委員會審定書 #
誌謝 i
中文摘要 ii
ABSTRACT iii
CONTENTS iv
LIST OF FIGURES vi
LIST OF TABLES vii
Chapter 1 Introduction 1
Chapter 2 Related Works 4
2.1 Formal Specification Language for Safety Expression 4
2.2 Monitoring Architecture 5
2.3 Event-B 5
Chapter 3 Rule Modeling for Safety Monitoring 8
3.1 Concept of Safety Rule and Process Overview 8
3.1.1 Warning State and Catastrophic State 8
3.1.2 Process Overview 9
3.2 Modeling the Safety Rule in Event-B 10
3.2.1 Meta-model of the Safety Rule 10
3.2.2 Safety Rule Design in Event-B Specification 13
3.3 Safety Monitoring Agent 18
3.3.1 Event-based FSM Approach 18
3.3.2 Reactive Agent Model 19
Chapter 4 Monitoring System Architecture 23
4.1 Instrumentation 24
4.2 Logging Layer 25
4.3 Safety Monitoring Agent 25
Chapter 5 Case Study 27
5.1 Safety Device 27
5.2 Basic Safety Rule 29
5.3 Safety Rule in Hazardous Zones 32
Chapter 6 Experiment Evaluation 34
6.1 Experiment Setup 34
6.2 Experiment Result 36
Chapter 7 Conclusion and Future Work 39
7.1 Conclusion 39
7.2 Future Work 39
REFERENCE 40

[1]M. Leucker and C. Schallhart, “A brief account of runtime verification,” Journal of Logic and Algebraic Programming, vol. 78, no. 5, pp. 293– 303, 2009.
[2]Vierhauser, M., Rabiser, R., Grünbacher, P.: Requirements monitoring frameworks: a systematic review. Inf. Softw. Technol. 80, 89–109 (2016)
[3]W. Robinson A roadmap for comprehensive requirements modeling Computer, 43 (5) (2009), pp. 64–72
[4]M. Machin, G. Jérémie, W. Hélène, J.-P. Blanquart, M. Roy, L. Masson, "SMOF - a safety monitoring framework for autonomous systems", IEEE Transactions on System Man and Cybernetics: Systems.
[5]B. Eberhardinger, J.-P. Stegh¨ofer, F. Nafz, and W. Reif, “Model- driven synthesis of monitoring infrastructure for reliable adaptive multi- agent systems,” in Proc. 24th IEEE Int. Symp. Software Reliability Engineering (ISSRE’13). IEEE, 2013, pp. 21–30.
[6]R. Calinescu, C. Ghezzi, M. Kwiatkowska, and R. Mirandola, “Self- adaptive software needs quantitative verification at runtime,” Commun. ACM, vol. 55, no. 9, pp. 69–77, Sep. 2012.
[7]J. Abrial, Modeling in Event-B: System and Software Engineering. New York, NY, USA: Cambridge Univ. Press, 2013.
[8]S. Hallerstede: On the purpose of Event-B proof obligations. Formal Aspects of Computing, 23: pp. 133-150, 2011.
[9]Back, R.-J.: Refinement calculus II: Parallel and reactive programs. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds.) Stepwise Refinement of Distributed Systems, Mook, The Netherlands, May 1989. Lecture Notes in Computer Science, vol. 430, pp. 67–93. Springer, Berlin (1990)
[10]M. Wooldridge, An Introduction to Multi-Agent Systems. Hoboken, NJ, USA: Wiley, 2002.
[11]A. Pnueli, The temporal logic of programs, Proceedings of the 18th IEEE Symposium on Foundation of Computer Science, 1977, 46-57
[12]J. Black and P. Koopman. System safety as an emergent property in composite systems. In Proceedings of the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2009), pp. 369–378, Estoril, Portugal, Jun 29 – Jul 2, 2009.
[13]X. Zheng, C. Julien, R. Podorozhny and F. Cassez, "BraceAssertion: Runtime Verification of Cyber-Physical Systems," 2015 IEEE 12th International Conference on Mobile Ad Hoc and Sensor Systems, Dallas, TX, 2015, pp. 298-306.
[14]Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon Moore, Qingzhou Luo, Aravind Sundaresan, Grigore Rosu, Borzoo Bonakdarpour, Scott A. Smolka, "ROSRV: Runtime verification for robots", LNCS 8734 Runtime Verification: 5th International Conference RV 2014, pp. 247-254, September 22–25, 2014.
[15]F. Chen and G. Ros¸u, “Java-MOP: A monitoring oriented programming environment for Java,” in TACAS’05, ser. LNCS, vol. 3440. SpringerVerlag, 2005, pp. 546–550.
[16]M. Kim, S. Kannan, I. Lee and O. Sokolsky, “Java-MaC: a Run-Time Assurance Tool for Java Programs”, Electronic Notes in Theoretical Computer Science 55, 2001.
[17]Lee Pike, Sebastian Niller, and Nis Wegmann. Runtime verification for ultra-critical systems. In Proceedings of the 2nd Intl. Conference on Runtime Verification, LNCS. Springer, September 2011.
[18]] A. Kane, O. Chowdhury, A. Datta & P. Koopman (2015): A Case Study on Runtime Monitoring of an Autonomous Research Vehicle (ARV) System. In E. Bartocci & R. Majumdar, editors: Runtime Verification: 6th International Conference, RV 2015, Vienna, Austria, September 22-25, 2015, Proceedings, LNCS 9333, Springer International Publishing, Vienna, Autria, pp. 102–117.
[19]X. Zheng; C. Julien; R. Podorozhny; F. Cassez; T. Rakotoarivelo, "Efficient and Scalable Runtime Monitoring for Cyber–Physical System," in IEEE Systems Journal , vol.PP, no.99, pp.1-12
[20]A. Goodloe and L. Pike, “Monitoring distributed real-time systems: A survey and future directions,” NASA Langley Research Center, Tech. Rep. NASA/CR-2010-216724, 2010.
[21]ANSI/ITSDF B56.5 -2012 “Safety Standard for Driverless, Automatic Guided Industrial Vehicles and Automated Functions of Manned Industrial Vehicles.”
[22]Roger Bostelman, Will Shackleford, Geraldine Cheok, Kamel Saidi, “Safe Control of Manufacturing Vehicles Research Towards Standard Test Methods,” Progress in Material Handling Practice (Book Chapter), June 2012.
[23]Development of Standard Test Methods for Unmanned and Manned Industrial Vehicles Used Near Humans