Verifying properties of process definitions

It seems imperative that the complex processes that syner-gize 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 spec-ify these processes and to then use analysis techniques to evaluate these definitions for important correctness proper-ties. Because humans demand flexibility in their participa-tion in complex processes, process definition languages must incorporate complicated control structures, such as various concurrency, choice, reactive control, and exception mecha-nisms. Well-designed process languages provide powerful abstractions for concise and precise specification of such control, but balance this with visualization support to help users also obtain intuitive insights. The underlying complex-ity of these control abstractions, however, often confounds these intuitions as well as complicates any analysis. Thus, the control abstraction complexity in process def-inition languages presents analysis challenges beyond those posed by traditional programming languages. This paper ex-plores some of the difficulties of analyzing process defini-tions. Specifically, we explore issues arising when applying the FLAVERS finite state verification system to processes written in the Little-JIL process definition language and il-lustrate these issues using a realistic ecommerce auction ex-ample. Although we employ a particular process definition language and analysis technique, our results seem more gen-erally applicable