More Web Proxy on the site http://driver.im/

announcement

Formal Model-Based Synthesis of Application-Specific Static RTOS

Authors:

Kabland Toussaint Gautier Tigori,

Jean-Luc Béchennec,

Sébastien Faucou,

Olivier Henri RouxAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 16, Issue 4

Article No.: 97, Pages 1 - 25

https://doi.org/10.1145/3015777

Published: 11 May 2017 Publication History

Abstract

In an embedded system, the specialization of the code of the real-time operating system (RTOS) according to the requirements of the application allows one to remove unused services and other sources of dead code from the binary program. The typical specialization process is based on a mix of precompiler macros and build scripts, both of which are known for being sources of errors.

In this article, we present a new model-based approach to the design of application-specific RTOS. Starting with finite state models describing the RTOS and the application requirements, the set of blocks in the RTOS code actually used by the application is automatically computed. This set is used to build an application-specific RTOS model. This model is fed into a code generator to produce the source code of an application-specific RTOS. It is also used to carry on model-based validations and verifications, including the formal verification that the specialization process did not introduce unwanted behaviors or suppress expected ones.

To demonstrate the feasibility of this approach, it is applied to specialize Trampoline, an open-source implementation of the AUTOSAR OS standard, to an industrial case study from the automotive domain.

References

[1]

Thomas E. Anderson. 1992. The case for application-specific operating systems. In Workshop on Workstation Operating Systems (WWOS’92).

[2]

Luciano Porto Barreto and Gilles Muller. 2002. Bossa: A language-based approach to the design of real-time schedulers. In 10th International Conference on Real-Time Systems (RTS’02), 19--31.

[3]

Jean-Luc Béchennec, Mikaël Briday, Sébastien Faucou, and Yvon Trinquet. 2006. Trampoline an open source implementation of the OSEK/VDX RTOS specification. In IEEE International Conference on Emerging Technologies and Factory Automation (ETFA’06).

[4]

Carsten Boke, Marcelo Gotz, Tales Heimfarth, D. El Kebbe, F. J. Rammig, and S. Rips. 2003. (Re-) configurable real-time operating systems and their applications. In IEEE International Workshop on Object-Oriented Real-Time Dependable Systems (WORDS’03). 148--155.

[5]

Ron Brightwell, Rolf Riesen, Keith Underwood, Trammell B. Hudson, Patrick Bridges, and Arthur B. Maccabe. 2003. A performance comparison of Linux and a lightweight kernel. In IEEE International Conference on Cluster Computing. IEEE, 251--258.

[6]

Jiang Chen and Toshiaki Aoki. 2011. Conformance testing for OSEK/VDX operating system using model checking. In 18th Asia Pacific Software Engineering Conference (APSEC’11). 274--281.

Digital Library

[7]

Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2012. Frama-c. In Software Engineering and Formal Methods. Springer.

Digital Library

[8]

Christian Dietrich, Martin Hoffman, and Daniel Lohmann. 2015. Back to the roots: Implementing the RTOS as a specialized state machine. In 11th Annual Workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT’15). 7--12.

[9]

Peter Druschel. 1993. Efficient support for incremental customization of OS services. In International Workshop on Object Orientation in Operating Systems.

[10]

Jason Hill, Robert Szewczyk, Alec Woo, Seth Hollar, David Culler, and Kristofer Pister. 2000. System architecture directions for networked sensors. In ACM SIGOPS Operating Systems Review, Vol. 34. ACM, 93--104.

Digital Library

[11]

D. John. 1998. OSEK/VDX conformance testing—MODISTARC. IET Conference Proceedings (January 1998), 7--7(1). http://digital-library.theiet.org/content/conferences/10.1049/ic_19981078.

[12]

Keith Krueger, David Loftesness, Amin Vahdat, and Thomas Anderson. 1993. Tools for the Development of Application-Specific Virtual Memory Management. Vol. 28. ACM.

Digital Library

[13]

Anil Kurmus, Reinhard Tartler, Daniela Dorneanu, Bernhard Heinloth, Valentin Rothberg, Andreas Ruprecht, Wolfgang Schröder-Preikschat, Daniel Lohmann, and Rüdiger Kapitza. 2013. Attack surface metrics and automated compile-time OS kernel tailoring. In 20th Network and Distributed System Security Symposium (NDSS’13).

[14]

Daniel Lohmann, Wanja Hofer, Wolfgang Schröder-Preikschat, Jochen Streicher, and Olaf Spinczyk. 2009. CiAO: An aspect-oriented operating-system family for resource-constrained embedded systems. In USENIX Annual Technical Conference.

[15]

Gregory Malecha, Ashish Gehani, and Natarajan Shankar. 2015. Automated software winnowing. In 30th Annual ACM Symposium on Applied Computing (SAC’15). ACM, 1504--1511.

Digital Library

[16]

OSEK Group et al. 1999a. OSEK/VDX OS Test Plan Version 2.0.

[17]

OSEK Group et al. 1999b. OSEK/VDX OS Test Procedure Version 2.0.

[18]

OSEK Group et al. 2005. OSEK/VDX Operating System Specification.

[19]

Kabland Toussaint Gautier Tigori, Jean-Luc Bechennec, and Olivier H. Roux. 2015. Formal synthesis of optimal RTOS (Best paper award). In Proceedings of the 12th IEEE International Conference on Embedded Software and Systems. IEEE, New York, 977--983.

[20]

Martin Treiber, Ansgar Hennecke, and Dirk Helbing. 2000. Congested traffic states in empirical observations and microscopic simulations. Phys. Rev. E 62, 2 (Aug. 2000), 1805--1824.

[21]

Kenro Yatake and Toshiaki Aoki. 2012. Model checking of OSEK/VDX OS design model based on environment modeling. In International Colloquium on Theoretical Aspects of Computing. Springer, 183--197.

Cited By

Adelt JGebker JHerber P(2024)Reusable formal models for concurrency and communication in custom real-time operating systemsInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00743-426:2(229-245)Online publication date: 20-Feb-2024
https://doi.org/10.1007/s10009-024-00743-4
Haur IBéchennec JH. Roux O(2023)Formal verification process of the compliance of a multicore AUTOSAR OSSoftware Quality Journal10.1007/s11219-023-09626-431:2(497-531)Online publication date: 25-May-2023
https://dl.acm.org/doi/10.1007/s11219-023-09626-4
Haur IBéchennec JRoux O(2022)Formal Verification of the Inter-core Synchronization of a Multi-core RTOS KernelFormal Methods and Software Engineering10.1007/978-3-031-17244-1_9(140-155)Online publication date: 24-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-17244-1_9
Show More Cited By

Index Terms

Formal Model-Based Synthesis of Application-Specific Static RTOS
1. Computer systems organization
  1. Embedded and cyber-physical systems
    1. Embedded systems
      1. Embedded software
2. Computing methodologies
  1. Modeling and simulation
    1. Model development and analysis
      1. Model verification and validation

Recommendations

Formal schedulability analysis based on multi-core RTOS model
RTNS '21: Proceedings of the 29th International Conference on Real-Time Networks and Systems

Verification of real-time application schedulability is usually performed using a very abstract representation of the system which poorly supports inter-task dependencies. This paper presents the use of model-checking techniques to check the ...
Formal Synthesis of Optimal RTOS
HPCC-CSS-ICESS '15: Proceedings of the 2015 IEEE 17th International Conference on High Performance Computing and Communications, 2015 IEEE 7th International Symposium on Cyberspace Safety and Security, and 2015 IEEE 12th International Conf on Embedded Software and Systems

The adaptation of an operating system to an application is often needed to optimize the embedded code. Adaptation consists in removing the unneeded operating systems services and the dead code according to applications requirements. The resulting ...
The Formal Design Model of a Real-Time Operating System RTOS+: Static and Dynamic Behaviors

A real-time operating system RTOS provides a platform for the design and implementation of a wide range of applications in real-time systems, embedded systems, and mission-critical systems. This paper presents a formal design model for a general RTOS ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 16, Issue 4

Special Issue on Secure and Fault-Tolerant Embedded Computing and Regular Papers

November 2017

614 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/3092956

Editor:
Sandeep K. Shukla
Indian Institute of Technology, India

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 11 May 2017

Accepted: 01 October 2016

Revised: 01 August 2016

Received: 01 October 2015

Published in TECS Volume 16, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Announcement
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
330
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)1

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Adelt JGebker JHerber P(2024)Reusable formal models for concurrency and communication in custom real-time operating systemsInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00743-426:2(229-245)Online publication date: 20-Feb-2024
https://doi.org/10.1007/s10009-024-00743-4
Haur IBéchennec JH. Roux O(2023)Formal verification process of the compliance of a multicore AUTOSAR OSSoftware Quality Journal10.1007/s11219-023-09626-431:2(497-531)Online publication date: 25-May-2023
https://dl.acm.org/doi/10.1007/s11219-023-09626-4
Haur IBéchennec JRoux O(2022)Formal Verification of the Inter-core Synchronization of a Multi-core RTOS KernelFormal Methods and Software Engineering10.1007/978-3-031-17244-1_9(140-155)Online publication date: 24-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-17244-1_9
Adelt JGebker JHerber P(2022)Towards Reusable Formal Models for Custom Real-Time Operating SystemsFormal Methods for Industrial Critical Systems10.1007/978-3-031-15008-1_6(69-85)Online publication date: 5-Sep-2022
https://doi.org/10.1007/978-3-031-15008-1_6
Haur IBéchennec JRoux O(2021)Formal schedulability analysis based on multi-core RTOS modelProceedings of the 29th International Conference on Real-Time Networks and Systems10.1145/3453417.3453437(216-225)Online publication date: 7-Apr-2021
https://dl.acm.org/doi/10.1145/3453417.3453437
Lencioni LLoubach DSaotome O(2021)A Methodology for Customization of a Real-Time Operating System for Embedded Systems2021 IEEE XXVIII International Conference on Electronics, Electrical Engineering and Computing (INTERCON)10.1109/INTERCON52678.2021.9532670(1-4)Online publication date: 5-Aug-2021
https://doi.org/10.1109/INTERCON52678.2021.9532670
Boukir KBéchennec JDéplanche AOuhammou YRidouard FGrolleau EJan MBehnam M(2018)Formal approach for a verified implementation of Global EDF in TrampolineProceedings of the 26th International Conference on Real-Time Networks and Systems10.1145/3273905.3273926(83-92)Online publication date: 10-Oct-2018
https://dl.acm.org/doi/10.1145/3273905.3273926
Deifel HGöttlinger MMilius SSchröder LDietrich CLohmann DStewart DWeissenbacher G(2017)Automatic verification of application-tailored OSEK kernelsProceedings of the 17th Conference on Formal Methods in Computer-Aided Design10.5555/3168451.3168493(196-203)Online publication date: 2-Oct-2017
https://dl.acm.org/doi/10.5555/3168451.3168493
Deifel HGottlinger MMilius SSchroder LDietrich CLohmann D(2017)Automatic verification of application-tailored OSEK kernels2017 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2017.8102260(196-203)Online publication date: Oct-2017
https://doi.org/10.23919/FMCAD.2017.8102260

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents