Verification of the legOS scheduler using Uppaal. 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.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Brekling, Aske; Hansen, Michael R.; Madsen, Jan: Models and formal verification of multiprocessor system-on-chips (2008)
- Corradini, Flavio (ed.); Inverardi, Paola (ed.): MTCS 2000. Proceedings of the international satellite workshop on models for time-critical systems, State College, University Park, PA, USA, 26 August 2000 (2000)
- Halkjaer, Lone; Haervig, Karen; Ingolfsdottir, Anna: Verification of the legOS scheduler using Uppaal (2000)