Schedulability Analysis Using Uppaal: Herschel-Planck Case Study

Schedulability Analysis Using Uppaal: Herschel-Planck case study, Marius Mikučionis, Kim Guldstrand Larsen, Jacob Illum Rasmussen, Brian Nielsen, Arne Skou, Palm Steen Ulrik, Jan Storbank Pedersen, Poul Hougaard. Proceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation - Volume Part II (ISOLA 2010), October 2010, Springer-Verlag, ISBN 3-642-16560-5, 978-3-642-16560-3. [DOI] [bib] [pre-print] [slides]

Abstract

We propose a modeling framework for performing schedulability analysis by using UPPAAL real-time model-checker. The framework is inspired by a case study where schedulability analysis of a satellite system is performed. The framework assumes a single CPU hardware where a fixed priority preemptive scheduler is used in a combination with two resource sharing protocols and in addition voluntary task suspension is considered. The contributions include the modeling framework, its application on an industrial case study and a comparison of results with classical response time analysis.