|Abstract : Nowadays, many computer systems are embedded and used to control physical elements. These systems are often critical (any failure can have catastrophic consequences). Safe and efficient design of those systems is a notoriously difficult task because their behaviour is hard to predict with a high degree of preciseness as it depends on quantitative parameters, such as time, energy consumptions or other metrics measuring quality of service. Computer-aided design tools, based on formal methods, is thus highly advocated for those systems.
Current formal methods consist of verification and synthesis techniques. The former allow to prove that the system respects some control objective while the latter build automatically a control programme that guarantees the control objective. These methods are general-purpose, and are focussed on designing safe systems. However, the results of the literature are mainly of qualitative nature: most of them allow neither to model quantitative aspects with sufficient precision, nor to perform quantitative analysis.
The PhD candidate will investigate new quantitative models, and new algorithms to analyse those models. They will allow to express with increased preciseness, the quantitative aspects in the behaviours and properties of embedded control systems; and to perform quantitative analysis of those models.|