Automatic Verification of Control Software in Cyber-Physical Systems with Plant Simulators

  • T. V. Lyakh
  • V. E. ZyubinEmail author
  • N. O. Garanina
Automation Systems in Scientific Research and Industry


The paper describes solving the problem of automatic verification of control software in cyber-physical systems created by means of process-oriented programming. A method based on plant simulators is proposed, and its implementation on the basis of the LabVIEW package and Reflex language translator is described.


verification control software cyber-physical systems plant simulators process-oriented programming 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    A. D. Zakrevskii, Parallel Algorithms of Logic Control (Editorial URSS, Moscow, 2003).Google Scholar
  2. 2.
    F. Wagner, R. Schmuki, T. Wagner, and P. Wolstenholme, Modeling Software With Finite State Machines: A Practical Approach (Auerbach Publications, New York, 2006).CrossRefzbMATHGoogle Scholar
  3. 3.
    D. Harel, “Statecharts: A Visual Formalism for Complex Systems,” Sci. Comput. Programm. 8(3), 231–274 (1987).MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    V. E. Zyubin, “Hyper-Automaton: A Model of Control Algorithms,” in Proc. of the IEEE Intern. Siberian Conf. on Control and Communications (SIBCON 2007), Tomsk, Russia, April 20–21, 2007, pp. 51–57. DOI:
  5. 5.
    T. V. Liakh and V. E. Zyubin, “The Reflex Language Usage to Automate the Large Solar Vacuum Telescope,” in Proc. of the 17th Intern. Conf. of Young Specialists on Micro/Nanotechnologies and Electron Devices (EDM-16), Erlagol, Russia, June 30–July 4, 2016, pp. 137–139. DOI:
  6. 6.
    F. Basile, P. Chiacchio, and D. Gerbasio, “On the Implementation of Industrial Automation Systems Based on PLC,” IEEE Trans. Automation Sci. Eng. 10(4), 990–1003 (2013).CrossRefGoogle Scholar
  7. 7.
    K. Thramboulidis, “A Cyber-Physical System-Based Approach for Industrial Automation Systems,” Comput. Industry 72(C), 92–102 (2015). Scholar
  8. 8.
    M. Samek and P. Montgomery, “State Oriented Programming,” Embedded Syst. Programm. 13(8), 22–43 (2000).Google Scholar
  9. 9.
    A. A. Shalyto and N. I. Tukkel, “SWITCH Technology as an Automated Approach to the Development of Software for ‘Response’ Systems,” Programmir. 27(5), 45–62 (2001).zbMATHGoogle Scholar
  10. 10.
    A. S. Rozov and V. E. Zyubin, “Process-Oriented Programming Language for MCU-Based Automation,” in Proc. of the IEEE Intern. Siberian Conf. on Control and Communications (SIBCON 2013), Krasnoyarsk, Russia, September 12–13, 2013, pp. 1–4. DOI:
  11. 11.
    T. V. Liakh, A. S. Rozov, and V. E. Zyubin, “Reflex Language: A Practical Notation for Cyber-Physical Systems,” System Informatics 2(12), 85–104 (2018).Google Scholar
  12. 12.
    V. Zyubin, “Using Process-Oriented Programming in LabVIEW,” in Proc. of the 2nd IASTED Intern. Multi-Conf. on Automation, Control, and Information Technology: Control, Diagnostics, and Automation, Novosibirsk, Russia, June 15–18, 2010, Vol. 1, pp. 35–41.Google Scholar
  13. 13.
    N. Garanina, V. Zyubin, T. Lyakh, and S. Gorlatch, “An Ontology of Specification Patterns for Verification of Concurrent Systems,” in Proc. of the 17th Intern. Conf. SoMeT-18. Ser.: Frontiers in Artificial Intell. and Appl. (IOS Press, Amsterdam, 2018), Vol. 303, pp. 515–528. DOI: Scholar
  14. 14.
    N. V. Shilov and N. O. Garanina, “Combined Logics of Knowledge, Time, and Actions for Reasoning about Multi-Agent Systems,” Knowledge Process. Data Analysis, No. 6581, 48–58 (2011).Google Scholar
  15. 15.
    V. I. Shelekhov, “Verification and Synthesis of Summation Codes on the Basis of Operator Correctness Rules,” Modelir. Analiz Inform. Sistem, 17(4), 101–110 (2010).Google Scholar
  16. 16.
    E. M. Clarke and S. Gao, “Model Checking Hybrid Systems,” in Proc. of the 6th Intern. Symp. on Leveraging Applications of Formal Methods, Verification and Validation, Corfu, Greece, October 8–11, 2014, Is. 8803, pp. 385–386.Google Scholar
  17. 17.
    D. Drozdov, S. Patil, V. Dubinin, and V. Vyatkin, “Towards Formal Verification for Cyber-Physically Agnostic Software: A Case Study,” in Proc. of the 43rd Annual Conf. of the IEEE Industrial Electronics Society (IECON 2017), Beijing, China, October 29–November 1, 2017, pp. 5509–5514.Google Scholar
  18. 18.
    N. V. Pakulin, “Dynamics Verification of Hybrid Systems,” Nauch.-Tekhn. Vedomosti Sankt-Peterburgskogo Gos. Politekhn. Univ. Informatika. Telekommunikatsii. Upravlenie 193(2), 189–203 (2014).Google Scholar
  19. 19.
    O. G. Stepanov, ‘Method of Automated Verification of Automata Codes,” Nauch.-Tekhn. Vestnik Sankt-Peterburgskogo Gos. Univ. Informats. Tekhnol., Mekhaniki i Optiki, 8(53), Automata Programming, 221–229 (2008).Google Scholar
  20. 20.
    A. Platzer, “Logic and Compositional Verification of Hybrid Systems (Invited Tutorial),” in Proc. of the Intern. Conf. on Computer Aided Verification, Snowbird, USA, July 14–20, 2011, Vol. 1, pp. 28–43.MathSciNetCrossRefGoogle Scholar
  21. 21.
    F. Cassez and K. G. Larsen, “The Impressive Power of Stopwatches,” in Proc. of the 11th Intern. Conf. on Concurrency Theory (CONCUR 2000), Penssylvania, USA, August 22–25, 2000, Vol. 1877, pp. 138–152.MathSciNetzbMATHGoogle Scholar
  22. 22.
    T. A. Henzinger, “The Theory of Hybrid Automata,” in Proc. of the 9th Annual IEEE Symp. on Logic in Computer Science, New Brunswick, USA, July 27–30, 1996, pp. 278–292.Google Scholar
  23. 23.
    J. Koziorek, S. Ozana, V. Srovnal, and T. Docekalin, “Modeling and Simulations in Control Software Design,” in Analytic Methods in Systems and Software Testing, Ed. by R. S. Kenett, F. Ruggeri, and F. W. Faltin (John Wiley & Sons Ltd., Oxford, 2018), pp. 287–326). DOI: Scholar
  24. 24.
    R. Isermann, J. Schaffnit, and S. Sinsel, “Hardware-in-the-Loop Simulation for the Design and Testing of Engine-Control Systems,” Control Eng. Practice 7(5), 643–653 (1999).CrossRefGoogle Scholar
  25. 25.
    B. Xiao, M. Starke, D. King, et al., “Implementation of System Level Control and Communications in a Hardware-in-the-Loop Microgridtestbed,” in Proc. of the IEEE Power & Energy Society Innovative Smart Grid Technologies Conf., Minnesota, USA, September 6–9, 2016, Vol. 1, pp. 1–5.Google Scholar
  26. 26.
    T. V. Lyakh, V. E. Zyubin, and N. O. Garanina, “Automated Verification of Control Algorithms for Complex Technological Objects on Software Simulators,” Vestnik NGU. Ser. Informats. Tekhnol. 16(4), 85–94 (2018). DOI: Scholar
  27. 27.
    V. E. Zyubin, “Information Complexity Hypothesis: A Conceptual Framework for Reasoning on Pragmatics Issues,” in Proc. of the IEEE Intern. Conf. on Computational Technologies in Electrical and Electronics Engineering, Novosibirsk, Russia, July 21–25, 2008, Vol. 1, pp. 272–275. DOI: Scholar
  28. 28.
    P. G. Kovadlo, A. A. Lubkov, A. N. Bevzov, et al., “Automation System for the Large Solar Vacuum Telescope,” Avtometriya 52(2), 97–106 (2016) [Optoelectron., Instrum. Data Process. 52 (2), 187–195 (2016)].Google Scholar
  29. 29.
    J. Ouaknine and J. Worrell, “Some Recent Results in Metric Temporal Logic,” in Proc. of the 6th Intern. Conf. on Formal Modelling and Analysis of Timed Systems (FORMATS 2008), Saint Malo, France, September 15–17, 2008, Vol. 1, pp. 1–13. DOI: Scholar

Copyright information

© Allerton Press, Inc. 2019

Authors and Affiliations

  • T. V. Lyakh
    • 1
    • 2
  • V. E. Zyubin
    • 1
    • 2
    Email author
  • N. O. Garanina
    • 3
  1. 1.Institute of Automation and Electrometry, Siberian BranchRussian Academy of SciencesNovosibirskRussia
  2. 2.Novosibirsk State UniversityNovosibirskRussia
  3. 3.Ershov Institute of Informatics Systems, 630090, NovosibirskNovosibirskRussia

Personalised recommendations