Context

Mutiprocessor real-time systems have become ubiquitous in the past few years. Some of them (e.g., automated plane and unmanned systems control, driverless cars) are critical in the sense that no error must occur. Testing these systems can possibly detect the presence of bugs, but not guarantee their absence. It is necessary to use formal methods such as model checking [BK08] so as to prove formally the correctness of a system. Designing a correct scheduling for a set of tasks to be executed by several processors is crucial for the system safety. Such systems are characterized by a set of timing constants, such as the read-ing period of a sensor on an unmanned aircraft system, or the minimal or maximal time needed by a satellite to compute some result. Although numerous techniques to verify a system for one set of constants exist, formally verifying the system for numerous values of these constants can require a very long time, or even infinite if one aims at verifying dense sets of values. It is therefore interesting to reason in a parametric manner, by considering that these con-stants are unknown, i.e., parameters, and synthesize a constraint on these parameters guarantee-ing that there exists a correct scheduling for the system. Several techniques have been proposed to solve this problem [AHV93, AS13], in particular in the setting of parametric schedulability anal