Skip to main content
SpringerLink
Log in
Book cover

International Conference on Computer Science, Engineering and Education Applications

ICCSEEA 2018: Advances in Computer Science for Engineering and Education pp 213–223Cite as

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

  • Conference paper
  • First Online:

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 754))

Abstract

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.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   169.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  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)

    Chapter  Google Scholar 

  2. Burns, A., Wellings, A.: Real Time Systems and Programming Languages, 3rd edn. Addison Wesley Longman, Reading (2001). 611 p.

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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. 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. 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. 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, Bulgaria

    Google Scholar 

  10. Geuvers, H.: Proof assistants: history, ideas and future. Sadhana 34, 3–25 (2009)

    Article  MathSciNet  Google Scholar 

  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. 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. http://www.jopdesign.com/doc/safecert2009.pdf

  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. Nikitchenko, M., Shkilniak, S.: Algebras and logics of partial quasiary predicates. Algebra Discrete Math. 23(2), 263–278 (2017)

    MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.5815/ijisa.2012.01.02

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Taras Shevchenko National University of Kyiv, Kyiv, Ukraine

    Ievgen Ivanov, Taras Panchenko, Mykola Nikitchenko & Fabunmi Sunmade

Authors
  1. Ievgen Ivanov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Taras Panchenko
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mykola Nikitchenko
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Fabunmi Sunmade
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Taras Panchenko .

Editor information

Editors and Affiliations

  1. School of Educational Information Technology, Central China Normal University, Wuhan, Hubei, China

    Zhengbing Hu

  2. Mechanical Engineering Research Institute, Russian Academy of Sciences, Moscow, Russia

    Sergey Petoukhov

  3. Faculty of Applied Mathematics, National Technical University of Ukraine “Igor Sikorsky Kiev Polytechnic Institute”, Kiev, Ukraine

    Ivan Dychka

  4. Halmos College of Natural Sciences and Oceanography, Nova Southeastern University, Ft. Lauderdale, Florida, USA

    Matthew He

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ivanov, I., Panchenko, T., Nikitchenko, M., Sunmade, F. (2019). On Formalization of Semantics of Real-Time and Cyber-Physical Systems. In: Hu, Z., Petoukhov, S., Dychka, I., He, M. (eds) Advances in Computer Science for Engineering and Education. ICCSEEA 2018. Advances in Intelligent Systems and Computing, vol 754. Springer, Cham. https://doi.org/10.1007/978-3-319-91008-6_22

Download citation

Publish with us

Policies and ethics

Search

Navigation