Presented by Tobias Olsson (because the author didn’t get a visa in time)
The idea of the paper is that while transforming you can have bad states that you do not want to reacah, maybe because the system is unstable (e.g. a buffer with messages), or because it is a deadlock. Another issue is that not all events can be observed, e.g., the internal state of the component is unknown, or that sensors are unreliable. Thus, one has partial observations. This results in inspecting a very large state space to prevent reaching bad states. The author’s approach takes a three-step approach.
Single components are modelled using FSMs. There is a FSM model for reconfiguration as well, with special actions to transform messages. To specify bad states, predicates are used. Based on these predicates, and the FSM model, the author generates a supervisory controller. Some events may be uncontrollable. In the end, the controller ensures with guards that no bad states can be reached. From the total state space, bad states are identified and the paths leading to it are removed. The approach comes with tool support.
The approach reminds me of the papers of Lohmann et al on adding constraints in controllers, and the adaptive nets worked upon by Olivia Oanea…
P.S. if you ever have to create slides for formal methods, don’t use LaTeX…