Supervisory Controller Synthesis for Safe Software Adaptation

Today's software systems need to adapt their behavior due to the changes in their operational environments and user requirements. To this end, an adaptive software performs a sequence of adaptations at runtime. Correctness of the behavior of an adaptive software system during dynamic adaptation is an important challenge along the way to realize correct adaptive systems. In this research, we model adaptation as a supervisory control problem and synthesize a controller that guides the behavior of a software system during adaptation. The system during adaptation is modeled using a graph transition system and properties to be enforced are specified using an automaton. To ensure correctness, we then synthesize a controller that imposes constraints on the system during adaptation.