Compositional Analysis of Timed-arc Resource Workflows with Communication

Student thesis: Master thesis (including HD thesis)

  • Christoffer Moesgaard
  • Sine Viesmose Birch
4. term, Computer Science, Master (Master Programme)
We propose timed-arc resource workflows (TARWFN), which have the possibility to save information in a workflow between executions, as well as being able to communicate with other workflows. We introduce a notion of local soundness and strong local soundness for TARWFN, sequential composition, and an algorithm for checking (strong) local soundness by reducing it to a formalism for which efficient soundness checking algorithms already exist. We make it possible to analyse workflows, still retaining a notion of soundness for sequential composition. For strong locally sound workflows we can determine minimum- and maximum execution time of the workflow, making it possible to approximate the entire workflow with a single transition having the minimum- and maximum execution times as its guards. The algorithm is implemented in the publicly available, open-source model checker TAPAAL. We demonstrate the usability of the workflows on a real-world smart house. The size of the state space of the house renders normal state space exploration infeasible. With TARWFNs we are able to approximate the smart house such that we are able to conclusively answer questions about the house within reasonable time.
Publication date8 Jun 2015
Number of pages60
ID: 213815071