Transformational Supervisor Synthesis for Evolving Systems

Supervisory controller synthesis is a means to compute correct-by-construction controllers for discrete event systems. As these systems and their requirements evolve over time, an updated supervisor needs to be computed each time an adaptation takes place. We consider the case that a supervisor has been synthesized for a given model, after which this model is (slightly) adapted. We investigate how we can make use of the previous synthesis result, in order to more efficiently compute the supervisor for the adapted model. We show how model deltas can be used to describe the difference between pairs of models. Using the model deltas, a notion of atomic model adaptations is introduced. For these atomic adaptations, algorithms are provided to compute the supervisor for the adapted model in a transformational manner from the previous synthesis result, rather than performing a completely new synthesis. These atomic model adaptations can be iterated over, to transformationally compute a supervisor for model deltas containing a number of atomic model adaptations. The efficiency of this method is evaluated by means of some experiments.