Formal-methods support for runtime adaptation in role-based systems

Abstract: With rising dependence on technology, it is getting ever more important to design systems for long-time deployment. This makes systems able to perform acceptably in a number of different situations and environments. This is why there is an ongoing effort to design self-adaptive systems, systems that are able to adapt to diverse situations without human input.

One particular challenge in this area consists of defining a proper behavior, in order to reach certain long term goals.

While most approaches use heuristics to define self-adaptation behavior, they are not able to bring ideal results in most cases, and can not be easily understood by human operators anymore.

Formal methods like Model Checking have a distinctive advantage in these two fields. Given a close approximation of the system, these techniques can be used to define theoretically ideal strategies for given objectives, while keeping them in a form still understandable by humans.

In my thesis, I research what advantage such formal methods, especially model checking based ones, can have on the varying aspects of self-adaptation in feature and role based systems. This ranges from verification of such systems at design time, to utilizing the advantage of formal methods in runtime.