An Executable and Testable Semantics for iTasks

The

iTask

system is an easy to use combinator library for specifying dynamic data dependent workflows in a very flexible way. The specified workflows are executed as a multi-user web-application. The implementation of the

iTask

system is fairly complicated. Hence we cannot use it for reasoning about the semantics of workflows in the

iTask

system. In this paper we define an executable semantics that specifies how workflows react on events generated by the workers executing them. The semantics is used to explain

iTask

and to reason about

iTask

. Based on this semantics we define a mathematical notion of equivalence of tasks and show how this equivalence for tasks can be approximated automatically. Advantages of this executable semantics are: it is easy to validate the semantics by interactive simulation; properties of the semantics can be tested by our model-based test system

G

 ∀ 

st

.

G

 ∀ 

st

can test a large number of properties within seconds. These tests appeared to be a good indication about the consistency of the specified semantics and equivalence relation for tasks. The automatic testing of properties was very helpful in the development of the semantics. The contribution of this paper is a semantics for

iTask

as well as the method used to construct this operational semantics.