Abstract
This paper introduces the application of formal modelling to cyber-physical systems for the purpose of formal verification of cyber-physical agnosticism properties of decentralised automation software. Service-oriented cyber-physical systems are modelled using the IEC 61499 function block architecture. Then, the IEC 61499 model is represented in terms of SMV formal language, which is verified using the nuXmv model checker. The timestamped events mechanism is implemented in IEC 61499 using the existing syntax of the standard. The impact of jitter on the behaviour of physical system is demonstrated in both simulation within IEC 61499 execution environment and in counter-examples extracted from nuXmv. The methodology presented in this paper creates the premise for automatic verification of the cyber-physical agnosticism of systems.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Årzén, K.E.: A simple event-based pid controller. In: 14th IFAC World Congress (1999)
Åström, K.J.: Event based control. In: Analysis and Design of Nonlinear Control Systems, pp. 127–147 (2008)
Carloni, L.P., McMillan, K.L., Sangiovanni-Vincentelli, A.L.: Theory of latency-insensitive design. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 1059–1076 (2001)
Dai, W., Christensen, J.H., Vyatkin, V., Dubinin, V.: Function block implementation of service oriented architecture: case study. In: 2014 12th IEEE International Conference on Industrial Informatics (INDIN), pp. 112–117. IEEE (2014)
Dai, W., Peltola, J., Vyatkin, V., Pang, C.: Service-oriented distributed control software design for process automation systems. In: 2014 IEEE International Conference on Systems, Man and Cybernetics (SMC), pp. 3637–3642. IEEE (2014)
Dai, W., Vyatkin, V., Christensen, J.H.: The application of service-oriented architectures in distributed automation systems. In: 2014 IEEE International Conference on Robotics and Automation (ICRA), pp. 252–257. IEEE (2014)
Dai, W., Vyatkin, V., Christensen, J.H., Dubinin, V.N.: Bridging service-oriented architecture and IEC 61499 for flexibility and interoperability. IEEE Trans. Industr. Inf. 771–781 (2015)
Dai, W., Vyatkin, V., Pang, C., Christensen, J.H.: Time-stamped event based execution semantics for industrial cyber-physical systems. In: 2015 IEEE 13th International Conference on Industrial Informatics (INDIN), pp. 1263–1268. IEEE (2015)
Demin, E., Dubinin, V., Patil, S., Vyatkin, V.: Automation services orchestration with function blocks: Web-service implementation and performance evaluation. In: Service Orientation in Holonic and Multi-Agent Manufacturing, pp. 213–221. Springer (2016)
Derhamy, H., Drozdov, D., Patil, S., van Deventer, J., Eliasson, J., Vyatkin, V.: Orchestration of arrowhead services using IEC 61499: Distributed automation case study. In: Proceedings of 2016 IEEE 20th International Conference on Emerging Technologies & Factory Automation (ETFA 2016). IEEE International Conference on Emerging Technologies and Factory Automation. Proceedings, IEEE (2016)
Drozdov, D.: fb2smv tool. https://github.com/dmitrydrozdov/fb2smv
Drozdov, D., Patil, S., Dubinin, V., Vyatkin, V.: Formal verification of cyber-physical automation systems modelled with timed block diagrams. In: 2016 IEEE 25th International Symposium on Industrial Electronics (ISIE). IEEE (2016)
Gerber, C., Ivanova-Vasileva, I., Hanisch, H.M.: Formal modelling of IEC 61499 function blocks with integer-valued data types. Control Cybern. 197–231 (2010)
Hanisch, H.M., Hirsch, M., Missal, D., Preuße, S., Gerber, C.: One decade of IEC 61499 modeling and verification–results and open issues. In: IFAC Proceedings Volumes, pp. 211–216 (2009)
Pang, C., Dai, W., Vyatkin, V.: Towards IEC 61499 models of computation in ptolemy ii. In: Industrial Electronics Society, IECON 2015-41st Annual Conference of the IEEE, pp. 001988–001993. IEEE (2015)
Pang, C., Vyatkin, V.: Automatic model generation of IEC 61499 function block using net condition/event systems. In: 2008 6th IEEE International Conference on Industrial Informatics, pp. 1133–1138. IEEE (2008)
Patil, S., Vyatkin, V., Pang, C.: Counterexample-guided simulation framework for formal verification of flexible automation systems. In: 2015 IEEE 13th International Conference on Industrial Informatics (INDIN), pp. 1192–1197, July 2015
Patil, S., Drozdov, D., Dubinin, V., Vyatkin, V.: Cloud-Based Framework for Practical Model-Checking of Industrial Automation Applications, pp. 73–81. Springer International Publishing, Cham (2015)
Patil, S., Dubinin, V., Vyatkin, V.: Formal verification of IEC 61499 function blocks with abstract state machines and smv–modelling. In: 2015 IEEE Trustcom/BigDataSE/ISPA, vol. 3, pp. 313–320. IEEE (2015)
Patil, S., Dubinin, V., Vyatkin, V.: Formal modelling and verification of IEC 61499 function blocks with abstract state machines and smv–execution semantics. In: International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, pp. 300–315. Springer (2015)
Patil, S., Zhabelova, G., Vyatkin, V., McMillin, B.: Towards formal verification of smart grid distributed intelligence: Freedm case. In: IECON 2015-41st Annual Conference of the IEEE Industrial Electronics Society, pp. 003974–003979. IEEE (2015)
Sorouri, M., Patil, S., Salcic, Z., Vyatkin, V.: Software composition and distributed operation scheduling in modular automated machines. IEEE Trans. Industr. Inf. 865–878 (2015)
Stanica, M., Guéguen, H.: Using timed automata for the verification of IEC 61499 applications. In: Discrete Event Systems 2004 (WODES’04): A Proceedings Volume from the 7th IFAC Workshop, Reims, France, 22–24 Sept 2004, p. 375. Elsevier (2005)
Vyatkin, V., Hanisch, H.M.: Development of adequate formalisms for verification of IEC 1499 distributed applications. In: SICE 2000. Proceedings of the 39th SICE Annual Conference. International Session Papers, pp. 73–78. IEEE (2000)
Vyatkin, V., Hanisch, H.M.: A modeling approach for verification of IEC1499 function blocks using net condition/event systems. In: 1999 7th IEEE International Conference on Emerging Technologies and Factory Automation, 1999. Proceedings. ETFA’99, vol. 1, pp. 261–270. IEEE (1999)
Vyatkin, V., Hanisch, H.M.: Verification of distributed control systems in intelligent manufacturing. J. Intell. Manuf. 123–136 (2003)
Vyatkin, V., Pang, C., Tripakis, S.: Towards cyber-physical agnosticism by enhancing IEC 61499 with ptides model of computations. In: Industrial Electronics Society, IECON 2015-41st Annual Conference of the IEEE, pp. 001970–001975. IEEE (2015)
Zhabelova, G., Patil, S., Yang, C.W., Vyatkin, V.: Smart grid applications with IEC 61499 reference architecture. In: 2013 11th IEEE International Conference on Industrial Informatics (INDIN), pp. 458–463, July 2013
Acknowledgements
This work was supported, in part, by the Vetenskapetsråd (Sweden) project DIACPA D.nr. 2015-04675.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Drozdov, D., Patil, S., Vyatkin, V. (2017). Formal Modelling of Distributed Automation CPS with CP-Agnostic Software. In: Borangiu, T., Trentesaux, D., Thomas, A., Leitão, P., Oliveira, J. (eds) Service Orientation in Holonic and Multi-Agent Manufacturing . SOHOMA 2016. Studies in Computational Intelligence, vol 694. Springer, Cham. https://doi.org/10.1007/978-3-319-51100-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-51100-9_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-51099-6
Online ISBN: 978-3-319-51100-9
eBook Packages: EngineeringEngineering (R0)