Constraint Verification for Concurrent System Management Workflows Sharing Resources

Workflow is an effective way to define and specify the behavior of autonomic systems which manage themselves. However, when a system is working following several workflows sharing resources, it is very difficult to analyze the behavior of the systems with mutual influences between workflows due to the shared resources, and to decide whether problems may be caused by such mutual influences, despite the need to do so in order to develop trustworthy autonomic systems. To solve this problem, we developed a verification framework to identify whether constraint violations could occur in a system working and following workflows sharing resources. In this paper, we initially define the system management workflows. Next, we show the procedure to translate these workflows into hybrid automata, with the mutual influences between workflows taken into consideration. Finally, we show how to detect possible constraint violations by adopting a model checking technique to the hybrid automata through a case study.