Formal Modeling and Analysis of Advanced Scheduling Features in an Avionics RTOS

  • Darren Cofer
  • Murali Rangarajan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2491)


Integrated modular avionics (IMA) architectures found in modern aircraft contain applications of different criticalities executing on the same CPU. The execution of these applications must be scheduled so that they do not inadvertently consume CPU time that has been budgeted for other applications. This scheduling function may be performed by a real-time operating system (RTOS) that provides time partitioning guarantees. The large number of variables affecting application execution interleavings makes it difficult and costly to verify time partitioning by traditional means.

This paper reports on our efforts to use model checking techniques to verify time partitioning properties in an avionics RTOS. Our modeling and analysis is based on the actual embedded software so as to capture the implementation details of the scheduler. We focus here on several advanced scheduling features of the RTOS that are particularly challenging to verify.


Application Program Interface Linear Temporal Logic Main Thread Interrupt Service Routine Tick Time 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Design Description Document for the Digital Engine Operating System. Honeywell specification no. PS7022409.Google Scholar
  2. 2.
    Binns, Pam: A robust high-performance time partitioning algorithm: the Digital Engine Operating System (Deos) approach. 20th Digital Avionics System Conference (2001)Google Scholar
  3. 3.
    Binns, Pam: Incremental rate monotonic scheduling for improved control system performance. IEEE Real-Time Applications Symposium (1997)Google Scholar
  4. 4.
    Binns, Pam: Scheduling slack in MetaH. IEEE Real-Time Systems Symposium work-in-progress session (1996)Google Scholar
  5. 5.
    Holzmann, G: The model checker Spin. IEEE Transactions on Software Engineering 23 (1997) 279–295CrossRefGoogle Scholar
  6. 6.
    Lehoczky, J. P. and S. Ramos-Thuel: An optimal algorithm for scheduling aperiodic tasks in fixed-priority preemptive systems. IEEE Real-Time Systems Symposium (1992)Google Scholar
  7. 7.
    Liu, C. L. and J. W. Leyland: Scheduling Algorithms for Multiprogramming in a Hard Real Time Environment. Journal of the ACM 20 (1973) 46–61zbMATHCrossRefGoogle Scholar
  8. 8.
    Pasareanu, Corina S., Deos Kernel: Environment Modeling using LTL Assumptions. NASA Ames Technical Report NASA-ARC-IC-2000-196 (2000)Google Scholar
  9. 9.
    Penix, J., W. Visser, E. Engstrom, A. Larson, and N. Weininger: Verification of Time Partitioning in the Deos Scheduler Kernel. International Conf. on Software Engineering (2000)Google Scholar
  10. 10.
    Penix, J., W. Visser, E. Engstrom, A. Larson, and N. Weininger: Translation and Verification of the Deos Scheduling Kernel. Technical report, NASA Ames Research Center/Honeywell Technology Center (1999)Google Scholar
  11. 11.
    RTCA/DO-178B: Software Considerations in Airborne Systems and Equipment Certification. RTCA, Inc., Washington DC (1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Darren Cofer
    • 1
  • Murali Rangarajan
    • 1
  1. 1.Honeywell LaboratoriesMinneapolis

Personalised recommendations