À la Une

Soutenance de thèse Stefan Klikovits

SK_1000.jpg  

M. Stefan Klikovits soutiendra en anglais, en vue de l'obtention du grade de docteur ès sciences mention informatique de la Faculté des sciences de l'Université de Genève, sa thèse intitulée:

A Domain-Specific Language Approach to Hybrid CPS Modelling

Date: Jeudi 13 juin 2019 à 10h30

Lieu: CUI / Battelle bâtiment A, auditoire rez-de-chaussée

 

Jury:

  • Prof. Didier Buchs (Directeur, Université de Genève)
  • Prof. Gilles Falquet (Université de Genève)
  • Prof. Joachim Denil (Université d'Anvers)
  • Dr. Moussa Amrani (Université de Namur)
  • Prof. Manuel Wimmer (Université de Linz)

Résumé:

The recent advent of cyber-physical systems (CPS) in end-user applications extends the need for sophisticated model creation, simulation and system verification from classical systems engineering domains to new application areas. Since CPS such as smart homes and office automation seamlessly integrate technology into everyday life, their safety and correctness become paramount. The intricacy of modelling these systems stems from the merging of two opposing system views: While flows of physical energy and resources are mostly described using mathematical methods such as differential equations, engineered applications are usually best expressed using automata and similar discrete formalisms. Many tools that support such hybrid models aim to maximise versatility and application areas, thereby widening the distance between software and target domain. This introduces complexity and configuration effort and increases the risk for errors not directly related to the system itself.

This thesis explores the use of domain-specific languages (DSLs) to bridge the gap between systems and models. It describes the creation of the CREST, a DSL dedicated to the combined modelling of physical resources and engineered behaviour. The language offers architectural concepts such as hierarchical system composition and typed ports, reactive dataflow aspects that assert a synchronous model behaviour, continuous variable evolution and support for non-deterministic systems. CREST is implemented as crestdsl, a Python-based, internal DSL that allows efficient modelling and simulation.

The research further describes the application of formal verification on CREST models. This advanced use case is explored from theoretical and practical points of view. Additionally, it has been implemented in crestdsl proving its viability. The positive result of the approach highlights the capabilities of CREST, the practicability of the hybrid DSL modelling approach and confirms their effectiveness.

SK_CREST.png