Multiprocessor Scheduling Systems
We have implemented with Cinco a high-level framework that allows to design a two-layer multiprocessor scheduling system. The first layer models the hardware platform, with a scheduling system composed of real-time tasks and CPUs. Each processor has its own scheduling mechanism and is parameterized by its frequency. The frequency defines the speed of the processor and its energy consumption when running.
The second layer models the application that is composed of a set of actions. Applications running in a cyber-physical system are unlimited, with no fixed design. To demonstrate the use of our framework we consider a simple design methodology for writing applications with stochastic behaviour.
The link between the two layers is implemented by a mapping from actions to tasks, that specify for each action of the application on which task it is intended to run. In our current framework this mapping is static and determined before an execution. However we would like to evaluate several mappings in order to optimize the system performances.
This design allows a separation of concerns that facilitates the verification of formal properties:
- Scheduling properties are verified on the platform layer only.
- Logical properties of the application are verified on the application layer only.
- Energy consumption or execution time properties need to consider both layer simultaneously.
We implemented a program that performs change detection using the CUSUM algorithm. It first generates the Uppaal model and it will run the CUSUM algorithm on this model several times. For each execution, it generates with Uppaal SMC a simulation trace that corresponds to the total length of the experiment. It then splits this execution into a set of samples and it analyses each sample to evaluate the query and update the CUSUM ratio. If the value of ratio exceeds the sensitivity threshold it outputs a detection with the detection time in a pop-up window.
The specification files to generate the tool are available for download. The archive file can simply be imported “as existing project into workspace” (via File/Import/General) in Cinco version 0.6.
Uppaal 4.1.19 is needed to run formal verification on the models. It is available at the Uppaal website.
For questions regarding the multiprocessor scheduling tool and project, please contact Chadli Mounir or Louis-Marie Traonouez.
