Formal Model-Based Development in Industrial Automation with Reactive Blocks

  • Peter HerrmannEmail author
  • Jan Olaf Blech
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9946)


The use of standard IT equipment to control machines is becoming increasingly popular mostly due to lower costs. Further, trends and initiatives such as Industry 4.0 and smart factories accelerate the use of standard IT components by demanding interconnected controllers and factory equipment communicating with internet services. This development offers new possibilities to use existing software frameworks and software architectural approaches as well as development standards in industrial automation. The formal methods-based support, that already exists for standard IT platforms, can now be applied to industrial control devices as well. In this paper, we look into the application of our Reactive Blocks framework for industrial automation. Reactive Blocks comes with a well established formal semantics and verification approaches tied to it. We demonstrate the advantages of our methodology with an example.


Model Checker Formal Method Control Software Programmable Logic Controller Industrial Automation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    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.) Integration of Software Specification Techniques for Applications in Engineering. LNCS, vol. 3147, pp. 517–540. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-27863-4_28 CrossRefGoogle Scholar
  2. 2.
    Bender, K., Katz, M.: PROFIBUS: der Feldbus für die Automation. Hanser (1990)Google Scholar
  3. 3.
    Bitreactive, A.S.: Reactive Blocks. Accessed 28 Jan 2016
  4. 4.
    Blech, J.O., Ould Biha, S.: Verification of PLC properties based on formal semantics in Coq. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 58–73. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-24690-6_6 CrossRefGoogle Scholar
  5. 5.
    Blech, J.O., Schmidt, H.: BeSpaceD: towards a tool framework and methodology for the specification and verification of spatial behavior of distributed software component systems. Technical report 1404.3537. (2014)
  6. 6.
    Boo, P.: A service tool grows up - ABB ServicePort. In: ABB Review (2015)Google Scholar
  7. 7.
    Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of PLC programs written in instruction list. In: Systems, Man, and Cybernetics, vol. 4, pp. 2449–2454. IEEE (2000)Google Scholar
  8. 8.
    Fernandez Adiego, B., Darvas, D., Vinuela, E.B., Tournier, J.C., Bliudze, S., Blech, J.O., Gonzalez Suarez, V.M.: Applying model checking to industrial-sized PLC programs. IEEE Trans. Ind. Inform. 11(6), 1400–1410 (2015)Google Scholar
  9. 9.
    Frey, G., Litz, L.: Formal methods in PLC programming. In: Systems, Man, and Cybernetics, vol. 4, pp. 2431–2436. IEEE (2000)Google Scholar
  10. 10.
    Gayet, P., Barillere, R.: UNICOS a framework to build industry like control systems: principles and methodology. In: International Conference on Accelerator and Large Experimental Physics Control Systems, Genève, Suisse (2005)Google Scholar
  11. 11.
    Graw, G.: Korrekte Steuerungssoftware. Dissertation, Technische Universität Dortmund (2010) (in German)Google Scholar
  12. 12.
    Han, F., Blech, J.O., Herrmann, P., Schmidt, H.: Model-based engineering and analysis of space-aware systems communicating via IEEE 802.11. In: 39th Annual International Computers, Software and Applications Conference (COMPSAC), pp. 638–646. IEEE Computer (2015)Google Scholar
  13. 13.
    Harland, J., Blech, J.O., Peake, I., Trodd, L.: Formal behavioural models to facilitate distributed development and commissioning in industrial automation. In: Evaluation of Novel Approaches to Software Engineering, COLAFORM Track (2016)Google Scholar
  14. 14.
    Herrmann, P., Blech, J.O., Han, F., Schmidt, H.: A model-based toolchain to verify spatial behavior of cyber-physical systems. Int. J. Web Serv. Res. (IJWSR) 13(1), 40–52 (2016)CrossRefGoogle Scholar
  15. 15.
    Herrmann, P., Krumm, H.: A framework for modeling transfer protocols. Comput. Netw. 34(2), 317–337 (2000)CrossRefGoogle Scholar
  16. 16.
    Hordvik, S., Øseth, K., Blech, J.O., Herrmann, P.: A methodology for model-based development and safety analysis of transport systems. In: 11th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE) (2016)Google Scholar
  17. 17.
    IEC: IEC Standard IEC 61161–3. Programmable Controllers – Programming Languages, 2.0 edn. (01 2003)Google Scholar
  18. 18.
    Kagermann, H., Wahlster, W., Helbig, J.: Umsetzungsempfehlungen für das Zukunftsprojekt Industrie 4.0. Abschlussbericht des Arbeitskreises Industrie 4, 5 (2013) (in German)Google Scholar
  19. 19.
    Kraemer, F.A., Herrmann, P.: Automated encapsulation of UML activities for incremental development and verification. In: Schürr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 571–585. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-04425-0_44 CrossRefGoogle Scholar
  20. 20.
    Kraemer, F.A., Herrmann, P.: Reactive semantics for distributed UML activities. In: Hatcliff, J., Zucca, E. (eds.) FMOODS/FORTE -2010. LNCS, vol. 6117, pp. 17–31. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-13464-7_3 CrossRefGoogle Scholar
  21. 21.
    Kraemer, F.A., Herrmann, P., Bræk, R.: Aligning UML 2.0 state machines and temporal logic for the efficient execution of services. In: Meersman, R., Tari, Z. (eds.) OTM 2006. LNCS, vol. 4276, pp. 1613–1632. Springer, Heidelberg (2006). doi: 10.1007/11914952_41 CrossRefGoogle Scholar
  22. 22.
    Kraemer, F.A., Slåtten, V., Herrmann, P.: Tool support for the rapid composition, analysis and implementation of reactive services. J. Syst. Softw. 82(12), 2068–2080 (2009)CrossRefGoogle Scholar
  23. 23.
    Kraemer, F.A., Herrmann, P.: formalizing collaboration-oriented service specifications using temporal logic. In: Networking and Electronic Commerce Research Conference (NAEC), pp. 194–220. ATSMA, Riva del Garda, October 2007Google Scholar
  24. 24.
    Lamport, L.: Specifying Systems: The TLA\(^+\) Language and Tools for Hardware and Software Engineers. Pearson Education Inc, London (2002)Google Scholar
  25. 25.
    Object Management Group: OMG Unified Modeling LanguageTM (OMG UML), Superstructure – Version 2.4.1 (2011). Accessed 28 Jan 2016
  26. 26.
    Rausch, M., Krogh, B.H.: Formal verification of PLC programs. In: American Control Conference, vol. 1, pp. 234–238. IEEE (1998)Google Scholar
  27. 27.
    Rushby, J.: Disappearing formal methods. In: High-Assurance Systems Engineering Symposium, pp. 95–96. ACM. Albuquerque (2000)Google Scholar
  28. 28.
    Steiner, W., Dutertre, B.: SMT-Based formal verification of a TTEthernet synchronization function. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 148–163. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-15898-8_10 CrossRefGoogle Scholar
  29. 29.
    Stursberg, O., Kowalewski, S., Hoffmann, I., Preußig, J.: Comparing timed and hybrid automata as approximations of continuous systems. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1996. LNCS, vol. 1273, pp. 361–377. Springer, Heidelberg (1997). doi: 10.1007/BFb0031569 CrossRefGoogle Scholar
  30. 30.
    Upton, E., Halfacree, G.: Raspberry Pi User Guide. Wiley, Cambridge (2014)Google Scholar
  31. 31.
    Vogel-Heuser, B., Witsch, D., Katzke, U.: Automatic code generation from a UML model to IEC 61131–3 and system configuration tools. In: International Conference on Control and Automation (ICCA), vol. 2, pp. 1034–1039. IEEE (2005)Google Scholar
  32. 32.
    Vyatkin, V., Hanisch, H.M.: Formal modeling and verification in the software engineering framework of IEC 61499: a way to self-verifying systems. In: Emerging Technologies and Factory Automation (ETFA), vol. 2. IEEE Computer (2001)Google Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.NTNUTrondheimNorway
  2. 2.RMIT UniversityMelbourneAustralia

Personalised recommendations