Affordable Access

Publisher Website

Verification of the legOS Scheduler using Uppaal

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
39
Issue
3
Identifiers
DOI: 10.1016/s1571-0661(05)80752-2
Disciplines
  • Design

Abstract

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.

There are no comments yet on this publication. Be the first to share your thoughts.