Skip to main content
SpringerLink
Log in

Towards Reusable Formal Models for Custom Real-Time Operating Systems

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13487))

  • 376 Accesses

Abstract

In embedded systems, the execution semantics of the real-time operating system (RTOS), which is responsible for scheduling and timely execution of concurrent processes, is crucial for the correctness of the overall system. However, existing approaches for the formal verification of embedded systems typically abstract from the RTOS completely, or provide a detailed and synthesizable formal model of the RTOS. While the former may lead to unsafe systems, the latter is not compatible with industrial design processes. In this paper, we present an approach for reusable abstract formal models that can be configured for custom RTOS. Our key idea is to formally capture common execution mechanisms of RTOS like preemptive scheduling and event synchronization abstractly in configurable timed automata models. These abstract formal models can be configured for a concrete custom RTOS, and they can be combined into a formal system model together with a concrete application. Our reusable models significantly reduce the manual effort of defining a formal model that captures concurrency and real-time behavior together with the functionality of an application. The resulting formal model enables analysis, verification, and graphical simulation. We validate our approach by formalizing and analyzing a rescue robot application running the custom open source RTOS EV3RT.

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

Access this chapter

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 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.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

Institutional subscriptions

References

  1. Abdeddaïm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 113–126. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46002-0_9

    Chapter  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)

    Article  MathSciNet  Google Scholar 

  3. Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7

    Chapter  Google Scholar 

  4. Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL — a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0020949

    Chapter  Google Scholar 

  5. Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27755-2_3

    Chapter  MATH  Google Scholar 

  6. Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16

    Chapter  Google Scholar 

  7. Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102–110. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_7

    Chapter  Google Scholar 

  8. Béchennec, J.L., Roux, O.H., Tigori, T.: Formal model-based conformance verification of an OSEK/VDX compliant RTOS. In: 2018 5th International Conference on Control, Decision and Information Technologies (CoDIT), pp. 628–634 (2018). https://doi.org/10.1109/CoDIT.2018.8394813

  9. Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_16

    Chapter  Google Scholar 

  10. Deifel, H.P., Göttlinger, M., Milius, S., Schröder, L., Dietrich, C., Lohmann, D.: Automatic verification of application-tailored OSEK kernels. In: IEEE (2017)

    Google Scholar 

  11. EV3RT Project: EV3RT (2019). https://ev3rt-git.github.io/about/

  12. Han, P., Zhai, Z., Nielsen, B., Nyman, U.: Model-based optimization of ARINC-653 partition scheduling. Int. J. Softw. Tools Technol. Transf. 23(5), 721–740 (2021)

    Article  Google Scholar 

  13. Herber, P., Fellmuth, J., Glesner, S.: Model checking systemc designs using timed automata. In: IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2008, pp. 131–136. ACM (2008). https://doi.org/10.1145/1450135.1450166

  14. Huang, Y., Zhao, Y., Zhu, L., Li, Q., Zhu, H., Shi, J.: Modeling and verifying the code-level OSEK/VDX operating system with CSP. In: 2011 Fifth International Conference on Theoretical Aspects of Software Engineering, pp. 142–149. IEEE (2011)

    Google Scholar 

  15. Klein, G., et al.: sel4: formal verification of an OS kernel. In: ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009. ACM (2009). https://doi.org/10.1145/1629575.1629596

  16. Laplante, P.A., et al.: Real-Time Systems Design And Analysis. Wiley, New York (2004)

    Book  Google Scholar 

  17. OSEK: ISO 17356–3:2005 Road vehicles - Open interface for embedded automotive applications - Part 3: OSEK/VDX Operating System (OS). International Organization for Standardization (2005)

    Google Scholar 

  18. Shi, J., He, J., Zhu, H., Fang, H., Huang, Y., Zhang, X.: ORIENTAIS: Formal verified OSEK/VDX real-time operating system. In: 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems. pp. 293–301. IEEE (2012)

    Google Scholar 

  19. Tigori, K.T.G., Béchennec, J.L., Faucou, S., Roux, O.H.: Formal model-based synthesis of application-specific static rtos. ACM Trans. Embed. Comput. Syst. 16(4), 1–25 (017). https://doi.org/10.1145/3015777

  20. TOPPERS Project: Toyohashi open platform for embedded real-time systems. https://www.toppers.jp/en/project.html

  21. TRON: \(\mu \)ITRON4.0 Specification (2007). https://www.tron.org/wp-content/themes/dp-magjam/pdf/specifications/en_US/TEF024-S001-04.03.00_en.pdf. Accessed 02 Sep 2021

  22. Vu, D.H., Chiba, Y., Yatake, K., Aoki, T.: Verifying OSEK/VDX OS design using its formal specification. In: 2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 81–88. IEEE (2016)

    Google Scholar 

  23. Waszniowski, L., Hanzálek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39–65 (2008)

    Article  Google Scholar 

  24. Zhang, H., Aoki, T., Chiba, Y.: Verifying OSEK/VDX applications: a sequentialization-based model checking approach. IEICE Trans. Inf. Sys. 98(10), 1765–1776 (2015)

    Article  Google Scholar 

  25. Zhang, H., Aoki, T., Lin, H.H., Zhang, M., Chiba, Y., Yatake, K.: SMT-based bounded model checking for OSEK/VDX applications. In: 2013 20th Asia-Pacific Software Engineering Conference (APSEC), vol. 1, pp. 307–314. IEEE (2013)

    Google Scholar 

  26. Zhang, H., Li, G., Cheng, Z., Xue, J.: Verifying OSEK/VDX automotive applications: a spin-based model checking approach. Softw. Test. Verif. Reliab. 28(3), e1662 (2018)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Julius Adelt, Julian Gebker & Paula Herber

Authors
  1. Julius Adelt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Julian Gebker
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paula Herber
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Julius Adelt or Paula Herber .

Editor information

Editors and Affiliations

  1. Eindhoven University of Technology, Eindhoven, The Netherlands

    Jan Friso Groote

  2. University of Twente, Enschede, The Netherlands

    Marieke Huisman

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Adelt, J., Gebker, J., Herber, P. (2022). Towards Reusable Formal Models for Custom Real-Time Operating Systems. In: Groote, J.F., Huisman, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2022. Lecture Notes in Computer Science, vol 13487. Springer, Cham. https://doi.org/10.1007/978-3-031-15008-1_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-15008-1_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-15007-4

  • Online ISBN: 978-3-031-15008-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation