Formal Modeling and Analysis of Advanced Scheduling Features in an Avionics RTOS
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.
KeywordsApplication Program Interface Linear Temporal Logic Main Thread Interrupt Service Routine Tick Time
Unable to display preview. Download preview PDF.
- 1.Design Description Document for the Digital Engine Operating System. Honeywell specification no. PS7022409.Google Scholar
- 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.Binns, Pam: Incremental rate monotonic scheduling for improved control system performance. IEEE Real-Time Applications Symposium (1997)Google Scholar
- 4.Binns, Pam: Scheduling slack in MetaH. IEEE Real-Time Systems Symposium work-in-progress session (1996)Google Scholar
- 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
- 8.Pasareanu, Corina S., Deos Kernel: Environment Modeling using LTL Assumptions. NASA Ames Technical Report NASA-ARC-IC-2000-196 (2000)Google Scholar
- 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.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.RTCA/DO-178B: Software Considerations in Airborne Systems and Equipment Certification. RTCA, Inc., Washington DC (1992)Google Scholar