Nothing Special   »   [go: up one dir, main page]
Skip to main content

Advertisement

Springer Nature Link
Log in

Formal verification process of the compliance of a multicore AUTOSAR OS

  • Published:
Software Quality Journal Aims and scope Submit manuscript

Abstract

\(\mathrm{A}\small{\mathrm{UTOSAR}}\) conformance testing is based on requirements verification. This work focuses on multicore operating system (OS) requirements, of which there are eighty. We present a semi-automated formal process to check multicore OS compliance using High-Level Colored Time Petri Net and model-checking methods. To apply our approach, we use the Roméo tool to build an operating system model called Trampoline that conforms to the AUTOSAR OS specification. Each requirement of the multicore OS is formalized by an observer modeled by a Petri net to evaluate compliance. The observers evolve according to the operating system evolution without altering its behavior to check whether the specification is true or false. The approach ensures that the operating system model respects the multicore specification of \(\mathrm{A}\small{\mathrm{UTOSAR}}\) OS.

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
$34.99 /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 excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15

Similar content being viewed by others

Data availability

The authors declare that the data used in this work is available on the Trampoline repository under a free license: https://github.com/TrampolineRTOS/trampoline/tree/master/tests/functional.

Notes

  1. https://www.autosar.org/fileadmin/user_upload/standards/classic/4-2/AUTOSAR_SWS_OS.pdf

  2. https://github.com/TrampolineRTOS/trampoline

  3. OSEK Implementation Language.

  4. In the example in this section and in the examples that follow we present models designed with the tool Roméo. In this tool, \(\$any\) is used instead of any in guards and updates for syntactic reasons but both have the same meaning.

  5. The two double dots (::) are equivalent to an arc in the model. This syntax proposed by Roméo allows a clear and better organization of the Petri subnet in different XML files, which form only one Petri net. Thus a function call is ensured by the following syntax: the XML file name of the Petri subnet:: the place name to which we want to send a token.

  6. WCET corresponds to the worst execution time of the code between two service calls, and BCET to the best case execution time of the code between two service calls.

  7. https://github.com/TrampolineRTOS/GTL/blob/master/documentation/GTL.pdf

  8. They are available in the Trampoline repository: https://github.com/TrampolineRTOS/trampoline/tree/master/tests/functional

  9. \(mc\_alarms\_s1\) to \(mc\_taskTermination\_s2\) are modeled and verified except for \(mc\_taskTermination\_s1\), \(mc\_schedtables\_s1\), and \(mc\_autostart\_s3\) that are in progress: https://github.com/TrampolineRTOS/trampoline/tree/master/tests/functional

References

  • Alur, R., Courcoubetis, C., & Dill, D. (1993). Model-checking in dense real-time. Information and Computation, 104, 2–34.

    Article  MathSciNet  MATH  Google Scholar 

  • AUTOSAR. (2010, November). AUTOSAR BSW and RTE Conformance Test Specification Part 2: Process Overview (Technical Report). AUTOSAR Consortium.

  • AUTOSAR GbR. (2009). Specification of operating system.

  • AUTOSAR. (2014, March). Specification of operating system (Technical Report ). AUTOSAR Consortium.

  • Béchennec, J.-L., Roux, O. H., & Tigori, T. (2018, April). Formal model-based conformance verification of an OSEK/VDX compliant RTOS. In International Conference on Control, Decision and Information Technologies (CODIT 2018).

  • Boucheneb, H., Gardey, G., & Roux, O. H. (2009). TCTL model checking of time Petri nets. Journal of Logic and Computation, 19, 1509–1540.

    Article  MathSciNet  MATH  Google Scholar 

  • Boukir, K., Béchennec, J.-L., & Déplanche, A.-M. (2020). Requirement specification and model-checking of a real-time scheduler implementation. In Proceedings of the 28th International Conference on Real-Time Networks and Systems RTNS 2020 (pp. 89–99). New York, NY, USA: Association for Computing Machinery.

  • Boyer, M., & Diaz, M. (2001). Multiple enabledness of transitions in Petri nets with time. In Proceedings of the 9th International Workshop on Petri Nets and Performance Models, PNPM 2001, Aachen, Germany, September 11-14, 2001 (pp. 219–228). IEEE Computer Society.

  • Chen, J., & Aoki, T. (2011). Conformance testing for OSEK/VDX operating system using model checking. In Software Engineering Conference (APSEC), 18th Asia Pacific (pp. 274–281).

  • Choi, Y. (2011). Safety analysis of Trampoline OS using model checking: An experience report. In 2011 IEEE 22nd International Symposium on Software Reliability Engineering (pp. 200–209).

  • Clarke, E. M., Filkorn, T., & Jha, S. (1993). Exploiting symmetry in temporal logic model checking. In Proceedings of the 5th International Conference on Computer Aided Verification CAV ’93 (pp. 450–462). Berlin, Heidelberg: Springer-Verlag.

  • Cook, S. A. (1971). The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing STOC ’71 (pp. 151–158). New York, NY, USA: Association for Computing Machinery.

  • Fang, L., Kitamura, T., Do, T. B. N., & Ohsaki, H. (2012). Formal model-based test for AUTOSAR multicore RTOS. In 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation (pp. 251–259).

  • Gadelha, M. R., Monteiro, F. R., Morse, J., Cordeiro, L. C., Fischer, B., & Nicole, D. A. (2018). ESBMC 5.0: An industrial-strength C model checker. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (pp. 888–891). New York, NY, USA: Association for Computing Machinery.

  • Group, O. et al. (2005). OSEK/VDK operating system specification. http://www.osek-vdx.org

  • Haur, I., Béchennec, J.-L., & Roux, O. H. (2021). Formal schedulability analysis based on multi-core RTOS model. In 29th International Conference on Real-Time Networks and Systems RTNS’2021 (pp. 216–225). Association for Computing Machinery: New York, NY, USA.

  • Haur, I., Béchennec, J., & Roux, O. H. (2022a). High-level Colored Time Petri Nets for true concurrency modeling in real-time software. In 8th International Conference on Control, Decision and Information Technologies, CoDIT 2022, Istanbul, Turkey, May 17-20, 2022 (pp. 21–26). IEEE.

  • Haur, I., Béchennec, J., & Roux, O. H. (2022b). High-level Colored Time Petri Nets for true concurrency modeling in real-time software. In International Conference on Control, Decision and Information Technologies (CODIT 2022). Istanbul, Turkey.

  • Hillah, L., Kordon, F., Petrucci, L., & Trèves, N. (2006). Pn standardisation: A survey. In Formal Techniques for Networked and Distributed Systems - FORTE 2006 (pp. 307–322). volume 4229 of Lecture Notes in Computer Science. Springer.

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

  • John, D. (1998). OSEK/VDX conformance testing - MODISTARC. IET Conference Proceedings, (pp. 7–7(1)).

  • Kindler, E., & Petrucci, L. (2009). A framework for the definition of variants of high-level Petri nets. In Proceedings of the Tenth Workshop and Tutorial on Practical Use of Coloured Petri Nets and CPN Tools (CPN ’09) (pp. 121–137).

  • Lime, D., Roux, O. H., Seidner, C., & Traonouez, L.-M. (2009). Romeo: A parametric model-checker for Petri nets with stopwatches. In S. Kowalewski, & A. Philippou (Eds.), 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009) (pp. 54–57). York, United Kingdom: Springer volume 5505 of Lecture Notes in Computer Science.

  • Murata, T. (1989). Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77, 541–580.

    Article  Google Scholar 

  • OSEK Group (1999). OSEK/VDX OS test plan version 2.0.

  • Peng, Y., Huang, Y., Su, T., & Guo, J. (2013). Modeling and verification of AUTOSAR OS and EMS application. In 2013 International Symposium on Theoretical Aspects of Software Engineering (pp. 37–44).

  • Roux, O. H., & Lime, D. (2000). Roméo: formal verification and synthesis for parametric timed systems. http://romeo.rts-software.org/?page_id=3.

  • Tigori, K. T. G., Béchennec, J.-L., Faucou, S., & Roux, O. H. (2017). Formal model-based synthesis of application-specific static RTOS. ACM Transactions on Embedded Computing Systems (TECS), 16, 1–25.

    Article  Google Scholar 

  • Trinh, L. K., Chiba, Y., & Aoki, T. (2018). Formalization and verification of AUTOSAR OS standard’s memory protection. In 2018 International Symposium on Theoretical Aspects of Software Engineering (TASE) (pp. 68–75).

  • Yan, R., & Guo, J. (2019). Timing modeling and analysis for AUTOSAR schedule tables. In 2019 IEEE 19th International Symposium on High Assurance Systems Engineering (HASE) (pp. 123–130).

Download references

Funding

This research work has been partly funded by ANRT and Huawei Technologies France under doctoral contract CIFRE2019-0798.

Author information

Author notes

  1. Imane Haur, Jean-Luc Béchennec, and Olivier H. Roux contribute equally to this work.

Authors and Affiliations

  1. Laboratoire des sciences du numérique de Nantes (LS2N), 1 Rue de la Noë, Nantes, 44300, France

    Imane Haur

  2. Huawei Paris Research center, 20 Quai du Point du Jour, Boulogne-Billancourt, 92100, France

    Imane Haur, Jean-Luc Béchennec & Olivier H. Roux

Authors
  1. Imane Haur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-Luc Béchennec
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Olivier H. Roux
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Imane Haur.

Ethics declarations

Conflict of interest

The authors declare that they have no conflict of interest.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Appendix. Requirements corresponding to multicore OS

Appendix. Requirements corresponding to multicore OS

See Table 3

Table 3 Subset of \(\mathrm{A}\small{\mathrm{UTOSAR}}\) OS requirements related to multicore
Full size table

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Haur, I., Béchennec, JL. & H. Roux, O. Formal verification process of the compliance of a multicore AUTOSAR OS. Software Qual J 31, 497–531 (2023). https://doi.org/10.1007/s11219-023-09626-4

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11219-023-09626-4

Keywords

Search

Navigation