PROPHETS. a framework for loose programming

Concepts

Loose Programming

In service-oriented/model-based software development, the process designer usually needs to have knowledge about the available services and their dependencies. Large service libraries are therefore difficult to cope with. Discovery techniques, synthesis and planning can be applied to generate service combinations automatically according to higher-level process specifications, but the formulation and formalization of appropriate search queries or process specifications is difficult for users that are not specially trained in IT and formal methods. Similarly, numerous approaches to general program synthesis exist, but also aim more at programmers or specialists in formal specification.

Our loose programming approach addresses this issue by enhancing model-driven software engineering with an intuitive mechanism for loose specification and translation of loose specifications into fully specified processes. PROPHETS is our proof-of-concept implementation of loose programming. With jABC and PROPHETS, process developers are given an experimentation platform that enables them to design their application-specific processes in an intuitive style.

Domain Modeling

During the domain modeling phase meta-information about the available services is collected and provided in appropriate form. This is usually not the business of the workflow developer, who simply works with it via the loose specification and synthesis framework, but of a dedicated domain expert. The domain knowledge includes basic descriptions of the available services by means of input and output type declarations as well as statements about type compatibility and dependencies between services. It can be extended by hierarchically organizing types and services in taxonomies, i.e. simple ontologies that relate entities in terms of is-a relations. With these taxonomies types and services can be classified according to semantic properties. The taxonomies are considered by the synthesis algorithm when evaluating type or service constraints. The originally defined services and types are named concrete, whereas semantic classifications are named abstract.

The domain definition for synthesis with PROPHETS is given by:

Each service is characterized by three subsets of the data types set. The input types are required for the service to be executed, and while the output types are produced by the service, the killed types are consumed or deleted.

Synthesis

The (graphical) loose specification is translated into a temporal logic formula that defines the starting point and end conditions of the workflow. Together with different additional constraints, it gives a comprehensive characterization of the loosely specified workflow. In fact, the specification formula that is finally given to the synthesis algorithm is a conjunction of all available constraints, comprising:

The specification formula describes all sequences of services that meet the individual workflow specification. As the explicit representation of all these sequences would be extremely large, they are not explicitly built, but given as a declarative formula in Semantic Linear Time Logic (SLTL), a variant of the commonly known propositional linear-time logic (PLTL).

To assure that a service sequence that is valid in the sense of the specification formula is also technically executable, a configuration universe is required. It contains all sequences that are valid executions without taking into account any problem-specific information. The configuration universe is represented as an automaton that connects states with edges according to available services. While each state represents a subset of all types (abstract and concrete), the connecting edges perform the transition on those types, according to input and output specifications, as defined in the domain model. Every path in this automaton, starting from a state that represents the initially available data, constitutes one executable service sequence. Note that as the configuration universe is usually very large, it is not explicitly generated from the domain definition, but expanded on the fly during the synthesis process.

The algorithm that is then applied to complete a loosely specified workflow to be fully executable takes the above introduced aspects into account. On the one hand, the constraints specified by the workflow designer must be met, on the other hand, the workflow must be type-consistent to be executable. Hence, the synthesis algorithms works on:

To start the search for solutions, the synthesis algorithm requires an initial state (i.e. a set of available start types). They are determined automatically, either according to the output specification of the service at the beginning of the loose specification or by a data-flow analysis to globally capture the availability of types. The synthesis algorithm then interprets the SLTL formula that expresses the synthesis problem over paths of the synthesis universe, that is, it searches the synthesis universe for paths that satisfy the given formula. The algorithm is based on a parallel evaluation of the synthesis universe and the formula. As each of the paths that are consistent with both the universe and the SLTL formula are valid concretizations of the loosely specified branch, it automatically generates only valid service compositions. Its output is the basis for the final assembly of the corresponding process model. If multiple valid service compositions are found, the user will either be queried to choose one, or the system will choose one according to a previously defined cost function (e.g. by length of solution, computation time etc.).

Many aspects of the synthesis algorithm, such as overall search strategy, data exchange pattern or start and goal constraint construction, can be configured within PROPHETS. Please refer to the manual for further details on those configuration possibilities.

Constraint Templates

The formulation of constraints in terms of SLTL is naturally restricted to experts trained in computer science's formal methods, who are not our focused user group. Therefore, the PROPHETS plugin provides a template-based wizard that enables the process developer to express his/her problem-specific constraints with natural-language statements. Those easily extensible templates contain wildcards that need to be defined by the user. These wildcards can be typed as either service or type both with the variations only abstract, only concrete and abstract or concrete. The wizard then presents the user a drop-down box to choose the appropriate service or type from. The following table shows the templates and associated SLTL formulas that are available in the PROPHETS default installation:
templates