[Master 2R 2014-2015] Performance Evaluation for Embedded Systems using Formal Methods

 Scientific Context

Modern embedded systems design must deal with more and more constraints in several domains: systems are increasingly complex, but have to be manufactured at low cost, and with a short life cycle. They have to be reliable, not only functionally (i.e. computations produce the expected results), but also with respect to performance (i.e. computations produce the results on time). For such “real-time systems”, it is not sufficient to optimize the code to make it compute as fast as possible, it is also important to be able to provide bounds on the possible execution times.

For multimedia applications, for example, it is important to be able to ensure that applications can encode/decode a stream at the speed at which it is received. More importantly, in critical systems like automotive or avionics, missing a deadline can cause severe damages, hence some formal guarantees on execution time is required. Also, embedded systems are often constrained in memory, hence unbounded buffers cannot be used as a communication medium between different components. For example, in a typical data-flow oriented application like a JPEG encoder, if one block (say, the DCT block) issues large amount of output in a small period of time (i.e. a burst), that the next block (the quantization in our example) cannot consume immediately, the data have to be stored in a buffer, which may be of limited size. The size needed for the buffer depends both on how fast the first block can produce data, and how fast the next one can consume them.

Given the short life cycle due to time-to-market pressure in the industry, it is no longer possible to wait for the physical prototypes to validate the decisions on the conception of a system, it is necessary to use a model (i.e. an abstract representation of the system, but not yet an implementation) as early as possible in the design flow. To use these models to validate real-time systems, several approaches are possible:

Simulation. The most fine-grained models of embedded systems are expressed as programs, written in usual languages like C or C++ (possibly enriched with libraries like SystemC). These programs can be executed to simulate the complete behavior of a system, and obtain some performance information. Just like testing, these approaches can give good confidence in the correctness of the system, but no formal guarantees.

Formal Models and State-Space Exploration. An alternative to common programming languages is to model the system with formal languages (like Lustre, Uppaal, …), that essentially describe state-machines. These languages are less expressive than general-purpose languages, but allow formal reasoning and exhaustive state-space exploration. For example, model-checking or abstract interpretation can be used to verify formally and automatically properties like “the system never takes more than X units of time to process an event”. These analysis provide formal guarantees, but encounter the “state-explosion” problem on large systems: analysis can take huge amount of time and memory, and may not be applied as-is on large systems in practice.

Modular Performance Analysis and Real-Time Calculus. One solution to the state-explosion problem is to perform formal analysis only on small parts (i.e. components) of a system at a time. This category of approach is called “compositional analysis”, or “modular analysis”. An existing approach is the Real-Time Calculus (RTC), which represents the interface of components with curves. Simple components can be analyzed with purely analytical methods (i.e. solving equations mathematically with efficient algorithms), while more complex components can be analyzed with the above mentioned abstract interpretation or model-checking techniques. Preliminary case studies performed in Verimag and by other teams like the ETH Zurich showed that this approach is interesting, but limited because of the low expressivity of RTC.

 Subject

The goal of the internship is to investigate a new modular performance analysis approach. This analysis should provide formal bounds on performance properties like maximum end-to-end delay of an event in a system, maximum buffer size, etc. Instead of describing component interfaces with curves, a state-based formalism (counter automata, or possibly timed-automata) should be used.

This subject involves three steps:

  • Define a formalism, based on the notion of automata, allowing the representation of an event flow,
  • Define the way to compute the abstraction of an output flow produced by a module, as a function of the information available on its input, and a model of the module’s behavior,
  • Implement these algorithms and apply them on several examples. Examples can include existing case studies like the 2-CPU/3-tasks system published in Emsoft09, or the FlexRay (used in automotive) analysis published in DAC07 and EUC2010.

The expected work includes a bibliographical study on modeling of embedded systems for performance evaluation (simulation models, RTC), concrete experimentation (and therefore an implementation of the proposed algorithms), and a comparison with RTC. This subject makes a bridge between programming for simulation and formal study of the same systems. It includes theoretical and practical points. Don’t hesitate to come and discuss the subject with us!

 Working environment

The student will work within the SYNCHRONE team of the Verimag laboratory.

Continuing with a Ph.D thesis on a related topic is possible.

 Contacts

Karine Altisen,
Matthieu Moy