WP-A. An architecture description framework.
Work has proceeded on the development of the behavioral theory of location graphs, a new computational model for dynamic software architectures with sharing and encapsulation. Specifically, we have developed encodings in location graphs of several formalisms, including BIP, the pi-calculus and the Kell calculus, and shown that any GSOS language can be encoded as an instance of the location graph framework. We have developed a strong bisimulation theory for location graphs, which we proved to be sound with respect to a (strong) notion of contextual equivalence for location graphs.
WP-B. Online optimization methods for dynamic reconfiguration systems.
During the first year, we made a contribution on the online energy optimization for a finite or infinite set of jobs with real-time constraints executed on a single processor. The objective is to find, at each (discrete) time instant, the speed of the processor such that the total energy (in the case of a finite set of jobs) or the average energy (in the case of an infinite set of jobs) is minimized. The processor is assumed to be equipped with DVFS capability (dynamic voltage and frequency scaling). Each job is characterized by a tuple (A, C, D) which are respectively its arrival time, its WCET (worst case execution time), and its relative deadline. Our goal is to benefit from the statistical knowledge of the job arrivals in order to optimize the energy consumption compared to the existing solutions.
We use a Markov Decision Process (MDP) approach to compute the optimal online speed scaling policy. In the finite case we use a Dynamic Programming algorithm, while in the infinite case we use a Value Iteration algorithm. The numerical experiments show that our solution performs well when compared with the off-line optimal solution and out-performs on-line solutions oblivious to statistical information on the job arrivals.
Some problems remain. First, the state space of our MPD is very large. The impact of this size on the computation time of the MDP is acceptable because it is computed offline. But the impact on the embedded memory is problematic. We are investigating on the one hand discretization techniques and on the other hand latency masking techniques to alleviate this problem.
Second, to compute our MDP, we have assumed that the statistical characteristics of the jobs are known. In practice this is not the case. We will therefore investigate reinforcement learning algorithm (e.g., Q-learning) to overcome this.
WP-C. A formal framework for real-time analysis in Coq.
This work builds on top of and enriches the Prosa library. More information is available here.
Two schedulability analyses for uniprocessor systems have been formalized and mechanically verified in Coq for:
- sporadic task sets scheduled according to the Time Division Multiple Access (TDMA) policy.
- periodic task sets with offsets scheduled according to the Fixed Priority Preemptive (FPP) policy.
Firstly, the analysis for TDMA has served to familiarize ourselves with the Prosa library.
Secondly, schedulability analysis in presence of offsets is a non-trivial problem with a high computational complexity. In contrast to the traditional (offset oblivious) analysis, many scenarios must be tested and compared to identify which one represents the worst-case scenario. We have formalized and proved in Coq the basic analysis presented by Tindell. This has allowed us to: (1) underline implicit assumptions made in Tindell’s informal analysis; (2) ease the generalization of the verified analysis; (3) generate a certifier and an analyzer. We are investigating these two tools in terms of computational complexity and implementation effort, in order to provide a good solution to guarantee schedulability of industrial systems.
In parallel, we have worked on a Coq formalization of Typical Worst Case Analysis (TWCA). We aim to provide certified generic results for weakly hard real time systems in the form of (m,k) guarantees (a task may miss at most m deadlines out of k consecutive activations). So far, we have adapted the initial TWCA for arbitrary schedulers. The proof relies on a practical definition of the concept of busy window which amounts to being able to perform a local response time analysis. We provide such an instantiation for Fixed Priority Preemptive (FPP) schedulers as in the original paper. Future work includes making the state of the art TWCA suitable for formal proofs, exploring more complex systems (e.g., bounded buffers) and providing instantiations of our results for other scheduling policies.
