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

research-article

Requirement specification and model-checking of a real-time scheduler implementation

Authors:

Khaoula Boukir,

Jean-Luc Béchennec,

Anne-Marie DéplancheAuthors Info & Claims

RTNS '20: Proceedings of the 28th International Conference on Real-Time Networks and Systems

Pages 89 - 99

https://doi.org/10.1145/3394810.3394817

Published: 12 June 2020 Publication History

Abstract

Implementing a new scheduler within a real-time operating system is challenging. The transition from a theoretical scheduling policy specification to a real platform implementation requires several constraints to be taken into account. Therefore, a verification process must support the implementation work to give it a level of confidence and validate its correctness.

In this paper, we present such a verification approach which is based on model-checking. It aims to identify subtle issues in our implementation of scheduling policies within an OSEK/VDX real-time operating system called Trampoline. As an example, the approach is conducted on elaborated models of an implemented G-EDF scheduler along with other OS components that contribute to the scheduling decision. Then, the verification is carried out by checking a set of relevant requirements which are identified based on the expected behavior of the scheduler as specified in the literature. This approach demonstrated its feasibility since potential issues are detected in our implementation.

References

[1]

Karine Altisen, Gregor Gößler, and Joseph Sifakis. 2002. Scheduler modeling based on the controller synthesis paradigm. Real-Time Systems 23, 1-2 (2002), 55--84.

Digital Library

[2]

Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Y Vardi, and Lenore D Zuck. 2005. Formal verification of backward compatibility of microcode. In International Conference on Computer Aided Verification. Springer, 185--198.

Digital Library

[3]

Theodore P Baker. 2010. What to make of multicore processors for reliable real-time systems?. In International Conference on Reliable Software Technologies. Springer, 1--18.

Digital Library

[4]

Luciano Porto Barreto and Gilles Muller. 2001. Bossa: a DSL framework for application-specific scheduling policies. Ph.D. Dissertation. INRIA.

[5]

Jean-Luc Béchennec, Mikael Briday, Sébastien Faucou, and Yvon Trinquet. 2006. Trampoline an open source implementation of the OSEK/VDX RTOS specification. In Emerging Technologies and Factory Automation, 2006. ETFA'06. IEEE Conference on. IEEE, 62--69.

[6]

Jean-Luc Béchennec, Olivier H. Roux, and Toussaint Tigori. 2018. Formal Model-Based Conformance Verification of an OSEK/VDX Compliant RTOS. In CODIt 2018-5th International Conference on Control, Decision and Information Technologies.

[7]

Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. 1996. UPPAAL---a tool suite for automatic verification of real-time systems. Hybrid Systems III (1996), 232--243.

[8]

Jean-Paul Bodeveix, Mamoun Filali, Julia L Lawall, and Gilles Muller. 2007. Automatic verification of bossa scheduler properties. Electronic Notes in Theoretical Computer Science 185 (2007), 17--32.

Digital Library

[9]

Khaoula Boukir, Jean-Luc Béchennec, and Anne-Marie Déplanche. 2017. Reducing the gap between theory and practice: towards A Proven Implementation of Global EDF in Trampoline. JRWRTC 2017 (2017), 9.

[10]

Khaoula Boukir, Jean-Luc Béchennec, and Anne-Marie Déplanche. 2018. Formal approach for a verified implementation of Global EDF in Trampoline. In Proceedings of the 26th International Conference on Real-Time Networks and Systems. ACM, 83--92.

Digital Library

[11]

John M Calandrino, Hennadiy Leontyev, Aaron Block, UmaMaheswari C Devi, and James H Anderson. 2006. LITMUSRT: A Testbed for Empirically Comparing Real-Time Multiprocessor Schedulers. In Real-Time Systems Symposium, 2006. RTSS'06. 27th IEEE International. IEEE, 111--126.

[12]

Alessio Carlini and Giorgio C Buttazzo. 2003. An efficient time representation for real-time embedded systems. In Proceedings of the 2003 ACM symposium on Applied computing. ACM, 705--712.

Digital Library

[13]

Felipe Cerqueira, Felix Stutz, and Björn B Brandenburg. 2016. PROSA: A case for readable mechanized schedulability analysis. In 2016 28th Euromicro Conference on Real-Time Systems (ECRTS). IEEE, 273--284.

[14]

Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Benjamin Werner, and Christine Paulin-Mohring. 1991. The COQ proof assistant user's guide: version 5.6. Ph.D. Dissertation. INRIA.

[15]

Dario Faggioli, Michael Trimarchi, Fabio Checconi, Marko Bertogna, and Antonio Mancina. 2009. An implementation of the earliest deadline first algorithm in Linux. In Proceedings of the 2009 ACM symposium on Applied Computing. ACM, 1984--1989.

Digital Library

[16]

Elena Fersman, Leonid Mokrushin, Paul Pettersson, and Wang Yi. 2006. Schedulability analysis of fixed-priority systems using timed automata. Theoretical Computer Science 354, 2 (2006), 301--317.

Digital Library

[17]

Limor Fix. 2008. Fifteen years of formal property verification in Intel. In 25 Years of Model Checking. Springer, 139--144.

[18]

Liang Gu, Alexander Vaynberg, Bryan Ford, Zhong Shao, and David Costanzo. 2011. CertiKOS: a certified kernel for secure cloud computing. In Proceedings of the Second Asia-Pacific Workshop on Systems. ACM, 3.

Digital Library

[19]

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. 2009. seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. ACM, 207--220.

Digital Library

[20]

Peng Li, Binoy Ravindran, Syed Suhaib, and Shahrooz Feizabadi. 2004. A formally verified application-level framework for real-time scheduling on posix real-time operating systems. IEEE Transactions on Software Engineering 30, 9 (2004), 613--629.

Digital Library

[21]

Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle/HOL: a proof assistant for higher-order logic. Vol. 2283. Springer Science & Business Media.

[22]

Evidence Srl. [n. d.]. Erika enterprise rtos. URL: http://www.evidence.eu.com ([n. d.]).

[23]

Kabland Toussaint Gautier Tigori, Jean-Luc Béchennec, Sébastien Faucou, and Olivier Henri Roux. 2017. Formal Model-Based Synthesis of Application-Specific Static RTOS. ACM Transactions on Embedded Computing Systems (TECS) 16, 4 (2017), 97.

[24]

Libor Waszniowski, Jan Krákora, and Zdeněk Hanzálek. 2009. Case study on distributed and fault tolerant system modeling based on timed automata. Journal of Systems and Software 82, 10 (2009), 1678--1694.

Digital Library

Cited By

Mousavi HEbnenasir AMahmoudzadeh E(2023)Formal Specification, Verification and Repair of Contiki’s SchedulerACM Transactions on Cyber-Physical Systems10.1145/36059487:4(1-28)Online publication date: 4-Jul-2023
https://dl.acm.org/doi/10.1145/3605948
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://doi.org/10.1007/s11219-023-09626-4
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

Index Terms

Requirement specification and model-checking of a real-time scheduler implementation
1. Computer systems organization
  1. Real-time systems
    1. Real-time operating systems
2. Theory of computation
  1. Logic
    1. Verification by model checking

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 approach for a verified implementation of Global EDF in Trampoline
RTNS '18: Proceedings of the 26th International Conference on Real-Time Networks and Systems

The technological progress in embedded system softwares increasingly requires the introduction of multiprocessor/multicore platforms for their considerable capacity and performances. This has introduced a large number of scientific researches in ...
A Survey of WCET Analysis of Real-Time Operating Systems
ICESS '09: Proceedings of the 2009 International Conference on Embedded Software and Systems

Timing correctness of hard real-time systems is guaranteed by schedulability analysis and worst-case execution time (WCET) analysis of programs. Traditional WCET analysis mainly deals with application programs and has achieved success in industry. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

RTNS '20: Proceedings of the 28th International Conference on Real-Time Networks and Systems

June 2020

177 pages

ISBN:9781450375931

DOI:10.1145/3394810

General Chairs:
Liliana Cucu-Grosjean
INRIA, Paris, France
,
Roberto Medina
INRIA, Paris, France
,
Program Chairs:
Sebastian Altmeyer
University of Augsburg, Germany
,
Jean-Luc Scharbarg
University of Toulouse, France

Copyright © 2020 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]

In-Cooperation

INRIA: INRIA Saclay Île-de-France

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 June 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

RTNS 2020

RTNS 2020: 28th International Conference on Real-Time Networks and Systems

June 9 - 10, 2020

Paris, France

Acceptance Rates

Overall Acceptance Rate 119 of 255 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
111
Total Downloads

Downloads (Last 12 months)23
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Mousavi HEbnenasir AMahmoudzadeh E(2023)Formal Specification, Verification and Repair of Contiki’s SchedulerACM Transactions on Cyber-Physical Systems10.1145/36059487:4(1-28)Online publication date: 4-Jul-2023
https://dl.acm.org/doi/10.1145/3605948
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://doi.org/10.1007/s11219-023-09626-4
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

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents