Automatic Verification of Control Software in Cyber-Physical Systems with Plant Simulators
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.
Keywordsverification control software cyber-physical systems plant simulators process-oriented programming
Unable to display preview. Download preview PDF.
- 1.A. D. Zakrevskii, Parallel Algorithms of Logic Control (Editorial URSS, Moscow, 2003).Google Scholar
- 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: https://doi.org/10.1109/SIBCON.2007371297.
- 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: https://doi.org/10.1109/EDM.2016.7538711.
- 8.M. Samek and P. Montgomery, “State Oriented Programming,” Embedded Syst. Programm. 13(8), 22–43 (2000).Google Scholar
- 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: https://doi.org/10.1109/SIBCON.2013.6693595.
- 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.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.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: https://doi.org/10.3233/978-1-61499-900-3-515.Google Scholar
- 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.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.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.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.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.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
- 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.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: https://doi.org/10.1002/9781119357056.ch12.CrossRefGoogle Scholar
- 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.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: https://doi.org/10.25205/1818-7900-2018-16-4-85-94.CrossRefGoogle Scholar
- 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: https://doi.org/10.1109/SIBIRCON.2008.4602608.Google Scholar
- 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.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: https://doi.org/10.1007/978-3-540-85778-5_1.zbMATHGoogle Scholar