Title
High-level frameworks for the specification and verification of scheduling problems.
Abstract
Over the years, schedulability of Cyber-Physical Systems (CPS) has mainly been performed by analytical methods. These techniques are known to be effective but limited to a few classes of scheduling policies. In a series of recent work, we have shown that schedulability analysis of CPS could be performed with a model-based approach and extensions of verification tools such as UPPAAL. One of our main contributions has been to show that such models are flexible enough to embed various types of scheduling policies, which goes beyond those in the scope of analytical tools. However, the specification of scheduling problems with model-based approaches requires a substantial modeling effort, and a deep understanding of the techniques employed in order to understand their results. In this paper we propose simplicity-driven high-level specification and verification frameworks for various scheduling problems. These frameworks consist of graphical and user-friendly languages for describing scheduling problems. The high-level specifications are then automatically translated to formal models, and results are transformed back into the comprehensible model view. To construct these frameworks we exploit a meta-modeling approach based on the tool generator Cinco . Additionally we propose in this paper two new techniques for scheduling analysis. The first performs runtime monitoring using the CUSUM algorithm to detect alarming change in the system. The second performs optimization using efficient statistical techniques. We illustrate our frameworks and techniques on two case studies.
Year
DOI
Venue
2018
10.1007/s10009-017-0466-1
STTT
Keywords
Field
DocType
Scheduling, Energy, Hierarchical scheduling, Formal methods, Statistical model-checking, High-level language, Meta-modeling
CUSUM,Programming language,Software engineering,Computer science,Scheduling (computing),Statistical model checking,Theoretical computer science,Two-level scheduling,Real-time computing,Exploit,High-level programming language,Formal methods
Journal
Volume
Issue
ISSN
20
4
1433-2779
Citations 
PageRank 
References 
0
0.34
25
Authors
7
Name
Order
Citations
PageRank
Mounir Chadli100.34
Jin Hyun Kim2376.75
Kim G. Larsen33922254.03
Axel Legay42982181.47
Stefan Naujokat517413.39
Bernhard Steffen601.69
Louis-Marie Traonouez724318.50