Skip to main content
SpringerLink
Log in
Book cover

International Andrei Ershov Memorial Conference on Perspectives of System Informatics

PSI 2014: Perspectives of System Informatics pp 76–91Cite as

Neutralizing Semantic Ambiguities of Function Block Architecture by Modeling with ASM

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8974))

Abstract

The Function Blocks Architecture of the IEC 61499 standard is an executable component model for distributed embedded control systems combining block-diagrams and state machines. The standard aims at the portability of control applications that is however hampered by ambiguities in its execution semantics descriptions. In recent years several execution models have been implemented in different software tools that generate mutually incompatible code.

This paper proposes a general approach to neutralizing these semantic ambiguities by formal description of the IEC 61499 in abstract state machines (ASM). The model embodies all known execution semantics of function blocks. The ASM model is further translated to the input format of the SMV model-checker which is used to verify formally properties of applications. In this way the proposed verification framework enables the portability checking of component-based control applications across different implementation platforms compliant with the IEC 61499 standard.

The paper first discusses different existing execution semantics of function blocks and the portability issues across different IEC 61499 tools. Then a modular formal model of function blocks’ operational semantics in ASM is introduced and exemplified in the paper by the cyclic execution semantics case for a composite function block. Subsequently, the SMV model is generated and model-checking is illustrated for a simple test case.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. International Standard IEC 61499 Function blocks—Part 1: Architecture, IEC Standard 61499-1 (2012)

    Google Scholar 

  2. Vyatkin, V.: IEC 61499 as enabler of distributed and intelligent automation: state-of-the-art review. IEEE Trans. Indus. Inf. 7, 768–781 (2011)

    Article  Google Scholar 

  3. Vyatkin, V.: The IEC 61499 standard and its semantics. Indus. Electron. Mag. IEEE 3, 40–48 (2009)

    Article  Google Scholar 

  4. Patil, S., Dubinin, V., Vyatkin, V.: Formal Modelling and Verification of IEC61499 Function Blocks with Abstract State Machines and SMV: the Cyclic Semantics Case (2014). https://pure.ltu.se/portal/en/publications/formal-modelling-and-verification-of-iec61499-function-blocks-with-abstract-state-machines-and-smv-the-cyclic-semantics-case%28a703dd4b-cd09-41ea-af45-67d8889852fe%29.html

  5. Cengic, G., Akesson, K.: On formal analysis of IEC 61499 applications, part B: Execution semantics. IEEE Trans. Indus. Inf. 6, 145–154 (2010)

    Article  Google Scholar 

  6. Cengic, G., Akesson, K.: On formal analysis of IEC 61499 applications, part A: modeling. IEEE Trans. Indus. Inf. 6, 136–144 (2010)

    Article  Google Scholar 

  7. Dubinin, V., Vyatkin, V.: On definition of a formal model for IEC 61499 function blocks. EURASIP J. Embedded Syst. 2008, 1–10 (2008)

    Article  Google Scholar 

  8. ICS Triplex ISaGRAF Workbench for IEC 61499/61131, v6. http://www.icstriplex.com/

  9. Gurevich, Y.: Logic and the challenge of computer science. In: Current Trends in Theoretical Computer Science, pp. 1–57 (1988)

    Google Scholar 

  10. Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford University Press, Inc. (1995)

    Google Scholar 

  11. Stark, R.F., Borger, E., Schmid, J.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)

    Book  Google Scholar 

  12. Börger, E., et al.: A high-level modular definition of the semantics of C#. Theor. Comput. Sci. 336, 235–284 (2005)

    Article  MATH  Google Scholar 

  13. Börger, E., Glässer, U., Muller, W.: A formal definition of an abstract VHDL 1993 simulator by EA-machines. In: Kloos, C., Breuer, P. (eds.) Formal Semantics for VHDL, vol. 307, pp. 107–139. Springer US, New York (1995)

    Google Scholar 

  14. Glässer, U., Gurevich, Y., Veanes, : An abstract communication model. Technical Report MSR-TR-2002-55, Microsoft Research2002

    Google Scholar 

  15. Glässer, U., Gurevich, Y., Veanes, M.: High-Level Executable Specification of the Universal Plug and Play Architecture. In: Presented at the HICSS 2002

    Google Scholar 

  16. Börger, E., Rosenzweig, D.: A mathematical definition of full Prolog. Sci. Comput. Programm. 24, 249–286 (1995)

    Article  MATH  Google Scholar 

  17. Gurevich, Y., Huggins, J.: The semantics of the C programming language. In: Meinke, K., Börger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol. 832, pp. 334–336. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  18. Börger, E., Schulte, W.: A programmer friendly modular definition of the semantics of java. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 353–404. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Hanisch, H.-M., et al.: One decade of IEC 61499 modeling and verification-results and open issues. In: 13th IFAC Symposium on Information Control Problems in Manufacturing, V.A. Trapeznikov Institute of Control Sciences, Russia (2009)

    Google Scholar 

  20. Bonfe, M., Fantuzzi, C.: Design and verification of mechatronic object-oriented models for industrial control systems. In: ETFA 2003, IEEE Conference on Emerging Technologies and Factory Automation, vol. 2, pp. 253–260 (2003)

    Google Scholar 

  21. Dimitrova, D., Frey, G., Bachkova, I.: Formal approach for modeling and verification of IEC 61499 function blocks. In: Advanced Manufacturing Technologies (AMTECH 2005), Russe, Bulgaria, pp. 731–736 (2005)

    Google Scholar 

  22. 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 1999, vol. 1, pp. 261–270 (1999)

    Google Scholar 

  23. Dubinin, V., et al.: Analysis of extended net condition/event systems on the basis of model checking. In: Presented at the Proceedings of International Conference on New Information Technologies and Systems (NITS 2010), vol. 2, pp.20–48. Penza (2010) (Originally published in Russian)

    Google Scholar 

  24. Dubinin, V., Vyatkin, V., Hanisch, H.M.: Modelling and verification of IEC 61499 applications using Prolog. In: IEEE Conference on Emerging Technologies and Factory Automation, ETFA 2006, pp. 774–781 (2006)

    Google Scholar 

  25. Schnakenbourg, C., Faure, J.M., Lesage, J.J.: Towards IEC 61499 function blocks diagrams verification. In: 2002 IEEE International Conference on Systems, Man and Cybernetics, vol. 3, p. 6 (2002)

    Google Scholar 

  26. Junbeom, Y., Sungdeok, C., Eunkyung, J.: A verification framework for FBD based software in nuclear power plants. In: 15th Asia-Pacific Software Engineering Conference, APSEC 2008, pp. 385–392 (2008)

    Google Scholar 

  27. Dubinin, V.N., Vyatkin, V.: Semantics-robust design patterns for IEC 61499. IEEE Trans. Indus. Inf. 8, 279–290 (2012)

    Article  Google Scholar 

  28. Pang, C., et al.: A portability study of IEC 61499: Semantics and Tools. In: 12th IEEE Conference on Industrial Informatics (INDIN 2014), pp. 440–445. Porto Alegre, Brazil (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Penza State University, Penza, Russia

    Victor Dubinin

  2. Department of Computer Science Electrical and Space Engineering, Luleå University of Technology, Luleå, Sweden

    Sandeep Patil, Cheng Pang & Valeriy Vyatkin

Authors
  1. Sandeep Patil
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Victor Dubinin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Cheng Pang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Valeriy Vyatkin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sandeep Patil .

Editor information

Editors and Affiliations

  1. School of Computer Science, University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

  2. A.P. Ershov Institute of Informatics Systems, Novosibirsk, Russia

    Irina Virbitskaite

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Patil, S., Dubinin, V., Pang, C., Vyatkin, V. (2015). Neutralizing Semantic Ambiguities of Function Block Architecture by Modeling with ASM. In: Voronkov, A., Virbitskaite, I. (eds) Perspectives of System Informatics. PSI 2014. Lecture Notes in Computer Science(), vol 8974. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46823-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-46823-4_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-46822-7

  • Online ISBN: 978-3-662-46823-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation