ions for concise and precise specification of such control, but balance this with visualization support to help users also obtain intuitive insights. The underlying complexhese control abstractions, however, often confounds these 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. Specifically, 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 ecommerce auction example. Although we employ a particular process definition language and analysis technique, our results seem more generally applicable.
Jamieson M. Cobleigh, Lori A. Clarke, Leon J. Oste