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.
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.