Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Formal Techniques for Safety-Critical Systems

FTSCS 2013: Formal Techniques for Safety-Critical Systems pp 125–141Cite as

Formalizing and Verifying Function Blocks Using Tabular Expressions and PVS

  • Conference paper
  • First Online:

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 419))

Abstract

Many industrial control systems use programmable logic controllers (PLCs) since they provide a highly reliable, off-the-shelf hardware platform. On the programming side, function blocks (FBs) are reusable components provided by the PLC supplier that can be combined to implement the required system behaviour. A higher quality system may be realized if the FBs are pre-certified to be compliant with an international standard such as IEC 61131-3. We present an approach to formalizing FB requirements using tabular expressions, and to verifying the correctness of the FBs implementations in the PVS proof environment. We applied our approach to the example FBs of IEC 61131-3 and identified issues in the standard: ambiguous behavioural descriptions, missing assumptions, and erroneous implementations.

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

Notes

  1. 1.

    PVS files are available at http://www.cas.mcmaster.ca/~lawford/papers/FTSCS2013. All verifications are conducted using PVS 5.0.

  2. 2.

    Other translation patterns can be found in [19].

  3. 3.

    For presenting our found issues, it suffices to show just the parts of in and \(q\).

  4. 4.

    If the less intuitive interpretation is intended, we fix the assumption accordingly.

References

  1. Bakhmach, E., Siora, O., Tokarev, V., Reshetytskyi, S., Kharchenko, V., Bezsalyi, V.: FPGA - based technology and systems for I&C of existing and advanced reactors. International Atomic Energy Agency, p. 173 (2009), IAEA-CN-164-7S04

    Google Scholar 

  2. Bauer, N., Engell, S., Huuck, R., Lohmann, S., Lukoschus, B., Remelhe, M., Stursberg, O.: Verification of PLC programs given as sequential function charts. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 517–540. Springer, Heidelberg (2004)

    Google Scholar 

  3. Blech, J.O., Biha, S.O.: On formal reasoning on the semantics of PLC using Coq. CoRR abs/1301.3047 (2013)

    Google Scholar 

  4. Camilleri, A., Gordon, M., Melham, T.: Hardware verification using higher-order logic. Technical Report UCAM-CL-TR-91, Cambridge University Computer Lab (1986)

    Google Scholar 

  5. Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of PLC programs written in instruction list. In: IEEE International Conference on Systems, Man and Cybernetics, pp. 2449–2454 (2000)

    Google Scholar 

  6. Eles, C., Lawford, M.: A tabular expression toolbox for Matlab/Simulink. In: NASA Formal Methods, pp. 494–499 (2011)

    Google Scholar 

  7. Hu, X., Lawford, M., Wassyng, A.: Formal verification of the implementability of timing requirements. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 119–134. Springer, Heidelberg (2009)

    Google Scholar 

  8. IEC: 61131–3 Ed. 2.0 en:2003: Programmable Controllers – Part 3: Programming Languages. International Electrotechnical Commission (2003)

    Google Scholar 

  9. IEC: 61131–3 Ed. 3.0 en:2013: Programmable Controllers – Part 3: Programming Languages. International Electrotechnical Commission (2013)

    Google Scholar 

  10. Jin, Y., Parnas, D.L.: Defining the meaning of tabular mathematical expressions. Sci. Comput. Program. 75(11), 980–1000 (2010)

    Article  MATH  Google Scholar 

  11. John, K.H., Tiegelkamp, M.: IEC 61131–3: Programming Industrial Automation Systems Concepts and Programming Languages, Requirements for Programming Systems, Decision-Making Aids, 2nd edn. Springer, Heidelberg (2010)

    Google Scholar 

  12. Kabra, A., Bhattacharjee, A., Karmakar, G., Wakankar, A.: Formalization of sequential function chart as synchronous model in Lustre. In: NCETACS, pp. 115–120 (2012)

    Google Scholar 

  13. Lawford, M., McDougall, J., Froebel, P., Moum, G.: Practical application of functional and relational methods for the specification and verification of safety critical software. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, p. 73. Springer, Heidelberg (2000)

    Google Scholar 

  14. Liu, Z., Parnas, D., Widemann, B.: Documenting and verifying systems assembled from components. Front. Comput. Sci. China 4(2), 151–161 (2010)

    Article  MATH  Google Scholar 

  15. Mader, A., Wupper, H.: Timed automaton models for simple programmable logic controllers. In: ECRTS, pp. 114–122. IEEE (1999)

    Google Scholar 

  16. Melham, T.: Abstraction mechanisms for hardware verification. VLSI Specification, Verification and Synthesis, pp. 129–157. Kluwer Academic Publishers, Boston (1987)

    Google Scholar 

  17. Németh, E., Bartha, T.: Formal verification of safety functions by reinterpretation of functional block based specifications. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 199–214. Springer, Heidelberg (2009)

    Google Scholar 

  18. Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)

    Google Scholar 

  19. Pang, L., Wang, C.W., Lawford, M., Wassyng, A.: Formalizing and verifying function blocks using tabular expressions and PVS. Technical Report 11, McSCert, Aug 2013

    Google Scholar 

  20. Parnas, D.L., Madey, J.: Functional documents for computer systems. Sci. Comput. Program. 25(1), 41–61 (1995)

    Article  Google Scholar 

  21. Parnas, D.L., Madey, J., Iglewski, M.: Precise documentation of well-structured programs. IEEE Trans. Softw. Eng. 20, 948–976 (1994)

    Article  Google Scholar 

  22. Roussel, J.M., Faure, J.: An algebraic approach for PLC programs verification. In: 6th International Workshop on Discrete Event Systems, pp. 303–308 (2002)

    Google Scholar 

  23. Soliman, D., Thramboulidis, K., Frey, G.: Transformation of function block diagrams to Uppaal timed automata for the verification of safety applications. Ann. Rev. Control 36, 338–345 (2012)

    Article  Google Scholar 

  24. Völker, N., Krämer, B.J.: Automated verification of function block-based industrial control systems. Sci. Comput. Program. 42(1), 101–113 (2002)

    Article  MATH  Google Scholar 

  25. Wassyng, A., Janicki, R.: Tabular expressions in software engineering. In: Proceedings of ICSSEA’03, Paris, France, vol. 4, pp. 1–46 (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. McMaster Centre for Software Certification, McMaster University, Hamilton, L8S 4K1, Canada

    Linna Pang, Chen-Wei Wang, Mark Lawford & Alan Wassyng

Authors
  1. Linna Pang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Chen-Wei Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mark Lawford
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alan Wassyng
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Linna Pang .

Editor information

Editors and Affiliations

  1. AIST, Research Institute for Secure Systems, Amagasaki, Japan

    Cyrille Artho

  2. University of Oslo Department of Informatics, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Pang, L., Wang, CW., Lawford, M., Wassyng, A. (2014). Formalizing and Verifying Function Blocks Using Tabular Expressions and PVS. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2013. Communications in Computer and Information Science, vol 419. Springer, Cham. https://doi.org/10.1007/978-3-319-05416-2_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-05416-2_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-05415-5

  • Online ISBN: 978-3-319-05416-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation