On Formalization of Semantics of Real-Time and Cyber-Physical Systems

  • Ievgen Ivanov
  • Taras Panchenko
  • Mykola Nikitchenko
  • Fabunmi Sunmade
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 754)


In the article we describe theoretical foundations of a framework for formalizing semantics of real-time and cyber-physical systems in interactive theorem proving environments. The framework is based on viewing a system as a predicate on system’s executions which are modeled as functions from the continuous time domain to a set of states. We consider how it can be applied to the safety verification problems. The proposed framework may be useful in verification of software for real-time and cyber-physical systems and of the corresponding development tools.


Formal methods Real-time systems Cyber-physical systems Formal semantics Proof assistant 


  1. 1.
    Sifakis, J.: Modeling real-time systems – challenges and work directions. In: Proceedings First International Workshop on Embedded Software, LNCS 2211, pp. 373–389. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Burns, A., Wellings, A.: Real Time Systems and Programming Languages, 3rd edn. Addison Wesley Longman, Reading (2001). 611 p.Google Scholar
  3. 3.
    Kirsch, C.M.: Principles of real-time programming. In: proceedings Second International Workshop on Embedded Software, LNCS 2491, pp. 61–75. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Merz, S., Navet, N. (eds.): Modeling and Verification of Real-Time Systems: Formalisms and Software Tools. INRIA Lorraine, Nancy (2008). 400 p.Google Scholar
  5. 5.
    Furia, C.A., Mandrioli, D., Morzenti, A., Rossi, M.: Modeling time in computing: a taxonomy and a comparative survey. ACM Comput. Surv. 42, 1–59 (2010)CrossRefGoogle Scholar
  6. 6.
    Panchenko, T., Ivanov, I.: A formal proof of properties of a presentation system using Isabelle. In: 2017 IEEE First Ukraine Conference on Electrical and Computer Engineering UKRCON, pp. 1155–1160 (2017)Google Scholar
  7. 7.
    Polishchuk, N., Kartavov, M., Panchenko, T.: Safety property proof using correctness proof methodology in IPCL. In: Proceedings of the 5th International Scientific Conference “Theoretical and Applied Aspects of Cybernetics”, Bukrek, Kyiv, pp. 37–44 (2015)Google Scholar
  8. 8.
    Kartavov, M., Panchenko, T., Polishchuk, N.: Infosoft e-detailing system total correctness proof in IPCL. Bull. Taras Shevchenko National Univ. Kyiv Ser. Phys. Math. Sci. 3, 80–83 (2015). (in Ukrainian)Google Scholar
  9. 9.
    Kartavov, M., Panchenko, T., Polishchuk, N.: Properties proof method in IPCL application to real-world system correctness proof. Int. J. Inf. Models Anal. 4(2), 142–155 (2015). ITHEA, Sofia, BulgariaGoogle Scholar
  10. 10.
    Geuvers, H.: Proof assistants: history, ideas and future. Sadhana 34, 3–25 (2009)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Paulson, L.C.: Isabelle: A Generic Theorem Prover; with Contributions by Tobias Nipkow, Lecture Notes in Computer Science, vol. 828. Springer, Heidelberg (1994). 321 p.Google Scholar
  12. 12.
    Henties, T., Hunt, J., Locke, D., Nilsen, K., Schoeberl, M., Vitek, J.: Java for Safety-Critical Applications. Electronic Notes in Theoretical Computer Science (2009). 11 p.
  13. 13.
    Nikitchenko, M., Shkilniak, S.: Applied Logic. Publishing House of Taras Shevchenko National University of Kyiv, Kyiv (2013) 278 p. (in Ukrainian)Google Scholar
  14. 14.
    Nikitchenko, M., Shkilniak, S.: Algebras and logics of partial quasiary predicates. Algebra Discrete Math. 23(2), 263–278 (2017)MathSciNetzbMATHGoogle Scholar
  15. 15.
    Gladun, A., Rogushina, J.: Use of semantic web technologies and multilinguistic thesauri for knowledge-based access to biomedical resources. Int. J. Intell. Syst. Appl. (IJISA) 4(1), 11–20 (2012). Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2019

Authors and Affiliations

  • Ievgen Ivanov
    • 1
  • Taras Panchenko
    • 1
  • Mykola Nikitchenko
    • 1
  • Fabunmi Sunmade
    • 1
  1. 1.Taras Shevchenko National University of KyivKyivUkraine

Personalised recommendations