Dedicative Verification of Reflex Programs | Programming and Computer Software
Skip to main content
Springer Nature Link
Log in

Dedicative Verification of Reflex Programs

  • Published:
Programming and Computer Software Aims and scope Submit manuscript

Abstract

This paper presents a new two-step verification method for control software. The novelty of the method is that it reduces the verification of the temporal properties of a control program to the deductive verification of an imperative program in the Hoare style, which explicitly models the time and history of the control program. The method is applied to programs written in the Reflex language, a domain-specific extension of C developed as an alternative to the languages of the IEC 61131-3 standard. Reflex is a process-oriented language that describes control programs in terms of communicating processes controlled by operator events, including the events generated by operations on discrete time intervals. At the first step, an annotated Reflex program is translated into an equivalent annotated imperative program on a bounded subset of C, which is extended with the logical type bool, supertype value (which combines the values that can return Reflex functions and operators), and statement havoc x (which assigns an arbitrary value to the variable x). At the second step, the resulting imperative program undergoes deductive verification. The proposed method is illustrated by the example of deductive verification of a Reflex program that controls a hand dryer. The example includes the original Reflex program, a set of requirements, the resulting annotated program, the correctness conditions generated, and results of verifying these conditions in Z3py, an interface to the Z3 SMT solver implemented in Python.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1.

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

REFERENCES

  1. Blanke, M., Kinnaert, M., Lunze, J., and Staroswiecki, M., Diagnosis and Fault-Tolerant Control, Springer, 2006, 2nd ed.

    MATH  Google Scholar 

  2. IEC 61131-3: Programmable controllers, Part 3: Programming languages, Rev. 2.0, International Electrotechnical Commission Std., 2003.

  3. Basile, F., Chiacchio, P., and Gerbasio, D., On the implementation of industrial automation systems based on PLC, IEEE Trans. Autom. Sci. Eng., 2013, vol. 4, no. 10, pp. 990–1003.

    Article  Google Scholar 

  4. Thramboulidis, K. and Frey, G., An MDD process for IEC 61131-based industrial automation systems, Proc. 16th IEEE Int. Conf. Emerging Technologies and Factory Automation (ETFA), Toulouse, France, 2011, pp. 1–8.

  5. IEC 61499: Function blocks for industrial process measurement and control systems, Parts 1–4, Rev. 1.0, International Electrotechnical Commission Std., 2004–2005.

  6. Wagner, F., Schmuki, R., Wagner, T., and Wolstenholme, P., Modeling Software with Finite State Machines, Boston: Auerbach, 2006.

    Book  Google Scholar 

  7. Samek, M., Practical UML Statecharts in C/C++: Event-Driven Programming for Embedded Systems, Oxford: Newnes, 2009, 2nd ed.

    Google Scholar 

  8. Control Technology Corporation, QuickBuilderTM reference guide, 2018. https://controltechnologycorp.com/docs/QuickBuilder_Ref.pdf. Accessed January 20, 2019.

  9. Zyubin, V.E., Hyper-automaton: A model of control algorithms, Proc. IEEE Int. Sib. Conf. Control and Communications (SIBCON), Tomsk, Russia, 2007, pp. 51–57.

  10. Hoare, C.A.R., Communicating Sequential Processes, Prentice-Hall, 1985.

    MATH  Google Scholar 

  11. Harel, D., Statecharts: A visual formalism for complex systems, Sci. Comput. Program., 1987, vol. 8, no. 3, pp. 231–274.

    Article  MathSciNet  Google Scholar 

  12. Lynch, N. and Tuttle, M., An introduction to input/output automata, CWI Quarterly, 1989, vol. 2, no. 3, pp. 219–246.

    MathSciNet  MATH  Google Scholar 

  13. Berry, G., The foundations of Esterel, Proof, Language, and Interaction: Essays in Honour of Robin Milner, MIT Press, 2000, pp. 425–454.

    Google Scholar 

  14. Henzinger, T.A., The theory of hybrid automata, Verification of Digital and Hybrid Systems, NATO ASI Series (Series F: Computer and Systems Sciences), Inan, M.K. and Kurshan, R.P., Eds., Springer, 2000, vol. 170, pp. 265–292.

    Google Scholar 

  15. Milner, R., Communication and Concurrency, New Jersey: Prentice Hall, 1989.

    MATH  Google Scholar 

  16. Kaynar, D.K., Lynch, N., Segala, R., and Vaandrager, F., Timed I/O automata: A mathematical framework for modeling and analyzing real-time systems, Proc. 24th IEEE Int. Real-Time Systems Symp. (RTSS), Cancun, Mexico, 2003, pp. 166–177.

  17. Kof, L. and Schätz, B., Combining aspects of reactive systems, Proc. Andrei Ershov 5th Int. Conf. Perspectives of System Informatics, Novosibirsk, 2003, pp. 239–243.

  18. Zyubin, V., SPARM language as a means for programming microcontrollers, Optoelectron., Instrum., Data Process., 1996, vol. 2, no. 7, pp. 36–44.

    Google Scholar 

  19. Liakh, T.V., Rozov, A.S., and Zyubin, V.E., Reflex language: A practical notation for cyber-physical systems, Syst. Inf., 2018, vol. 12, no. 6, pp. 85–104.

    Google Scholar 

  20. Rozov, A.S. and Zyubin, V.E., Process-oriented programming language for MCU-based automation, Proc. IEEE Int. Sib. Conf. Control and Communications, Tomsk, Russia, 2013, pp. 1–4.

  21. Bulavskij, D., Zyubin, V., Karlson, N., Krivoruchko, V., and Mironov, V., An automated control system for a silicon single-crystal growth furnace, Optoelectron., Instrum., Data Process., 1996, vol. 2, no. 5, pp. 25–30.

    Google Scholar 

  22. Travis, J. and Kring, J., LabVIEW for Everyone: Graphical Programming Made Easy and Fun, New Jersey: Prentice Hall, 2006, 3rd ed.

    Google Scholar 

  23. Zyubin, V., Using process-oriented programming in LabVIEW, Proc. 2nd IASTED Int. Multi-Conf. “Automation, Control, and Information Technology: Control, Diagnostics, and Automation,” Novosibirsk, 2010, pp. 35–41.

  24. Randell, B., Software engineering techniques, Report on a conference sponsored by the NATO Science Committee, Brussels, Scientific Affairs Division, NATO, Rome, Italy, 1970, p. 16.

    Google Scholar 

  25. Z3 API in Python. https://ericpony.github.io/z3py-tutorial/guide-examples.htm. Accessed January 20, 2019.

  26. Moura, L. and Bjørner, N., Z3: An efficient SMT solver, Proc. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lect. Notes Comput. Sci., 2008, vol. 4963, pp. 337–340.

  27. Anureev, I.S., Garanina, N.O., Liakh, T.V., Rozov, A.S., Zyubin, V.E., and Gorlatch, S., Two-step deductive verification of control software using Reflex, Proc. A.P. Ershov Informatics Conference (PSI), Novosibirsk, Russia, Lect. Notes Comput. Sci., 2019, vol. 11964, pp. 50–63.

  28. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., and Leino, K.R.M., Boogie: A modular reusable verifier for object-oriented programs, Proc. 4th Int. Conf. Formal Methods for Components and Objects, Lect. Notes Comput. Sci., 2005, vol. 4111, pp. 364–387.

  29. FramaC homepage. https://frama-c.com.

  30. Spark Pro homepage. https://www.adacore.com/ sparkpro.

  31. The KeY project homepage. https://www.key-project.org.

  32. Dafny homepage. https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness.

  33. Dijkstra, E.W. and Scholten, C.S., Predicate Calculus and Program Semantics, Springer, 1990.

    Book  Google Scholar 

  34. Nepomniaschy, V., Anureev, I., Mikhailov, I., and Promsky, A., Towards verification of C programs: C‑light language and its formal semantics, Program. Comput. Software, 2002, vol. 28, no. 6, pp. 314–323.

    Article  MathSciNet  Google Scholar 

  35. Nepomniaschy, V., Anureev, I., and Promsky, A., Towards verification of C programs: Axiomatic semantics of the C-kernel language, Program. Comput. Software, 2003, vol. 29, no. 6, pp. 338–350.

    Article  MathSciNet  Google Scholar 

  36. Garanina, N., Zyubin, V., Lyakh, V., and Gorlatch, S., An ontology of specification patterns for verification of concurrent systems, New Trends in Intelligent Software Methodologies, Tools, and Techniques (Proc. 17th Int. Conf. SoMeT), Series: Frontiers in Artificial Intelligence and Applications, Amsterdam: IOS Press, 2018, pp. 515–528.

  37. ACL2 homepage. http://www.cs.utexas.edu/users/ moore/acl2.

  38. Anureev, I.S., Operational ontological approach to formal programming language specification, Program. Comput. Software, 2009, vol. 35, no. 1, pp. 35–42.

    Article  MathSciNet  Google Scholar 

Download references

Funding

This work was supported by the State budget of the Russian Federation (IAE project no. AAAA-A19-119120290056-0), Russian Foundation for Basic Research (project nos. 17-07-01600 and 20-01-00541), and German Federal Ministry of Education and Research (project HPC2SE).

Author information

Authors and Affiliations

  1. Ershov Institute of Informatics Systems, Siberian Branch, Russian Academy of Sciences, pr. Akademika Lavrent’eva 6, 630090, Novosibirsk, Russia

    I. S. Anureev & N. O. Garanina

  2. Institute of Automation and Electrometry, Siberian Branch, Russian Academy of Sciences, pr. Akademika Koptyuga 1, 630090, Novosibirsk, Russia

    I. S. Anureev, N. O. Garanina, T. V. Lyakh, A. S. Rozov & V. E. Zyubin

  3. University of Münster, Einsteinstr. 62, 48149, Münster, Germany

    S. P. Gorlatch

Authors
  1. I. S. Anureev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. N. O. Garanina
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. T. V. Lyakh
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. A. S. Rozov
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. V. E. Zyubin
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. S. P. Gorlatch
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to I. S. Anureev, N. O. Garanina, T. V. Lyakh, A. S. Rozov, V. E. Zyubin or S. P. Gorlatch.

Additional information

Translated by Yu. Kornienko

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Anureev, I.S., Garanina, N.O., Lyakh, T.V. et al. Dedicative Verification of Reflex Programs. Program Comput Soft 46, 261–272 (2020). https://doi.org/10.1134/S0361768820040027

Download citation

  • Received:

  • Revised:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1134/S0361768820040027

Search

Navigation