Quantitative models for verification and synthesis of correct software

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.
Promoteur/Supervisor : Prof. Geeraerts Gilles
Email : gigeerae@ulb.ac.be
Site Web/Web site :
Centre de recherche/Research center : Formal methods and verification
Faculté/Faculty : Faculty of Sciences/Faculté des Sciences
Ecole doctorale/Graduate Colleges : Science/Sciences
Ecole doctorale thématique/Graduate School (French Only):

Retour à la liste principale/Back to main list