Workflows with Passbacks and Incremental Verification of Their Correctness

概要

論文の詳細を見る
In this paper, we discuss a fundamental theory of incremental verification for workflows. Incremental verification is a method to help multiple designers share and collaborate on huge workflows while maintaining their consistency. To this end, we introduce ipassbacks/i in workflows and their consistency property in the control flow perspective. passbacks indicate redoing of works. Workflows with passbacks are useful to naturally represent human works. To define the consistency property above, we define normality of workflows with passbacks and total correctness of normal workflows based on transition system-based semantics of normal workflows. We further extend workflows to sorted workflows and define their vertical division and composition. We also extend total correctness to normal sorted workflows, for the sake of incremental verification of a large-scale workflow with passbacks via vertical division and composition.
2012-04-01