Formal Modeling of Cyber-Physical System for Conveyor Sorter

 
 
 
  • Abstract
  • Keywords
  • References
  • PDF
  • Abstract


    Conveyor is usually used in materials handling in manufacturing. Conveyor able to transfer the product from one to another place. In order to use concept of Cyber Physical System (CPS), conveyor have to represent itself to user in cyber and physical. CPS is a communication between cyber and physical of product in real-time system which is user can control the conveyor by using cyber or manually. In this paper, we focused on three goals which are to design CPS model for manufacturing application, modelling the system by using concept Object-Oriented (OO) in any OO software and verification on model using model-checking method. This paper proposes conveyor system as the model for manufacturing. We represent the model as cyber conveyor according to physical conveyor and proposed the methodology how they communicate each other in real time.

     

     


     

  • Keywords


    cyber-physical system; formal method; industrial automation system; model checking; programmable logic controller.

  • References


      [1] Lee, J., Bagheri, B. and Kao, H.A. A cyber-physical systems architecture for industry 4.0-based manufacturing systems. Manufacturing Letters. 2015. 3, 18-23.

      [2] Baheti, R. and Gill, H. Cyber-physical systems. The Impact of Control Technology. 2011. 12(1), 161-166.

      [3] Liu, Y., Peng, Y., Wang, B., Yao, S. and Liu, Z. Review on cyber-physical systems. IEEE/CAA Journal of Automatica Sinica. 2017. 4(1), 27-40.

      [4] Zhang, L. Formal methods for aspect-oriented specification of cyber physical systems. Proceedings of the International Conference on Computer Science, Environment, Ecoinformatics, and Education. 2011. pp. 316-322.

      [5] Seshia, S.A., Sadigh, D. and Sastry, S.S. Formal methods for semi-autonomous driving. Proceedings of the 52nd Annual Design Automation Conference. 2015. pp. 1-5.

      [6] Clarke, E.M. and Wing, J.M. Formal methods: State of the art and future directions. ACM Computing Surveys. 1996. 28(4), 626-643.

      [7] Wing, J.M. A specifier’s introduction to formal methods. IEEE Computer. 1990. 23(9), 8-24.

      [8] Alawneh, L., Debbabi, M., Hassaine, F., Jarraya, Y. and Soeanu, A. A unified approach for verification and validation of systems and software engineering models. Proceedings of the 13th Annual IEEE International Symposium and Workshop Engineering of Computer Based Systems. 2006. pp. 1-10.

      [9] Stevenson, D.E. Verification and validation of complex systems. Proceedings of the Artificial Neural Networks in Engineering: Smart Engineering System Design. 2002. pp. 159-164.

      [10] Lee, E.A. and Seshia, S.A. Introduction to embedded systems: A cyber-physical systems approach. 2016. MIT Press.

      [11] Lee, E.A. Cyber physical systems: Design challenges. Proceedings of the 11th IEEE Symposium on Object Oriented Real-Time Distributed Computing. 2008. pp. 363-369.

      [12] Seshia, S.A. New frontiers in formal methods: Learning, cyber-physical systems, education, and beyond. CSI Journal of Computing. 2(4), 1-14.

      [13] Baheti, R. and Gill, H. Cyber-physical systems. In T. Samad and A.M. Annaswamy (Eds.), The Impact of Control Technology. IEEE Control Systems Society. 2011. pp. 161-166.

      [14] Fitzgerald, J., Gamble, C., Larsen, P.G., Pierce, K. and Woodcock, J., Cyber-physical systems design: Formal foundations, methods and integrated tool chains. Proceedings of the IEEE/ACM 3rd FME Workshop Formal Methods in Software Engineering. 2015. pp. 40-46.

      [15] Alwi, S. and Fujimoto, Y. Formal verification of logic control systems with nondeterministic behaviors. IEEJ Journal of Industry Applications. 2(16), 306-314, 2013.

      [16] Alwi, S. and Fujimoto, Y. Safety property comparison between Gr¨obner Bases and BDD-based model checking method. Proceedings of the 13th International Conference on Control, Automation, Robotics and Vision. 2014. pp. 511-516.

      [17] Alwi, S. and Fujimoto, Y. On a safety of sequential control system based on Gr¨obner Bases computation. Proceedings of the International Conference on Control Automation and Systems. 2010. pp. 3-28.

      [18] Griffor, E.R., Greer, C., Wollman, D.A. and Burns, M.J. Framework for cyber-physical systems: Volume 1, Overview. No. Special Publication (NIST SP)-1500-201. 2017.

      [19] Frey, G. and Litz, L. Formal methods in PLC programming. Proceedings of the IEEE International Conference on Systems, Man, and Cybernetics. 2000. pp. 2431-2436.

      [20] Gawanmeh, A., Abu Omar, A. and April, A. Design and analysis of control strategies for a cyber-physical system. Computer Systems Science and Engineering. 2017. 32(5), 397-403.

      [21] Clarke, E.M., Grumberg, O. and Peled, D. Model checking. 1999. MIT Press.


 

View

Download

Article ID: 23429
 
DOI: 10.14419/ijet.v7i3.28.23429




Copyright © 2012-2015 Science Publishing Corporation Inc. All rights reserved.