In this paper we show that the automated reasoning technique of deductive synthesis can be applied to address the problem of machine-assisted composition of e-Science work ows according to users' speci cations. We encode formal speci cations of e-Science data, services and workows, constructed from their descriptions, in the generic theorem prover Isabelle. Work ows meeting this speci cation are then synthesised as a side-effect of proving that these speci cations can be met.
Data-intensive scienti c computing usually involves
very complicated processes that are normally composed
of many steps, each involving signi cant computation.
eScience provides a distributed problem solving environment
for many scienti c projects and researchers, in which Grid
computing is the key enabling infrastructure. Grid services
are composed into work ows to build composite e-Science
applications to achieve complex user tasks. Recent
implementations of Grid computing environments [
Work ow-level access to Grid resources is a
substantial step toward the realisation of the vision of e-Science.
However, the e-Science Grid will keep expanding as more
resources are incorporated into the e-Science community;
the scale and complexity of such distributed and
heterogeneous systems would make any level of assistance desirable
to even experienced users. Several projects have addressed
the problem and provided different levels of automation in
helping users compose, validate and execute their
workows, such as [
Our project focuses on the machine-assisted synthesis of
work ows to meet users' speci cations. In this paper, we
describe a novel approach of modelling Grid data and
services, in which they are extracted from their semantic
descriptions in a formal system that is a further abstraction
of the Virtual Data Language (VDL) [
Current work ow environments are still far from the
reach of real scientists who are working with real scienti c
problems. To use a Grid through its work ow interface,
many users have to struggle with the following obstacles:
Considerable Expertise is required for scientists to
effectively design their work ows using interfaces to
script-based language [
Service Look-up is dif cult for users as there are many service instances published by different service providers, intended for different disciplines, implemented over different platforms and with different levels of encapsulation.
Resource Deployment is a prohibitive task for users due to its complexity. The abstract work ow has to be deployed onto a network of concrete Grid resources connected and con gured accordingly.
In addition to the problems described above, there are two further dif culties that often arise in the manual composition approaches: Service instances have Contextual Properties which may need to be considered. For example, it may be preferable to incorporate services from a certain set of af liated providers, or produce the computing result in a particular format depending on the local computing architecture. However, users are usually provided with limited information about the contextual properties of service instances. This is mainly due to the inadequate expressiveness of service description languages and the heterogeneity of the Grid environment and eScience application domains.
The complexity involved in the manual composition of work ows makes them likely to fail. The Execution Failure of composed work ow can be very hard to detect and avoid manually, as even advanced users cannot easily deal with all the issues stated above.
To address these problems, rst, we adopt a semantic
description of Grid resources. In our approach, Grid
services, data and other Grid resources are declared as objects
formally speci ed with their properties. Extra
applicationspeci c replicas of Grid services and data can be
implemented for different computing architectures or stored in
different locations, and they will have different physical
properties, location, local name, run-time parameter, etc.
However, the replicas remain logically equivalent in term
of the metadata specifying their logical properties:
ontological types and so on. We reason at this abstract
logical level. Abstract work ows then need to be compiled
into concrete ones, augmenting them with the details of
actual Grid services. The compilation process is addressed by
other projects [
Logic descriptions of Grid resources can be obtained
through the Metadata Catalog Service (MCS) that responds
to queries of domain-speci c metadata and returns the
logical names of matching Grid services or data [
Second, Grid services and data are modelled as logical
formulae. Our formalisation in Isabelle is rather
straightforward, as all the property elds of Grid resource declarations
are mapped into the Isabelle record datatype. We extract the
ontology of data from the metadata used in existing Grid
applications. For example, in the application domain of
the Laser Interferonmeter Gravitational Wave Observatory
(LIGO) [
In the data-centric e-Science environment, Grid services can be modelled as transformations on data. Therefore, the service metadata can be simply designed to include only the input and output data of the Grid service. Again, physical properties are used to declare the concrete details, including the location, the UNIX script and the arguments to access or invoke the service instance.
By allowing the declaration of pre-conditions, which can be the evaluations of the properties of the service and its in/output data, as well as the relationships between them. This allows the representation of knowledge about the contextual properties of Grid services, for example, how the service interacts with others, and other service-speci c characteristics, requirements and capabilities.
With the application-speci c knowledge of Grid services encapsulated in their independent speci cations, we implemented generic work ow operators that depict the data- ow nature of e-Science Grid applications and are no longer speci c to particular e-Science knowledge domains or applications.
The Isabelle theorem prover is used to prove that the
speci cations of the abstract work ow can be met, and the
synthesised work ow is extracted from the proved theorem,
cf. [
Scienti c experiments are data-centric: data are collected by measurement instruments, stored, processed and analysed; later it may be retrieved, compared and derived; or used by other researchers. e-Science is therefore datacentric as well. It is crucial to model the data objects, as well as the processes that transforms the data.
In a data-centric Grid, services can be modelled by the application of computational procedures that derive and transform data. Explicit representation of these procedures, so-called virtual data, enables the recording of data provenance, discovery of matching services and on-demand data generation. where { LIGO-pulsar;
LSC-AS_Q H1 ILWD annotated with domain-speci c knowledge from the LIGO elds describe the logical properties of the abstract data stored in the data le. The ontology is extracted from the data replica that store the pulsar data in the LIGO knowlWe now de ne the abstract logical representation of a is of the ontological type
is the ontological type and other
The generic type of Pulsar data is de ned as an extenedge domain: (1) bridge the gap between the logical data discovery, by uni cation over the ontological type, and the instantiation of logical data to data instances, that can be regarded as extending the logical data with the instance-speci c properties.
Uni cation is provided by Isabelle's implementation of
Huet's higher order algorithm [
that contains only the , by extending the base (super-class) with extra elds.
This representation allows uni cation to supports users querying e-Science data using domain knowledge and semantic descriptions expressed, such as: (3) The query can be read as: Is there a data replica that and describes the ?. Note that , as the data instances eld. The is existentially quanti ed. The proof of (3) will instantiate . This instantiation will represent the desired abstract work ow. In this way, the proof synthesises the work ow.
can be instantiated to any data instance whose data instances are either manually declared or provided by RLS, and then translated to logical formulae as in (2). If there is such a logical representation of a data instance of that stores the LIGO sequence of the rst 1000 samples, then we are able to prove the formula (3) directly and thus
is synthesised to be that data instance; otherwise, search is needed to nd a combination of data instances that together satisfy the conditions in the conjunction. We employ backward search using uni cation with heuristics and tactics to guiding the proofs automation. 3.2
exible and generic work ow synthesis system, we started by extending VDL to support types of data. The simple DAG shown in Figure 1 is an abstract LIGO work ow example. Below, we discuss how our system can synthesise this work ow from its speci cation.
We need to declare the new LIGO logical data and
services that are speci ed as transformations of data:
sible record type [
are both to be extracted.
We now show how the two service types are de ned by and . Both have the
and is de ned in a way similar which is the type of raw LIGO data (4) where we currently model Grid services with multiple insynthesis procedures. We plan to incorporate more logidatatype of lists has built-in recursively-de ned constructors that are convenient for peeling off the elements of a list of input/output data. The reaA work ow, which is a network composed of a number son is that, during the synthesis of work ows, we need to analyse each logical datum of the input/output elds. The of Grid services, can be modelled as the accumulated data component. transformation. In this fashion, a Grid service is then a singular work ow that consists of only one high-level service The physical properties of Grid services are simply modAbstract work ows have only work ow-level properties elled as a string containing the arguments. Currently they are not taken into consideration during the veri cation and instead of concrete runtime parameters, such as the execution arguments and physical locations. Therefore we model common base type of work ows and processes, is now deeld is designed to record the provenance, which, in the current implementation, is simply constructed elds of the work ow's components. The runtime eld is the sum of the execution 4.2
The work ow example as shown in Figure 1 can then be formalised using these two operators: } p for propagating QoS properties around work ows. , the ity of service (QoS) properties, including provenance, runtime and reliability, which is the probability that the profor the bene t further work, such as the recently started project Inferring Quality of Service Properties for Grid Applications, which aims to develop compositional calculi cess will execute successfully. QoS information is included
ned as:
times.
Instantiated all current variables?
N
N Find an service (Si) with output data that unifies with the goal output data of some variable
Succeed?
Y Y
Succeed? Synthesis Succeed!
introducing (?v2 || ... || ?v3) -> Si introducing ?v2 -> Si Y
Si has Multiple Input Data?
N Synthesis Failed! VO1 and VO2; the runtimes are 20, 30 and 20; and the reliabilities are 0.80, 0.60 and 0.70, respectively2, then the resulting combined work ow is: elds for 2The work ow runtime is obtained by summing the runtime elds on sequentially executed processes and enumerating the maximum runtime of processes executed in parallel.
The synthesis of this simple work ow is performed by repeatedly applying to the goal the set of tactics given in 4.3
Equipped with the formal speci cations of the service instances and work ow, we are able to generate the desired work ow from its speci cation using deductive synthesis. de ned as in (8), the goal we need to prove is de ned in Isabelle notation as: which can be instantiated to be any term of the correct type, is implicitly existentially quanti ed. The goal can be read as What kind of work ow can satisfy the speci (8) ? satis es the
(9) (10) from equation (10) can directly with criteria: ˝ o be achieved as follows:
inputs and outputs. i. The meta variable ¿`«˜ fails, as there is no service that directly matching these 3. This introduces the sequential operator, , and the (11) (12)
. can now be in
1. Trying to instantiate ¿` ¿` The deductive synthesis of 2. Unifying only the output of ¿`
sults in the new goal: a goal: be left unknown in the query and can be instantiated during the synthesis by calculation from the corresponding QoS properties of the atomic Grid services from which the workow is composed. 5
Chimera [
Pegasus is a planning system to reason about the
runtime properties of Grid service instances, map the abstract
work ow components to physical resources according to
users' and resource providers' preference and generate
executable work ows to the Condor work ow interface,
DAGMan [
The Chimera approach to work ow generation is
restrictive in terms of the work ow constructs it is capable of
supporting. In contrast, our approach supports a richer
language and uses deductive synthesis to incrementally
synthesise a work ow that has been proved to meet the
speci cation. Regarding the work ow synthesis as a theorem
proving problem offers us a rich set of well-studied
constructs, including conditional branching, iteration and
recursion, greater expressiveness of preconditions and effects,
and many powerful techniques that help us in automating
the synthesis. Representing the Grid services and data using
an extensible record datatype in Isabelle, we intend to
address resource deployment as an integrated procedure
during the work ow synthesis. Our research group has
previously contributed to the deductive synthesis of programs
with several successful projects [
more complex representation used, and the extra work involved in proving that the speci cation is met, we expect the automated work ow synthesis to be slower than planning based approached. 6
Alternative approaches to automated work ow synthesis
use AI plan formation rather than deductive synthesis, [
can then be instantiated with the other one.
thesis succeed.
iii. All schematic variables instantiated, the synThe tactics are currently applied interactively, but a fully automated version is being developed. Equipped with additional tactics and heuristics, we have successfully synthesised more complex work ows with nested operators, such as the one shown in Figure 3. To synthesise this complex work ow, we just need to build the goal as following:
The synthesis proof produces the following synthesised work ow:
The work ow properties of provenance, runtime and reliability do not contribute to the composition of the workow, so that their values for the synthesised work ow can and if so demonstrate that deductive synthesis can supply it.
We also intend to complete the automation of synthesis. the kinds of work ows they can synthesise. We will investigate whether e-Science requires this greater expressivity
Deductive synthesis in Isabelle allows the use of arbi6.1
Representation of Preconditions trary, higher-order logical formulae to describe Grid services. In contrast, planners are typically restricted to conand effects of services. We are investigating whether this greater expressivity is of practical use in describing serseveral different kinds, but not all kinds; it might be used in effects to explain that a service can have more than one kind of output, perhaps depending on the input. Universal quanti cation might be used in pre-conditions to ensure that each of a large and varying number of tasks must have certain properties. Existential quanti cation might be used in to infer QoS properties of a compound work ow from its the representation into a conjunction of propositions.
As mentioned earlier, further work also includes trying 6.2
Synthesis Meeting QoS Requirements ing work ows to meet various QoS properties, e.g. a high reliability or accuracy, or a low runtime. For instance, let us components. For instance, the representation and calculation of QoS properties holds out the prospect of synthesisassume there is a creditability property of data that indicates how reliable the data replica is. The pre-condition can vices.
For instance, disjunction might be used in preconditions to specify that a service can deal with data of junctions of propositions in describing the pre-conditions service effects to introduce a new object into the ontology, e.g. a new data item. We will both invent services with such properties and search the e-Science literature to nd naturally occurring exemplars. We then plan to examine how deductive synthesis can represent and use these services in a natural way, i.e. without the use of kludges to shoe-horn 6.3
We plan to implement more work ow operators in our
framework for better representation of the real Grid
environment and more practically useful features. For instance,
the work ow interface of the Unicore system [
In this paper, we present the current progress of our project aiming at the automatic synthesis of e-Science work ows. Our approach, compared with other rival approaches: provides richer abstraction of Grid data and services, which will enable on-demand query and computing of complex e-Science data, implements a deductive synthesis system in which eScience work ows are formalised and can be veri ed against their speci cation, has the potential to provide more expressive descriptions of Grid services and to synthesise more expressive work ows, has the potential to represent and reason about QoS properties, and is notable as the rst attempt, to the authors' knowledge, to apply deductive synthesis technique to synthesise e-Science work ow interactively on users' demand.
We are working to fully automate the synthesis process, to explore the potential for greater expressivity in service descriptions and work ows, and to synthesise work ows with respect to QoS properties. These further work plans dovetail together in that greater expressivity is required for QoS synthesis, and greater expressivity in work ows requires greater expressivity in service descriptions.