Software & Systems Modeling

, Volume 18, Issue 2, pp 797–823 | Cite as

Model-based testing of software for automation systems using heuristics and coverage criterion

  • Rodrigo José Sarmento Peixoto
  • Leandro Dias da SilvaEmail author
  • Angelo Perkusich
Theme Section Paper


The aim of this work is to increase the confidence on software for automation systems defining a coverage criterion to measure the quality level of generated tests and the time interval needed to execute them. This coverage criterion called At Least N (ALN) is based on the Effect Predicate Heuristic (EPH) that provides all effect predicate for ISA 5.2 diagrams. The ALN and EPH have been incorporated into the Gungnir tool that was built using model-based testing concepts. The Gungnir uses timed automata to model the specification, in the ISA 5.2 diagrams, and the implementation, in the Ladder language. The timed automata models are automatically extracted, data tests are generated and the tool automatically verifies if the implementation is in conformance with the specification, given a quality level defined by the user.


Model-based testing Conformance tests Automation systems Timed automata Programmable logic controllers Ladder ISA 5.2 


  1. 1.
    AbouTrab, M.S., Brockway, M., Counsell, S., Hierons, R.M.: Testing real-time embedded systems using timed automata based approaches. J. Syst. Softw. 86(5), 1209–1223 (2013). CrossRefGoogle Scholar
  2. 2.
    Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)CrossRefzbMATHGoogle Scholar
  3. 3.
    Alur, R.: Timed Automata. Theor. Comput. Sci. 126, 183–235 (1999)CrossRefzbMATHGoogle Scholar
  4. 4.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Aspar, Z., Shaikh-Husin, N., Khalil-Hani, M.: Algorithm to convert programmable logic controller ladder logic diagram models to petri net models. In: 2015 IEEE Student Conference on Research and Development (SCOReD), pp. 156–161. IEEE (2015)Google Scholar
  6. 6.
    Bao, J., Wu, H., Yan, Y.: A fault diagnosis system-plc design for system reliability improvement. Int. J. Adv. Manuf. Technol. 75(1), 523–534 (2014). CrossRefGoogle Scholar
  7. 7.
    Behrmann, G., David, A., Larsen, P.K.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) LNCS, Formal Methods for the Design of Real-Time Systems (Revised Lectures), vol. 3185, pp. 200–237. Springer, Berlin (2004a)CrossRefGoogle Scholar
  8. 8.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: M. Bernardo, F. Corradini (eds.) Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, no. 3185 in LNCS, pp. 200–236. Springer (2004)Google Scholar
  9. 9.
    Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. Lect. Concurr. Petri Nets 1633, 8–22 (2004)zbMATHGoogle Scholar
  10. 10.
    Biallas, S., Brauer, J., Kowalewski, S.: Arcade.plc: A verification platform for programmable logic controllers. In: Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering, ASE 2012, pp. 338–341. ACM, New York, NY, USA (2012).
  11. 11.
    Bryan, L.A., Bryan, E.A.: Programmable Controllers: Theory and Implementation. Industrial Text Company. Illustrator-Kory, Gina (1997)Google Scholar
  12. 12.
    Chang, J.R., Huang, C.Y.: A study of enhanced mc/dc coverage criterion for software testing. In: 31st Annual International Computer Software and Applications Conference, 2007 (COMPSAC 2007), vol. 1, pp. 457 –464 (2007).
  13. 13.
    Chilenski, J., Miller, S.: Applicability of modified condition/decision coverage to software testing. Softw. Eng. J. 9(5), 193–200 (1994)CrossRefGoogle Scholar
  14. 14.
    de Vasconcelos Oliveira, K., Perkusich, A., Lima, A.M.N., Gorgônio, K., da Silva, L.D.: Standard-based formal validation of programmable logic controller programs. In: 2010 IEEE International Conference on Industrial Technology (ICIT), pp. 1655–1660. IEEE (2010)Google Scholar
  15. 15.
    de Vasconcelos Oliveira, K., da Silva, L.D., Perkusich, A., Lima, A.M.N., Gorgônio, K.: Automatic timed automata extraction from ladder programs for model-based analysis of control systems. In: 2010 IEEE International Symposium on Industrial Electronics, pp. 90–95. IEEE (2010)Google Scholar
  16. 16.
    Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: K. Havelund, G. Holzmann, R. Joshi (eds.) NASA Formal Methods: 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27–29, 2015, Proceedings, pp. 127–142. Springer International Publishing, Cham (2015)Google Scholar
  17. 17.
    Goble, W.M., Cheddie, H.: Safety Instrumented Systems Verification: Practical Probabilistic Calculations. ISA (2005)Google Scholar
  18. 18.
    Hasanain, W., Labiche, Y., Gheorghe, S.: Automated state-based online testing real-time embedded software with rtedge. In: 2015 3rd International Conference on Model-Driven Engineering and Software Development (MODELSWARD), pp. 294–302 (2015)Google Scholar
  19. 19.
    Hessel, A., Larsen, K., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing Real-Time systems using UPPAAL. In: Formal Methods and Testing, pp. 77–117. Springer (2008)Google Scholar
  20. 20.
    Hessel, A., Pettersson, P.: Cover—a real-time test case generation tool. In: Proceedings of the 19th IFIP International Conference on Testing of Communicating Systems and 7th International Workshop on Formal Approaches to Testing of Software (2007)Google Scholar
  21. 21.
    Iqbal, M.Z., Arcuri, A., Briand, L.: Environment modeling and simulation for automated testing of soft real-time embedded software. Softw. Syst. Model. 14(1), 483–524 (2015). CrossRefGoogle Scholar
  22. 22.
    ISA: Binary Logic Diagrams for Process Operations. ISA—The Instrumentation, Systems, and Automation Society, ISA 5.2-1976 (R1992) edn (1992)Google Scholar
  23. 23.
    Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)zbMATHGoogle Scholar
  24. 24.
    Kosmatov, N., Legeard, B., Peureux, F., Utting, M.: Boundary coverage criteria for test generation from formal models. In: 15th International Symposium on Software Reliability Engineering, pp. 139 – 150 (2004).
  25. 25.
    Kuzmin, E.V., Sokolov, V.A.: On construction and verification of PLC programs. Autom. Control Comput. Sci. 47(7), 443–451 (2013). CrossRefGoogle Scholar
  26. 26.
    Kuzmin, E.V., Sokolov, V.A.: Modeling, specification and construction of PLC-programs. Autom. Control Comput. Sci. 48(7), 554–563 (2014). CrossRefGoogle Scholar
  27. 27.
    Larsen, K.G., Mikucionis, M., Nielsen, B.: Uppaal Tron User Manual (2009). In
  28. 28.
    Larsen, K.G., Mikucionis, M., Nielsen, B., Skou, A.: Testing real-time embedded software using uppaal-tron: an industrial case study. In: EMSOFT ’05: Proceedings of the 5th ACM international conference on Embedded software, pp. 299–306. ACM, New York, NY, USA (2005).
  29. 29.
    Lo, H., Peleska, J.: Timed moore automata: Test data generation and model checking. In: 2010 Third International Conference on Software Testing, Verification and Validation, pp. 449 –458 (2010).
  30. 30.
    Ovatman, T., Aral, A., Polat, D., Ünver, A.O.: An overview of model checking practices on verification of plc software. Softw. Syst. Model. 15(4), 937–960 (2016). CrossRefGoogle Scholar
  31. 31.
    Parr, A.: Programmable Controllers an Engineers Guide, 3rd edn. Newnes, Oxford (2003)Google Scholar
  32. 32.
    PLCopen: IEC 61131-3: a standard programming resource. PLCopen For Efficiency in Automation (2004).
  33. 33.
    Quezada, J.C., Medina, J., Flores, E., Seck Tuoh, J.C., Solís, A.E., Quezada, V.: Simulation and validation of diagram ladder—petri nets. Int. J. Adv. Manuf. Technol. 1–13 (2016).
  34. 34.
    Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall, Hertfordshire (1992)zbMATHGoogle Scholar
  35. 35.
    Tahat, L., Vaysburg, B., Korel, B., Bader, A.: Requirement-based automated black-box test generation. In: 25th Annual International Computer Software and Applications Conference. COMPSAC 2001, pp. 489 –495 (2001).
  36. 36.
    Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann Publishers Inc., San Francisco (2006)Google Scholar
  37. 37.
    Waez, M.T.B., Dingel, J., Rudie, K.: A survey of timed automata for the development of real-time systems. Computer Science Review 9, 1–26 (2013). CrossRefzbMATHGoogle Scholar
  38. 38.
    Yu, Y., Lau, M.: Comparing several coverage criteria for detecting faults in logical decisions. In: Fourth International Conference on Quality Software, 2004 (QSIC 2004), Proceedings, pp. 14 – 21 (2004).

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2018

Authors and Affiliations

  • Rodrigo José Sarmento Peixoto
    • 1
  • Leandro Dias da Silva
    • 1
    Email author
  • Angelo Perkusich
    • 2
  1. 1.Instituto de ComputacãoUniversidade Federal de AlagoasMaceióBrazil
  2. 2.Laboratório de Sistemas Embarcados e Computacão Pervasiva, Unidade Acadêmica de Engenharia ElétricaUniversidade Federal de Campina GrandeCampina GrandeBrazil

Personalised recommendations