Last man standing: Static, decremental and dynamic resiliency via controller synthesis

The workflow satisfiability problem is the problem of finding an assignment of users to tasks (i.e., a plan) so that all authorization constraints are satisfied. The workflow resiliency problem is a dynamic workflow satisfiability problem coping with the absence of users. If a workflow is resilient, it is of course satisfiable, but the vice versa does not hold. There are three levels of resiliency: in static resiliency, up to k users might be absent before the execution starts and never become available for that execution; in decremental resiliency, up to k users might be absent before or during execution and, again, they never become available for that execution; in dynamic resiliency, up to k users might be absent before executing any task and they may in general turn absent and available continuously, before or during the execution. Much work has been carried out to address static resiliency, little for decremental resiliency and, to the best of our knowledge, for dynamic resiliency no exact approach that returns a dynamic execution plan if and only if a workflow is resilient has been provided so far. In this paper, we tackle workflow resiliency via extended game automata. We provide three encodings (having polynomial-time complexity) from workflows to extended game automata to model each kind of resiliency as an instantaneous game and we use UPPAALTIGA to synthesize a winning strategy (i.e., a controller) for such a game. If a controller exists, then the workflow is resilient (as the controller's strategy corresponds to a dynamic plan). If it doesn't, then the workflow is breakable. The approach that we propose is correct because it corresponds to a reachability problem for extended game automata (TCTL model checking). Moreover, we have developed ERRE, the first tool for workflow resiliency that relies on a controller synthesis approach for the three kinds of resiliency. Thanks to ERRE, our approach is thus also fully-automated from analysis to simulation.