Skip to main content

2017 | OriginalPaper | Buchkapitel

Formal Modelling of Distributed Automation CPS with CP-Agnostic Software

verfasst von : Dmitrii Drozdov, Sandeep Patil, Valeriy Vyatkin

Erschienen in: Service Orientation in Holonic and Multi-Agent Manufacturing

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
1.
Zurück zum Zitat Årzén, K.E.: A simple event-based pid controller. In: 14th IFAC World Congress (1999) Årzén, K.E.: A simple event-based pid controller. In: 14th IFAC World Congress (1999)
2.
Zurück zum Zitat Åström, K.J.: Event based control. In: Analysis and Design of Nonlinear Control Systems, pp. 127–147 (2008) Åström, K.J.: Event based control. In: Analysis and Design of Nonlinear Control Systems, pp. 127–147 (2008)
3.
Zurück zum Zitat 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) 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)
4.
Zurück zum Zitat 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., 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)
5.
Zurück zum Zitat 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., 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)
6.
Zurück zum Zitat 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.: 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)
7.
Zurück zum Zitat 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., Christensen, J.H., Dubinin, V.N.: Bridging service-oriented architecture and IEC 61499 for flexibility and interoperability. IEEE Trans. Industr. Inf. 771–781 (2015)
8.
Zurück zum Zitat 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) 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)
9.
Zurück zum Zitat 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) 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)
10.
Zurück zum Zitat 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) 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)
12.
Zurück zum Zitat 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) 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)
13.
Zurück zum Zitat 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) 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)
14.
Zurück zum Zitat 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) 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)
15.
Zurück zum Zitat 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., 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)
16.
Zurück zum Zitat 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) 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)
17.
Zurück zum Zitat 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., 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
18.
Zurück zum Zitat 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., 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)
19.
Zurück zum Zitat 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 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)
20.
Zurück zum Zitat 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., 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)
21.
Zurück zum Zitat 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) 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)
22.
Zurück zum Zitat 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) 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)
23.
Zurück zum Zitat 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) 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)
24.
Zurück zum Zitat 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.: 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)
25.
Zurück zum Zitat 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.: 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)
26.
Zurück zum Zitat Vyatkin, V., Hanisch, H.M.: Verification of distributed control systems in intelligent manufacturing. J. Intell. Manuf. 123–136 (2003) Vyatkin, V., Hanisch, H.M.: Verification of distributed control systems in intelligent manufacturing. J. Intell. Manuf. 123–136 (2003)
27.
Zurück zum Zitat 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) 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)
28.
Zurück zum Zitat 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 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
Metadaten
Titel
Formal Modelling of Distributed Automation CPS with CP-Agnostic Software
verfasst von
Dmitrii Drozdov
Sandeep Patil
Valeriy Vyatkin
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-51100-9_4