Title
Verification of the legOS Scheduler using Uppaal
Abstract
This article concentrates on the scheduler in the operating system legOS. LegOS is an open source embedded operating system for the Lego Mindstorms ® system. The scheduler in legOS practices starvation of lower priority threads. In this article the validity of starvation problems is proven through tests of the scheduler and through an Uppaal model of the scheduler wherein the starvation is verified. A new scheduler is designed and modeled in Uppaal. This Uppaal model is used to verify that starvation is no longer a problem in the new design. The new design is implemented in a new scheduler and tests are performed to show that the problem with starvation is no longer present.
Year
DOI
Venue
2000
10.1016/S1571-0661(05)80752-2
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
operating system
Embedded operating system,Computer science,Thread (computing),Operating system,Embedded system
Journal
Volume
Issue
ISSN
39
3
Electronic Notes in Theoretical Computer Science
Citations 
PageRank 
References 
2
0.40
1
Authors
3
Name
Order
Citations
PageRank
Lone Halkjaer120.40
Karen Haervi220.40
Anna Ingolfsdottir3394.89