Supervisor:
In control software, inputs and outputs depend in complex ways on each other and their own previous state. Classical functional specifications thus do not exist; instead, control software is specified by behavioural models, which, when run, simulate the evolution of outputs. Self-explanations that are useful to (software or human) clients of a control software must reduce its complexity but at the same time also capture its overall behaviour. In addition, they must detect when they are outdated and then adapt appropriately. In this project we develop methods for self-repair of timed automata and provide a decision procedure for accepting or rejecting new explanations.
Desirable background and expertise: Expertise in temporal logics and in model checking of timed automata; experience with formal modeling of engineering applications; advanced programming skills.