Most graphical workflow modeling tools and concepts somehow involve placing services at a graph canvas and connecting them with branches according to the flow of control. The PROPHETS plugin extends the jABC framework by introducing another modeling possibility, which is to our knowledge unique to our framework: Loose Programming. There, the process developer can mark branches as loosely specified, the plugin will then apply synthesis methods to find appropriate service sequences and replace the loosely specified branch, if necessary.
As the figure shows, working with PROPHETS incorporates two major phases: domain modeling and workflow design. During domain modeling PROPHETS is prepared for the application domain. This involves at first the definition of available services and data types as well as the interface description of services regarding their input and output data. After that, further semantic classification can be applied on types and services using taxonomies and finally, domain-specific constraints may be added to the domain model. The workflow design phase then constitutes the main working area of PROPHETS. Starting from a loosely specified workflow (top left corner of workflow design box) an iterative refinement of constraints and synthesis parameters is applied until the user chooses one appropriate solution. If during experimentation with the loose workflow refinement further general domain-specific information is revealed, domain-specific constraints might be added to the domain model.
In the background, PROPHETS uses a synthesis algorithm, which performs a search by evaluating a synthesis universe and a given formula in Semantic Linear Time Logic (SLTL) in parallel. SLTL, a variant of the commonly known PLTL, is tailored to finite paths and enhanced by transitions with actions and the possibility to express semantic ranges for actions and propositions based on taxonomies.