Compositional Analysis of Timed-arc Resource Workflows with Communication

Studenteropgave: Speciale (inkl. HD afgangsprojekt)

  • Christoffer Moesgaard
  • Sine Viesmose Birch
4. semester, Datalogi, Kandidat (Kandidatuddannelse)
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.
Udgivelsesdato8 jun. 2015
Antal sider60
ID: 213815071