PhD Fellowship/Scholarship in Model Based Development of Formally Verified Digital Twins, Opportunity at Aarhus University, Aarhus C, Denmark

Job Overview

PhD Fellowship/Scholarship in Model Based Development of Formally Verified Digital Twins

Applications are invited for a PhD fellowship/scholarship at Graduate School of Technical Sciences, Aarhus University, Denmark, within the Electrical and Computer Engineering programme. The position is available from 1 April 2022 or later.    

Title:

Model Based Development of Formally Verified Digital Twins    

Research area and project description:

Modern Cyber-Physical Systems (CPS) are often deployed in environments that cannot be reproduced in laboratory conditions.
For example, an autonomous agricultural robot is expected to work under heterogeneous terrain, under varying meteorologic conditions, and in the proximity of other robots, humans, and/or wildlife.
When faced with unforeseen environments, the CPS must not fail or harm its surroundings.
During the development of the CPS, a large body of knowledge is generated in the form of models and experimental results, that is not being put to use after the CPS is deployed.

To leverage this data, every CPS will eventually come with its own Digital Twin (DT).
The DT is a virtual system that represents a CPS — its Physical Twin (PT) — that continuously collects data about the PT and its environment, correlates it with the models of the PT, and provides services such as anomaly detection and self-adaptation.
DTs will be open ended, that is, they will allow new services to be added by different stakeholders throughout the lifetime of the PT.
DT services and their interaction will be formally verified, and thus dependable.

The main goal of this PhD is to advance the state of the art in the way dependable DTs are synthesized from models used in the PT development.

This goal can be broken down into two objectives:

– O1: Synthesis of Formally Verified SotA DTs — to synthesize DTs with the most common services (state estimation, anomaly detection, and self-adaptation), with formal guarantees on behavior and compatibility between services.
– O2: Formally Verified Open-Ended DTs — To provide formal guarantees for open ended DTs, where new DT services can be added/discovered and may disrupt the PT.
This involves moving from static formal techniques to run-time verification, to assert service composition properties as new services are added.
Standard interfaces, contracts, and novel definitions of what constitutes safe behavior, will be defined.
This research will be applied to O1’s case studies and to an agricultural robot fleet (a system of systems, with a DT composed of other DTs).    

Qualifications and specific competences:

Model-based Design and System Engineering
Application of Formal Methods and Software Verification Techniques (Model checking, dataflow analysis, etc)
Distributed system programming (message passing systems, REST, etc.)
Numerical methods for simulation of differential equations

Place of employment and place of work:

The place of employment is Aarhus University, and the place of work is Department of Electrical and Computer Engineering, Finlandsgade 22, 8200 Aarhus N, Denmark.   

Contacts:
Applicants seeking further information are invited to contact: 

• Professor Peter Gorm Larsen, pgl@ece.au.dk  
• Postdoc Cláudio Ângelo Gonçalves Gomes, claudio.gomes@ece.au.dk 

How to apply:
Please follow this link to submit your application. Application deadline is 31 January 2022 23:59. Preferred starting date is 1 April 2022.

For information about application requirements and mandatory attachments, please see our application guide.

Shortlisting will be used, which means that the evaluation committee only will evaluate the most relevant applications.

All interested candidates are encouraged to apply, regardless of their personal background. Aarhus University’s ambition is to be an attractive and inspiring workplace for all and to foster a culture in which each individual has opportunities to thrive, achieve and develop. We view equality and diversity as assets, and we welcome all applicants.

APPLY NOW