Verifying Properties of Process Definitions

It seems important that the complex processes that synergize humans and computers to solve widening classes of societal problems be subjected to rigorous analysis. One approach is to use a process definition language to specify these processes and to then use analysis techniques to evaluate these definitions for important correctness properties. Because humans demand flexibility in their participation in complex processes, process definition languages must incorporate complicated control structures, such as various concurrency, choice, reactive control, and exception mechanisms. The underlying complexity of these control abstractions, however, often confounds the users’ intuitions as well as complicates any analysis. Thus, the control abstraction complexity in process definition languages presents analysis challenges beyond those posed by traditional programming languages. This paper explores some of the difficulties of analyzing process definitions. We explore issues arising when applying the FLAVERS finite state verification system to processes written in the Little-JIL process definition language and illustrate these issues using a realistic auction example. Although we employ a particular process definition language and analysis technique, our results seem more generally applicable