{'fraction_non_alphanumeric': 0.04395455774952664, 'fraction_numerical': 0.00708682715715445, 'mean_word_length': 4.380730606898559, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Towards Formal Interaction-Based Models of Grid Computing Infrastructures

Grid computing (GC) systems are large-scale virtual machines, built upon a massive pool of resources (processing time, storage, software) that often span multiple distributed domains. Concurrent users interact with the grid by adding new tasks; the grid is expected to assign resources to tasks in a fair, trustworthy way. These distinctive features of GC systems make their specification and verification a challenging issue. Although prior works have proposed formal approaches to the specification of GC systems, a precise account of the interaction model which underlies resource sharing has not been yet proposed. In this paper, we describe ongoing work aimed at filling in this gap. Our approach relies on (higher-order) process calculi: these core languages for concurrency offer a compositional framework in which GC systems can be precisely described and potentially reasoned about.

such as CCS [11] and the π-calculus [12] have been developed within the concurrency theory community as basic models for communicating systems. As process calculi are compositional, they have proved useful for developing reasoning techniques over specifications (e.g. behavioral equivalences and type systems) and for investigating new programming abstractions based on communication. These features make process calculi an attractive basis for the formal specification and verification of GC systems.
In particular, in this paper we rely on higher-order process calculi, i.e., calculi in which processes (more generally, values containing processes) can be communicated. This is in contrast to first-order calculi such as the π-calculus, in which only basic values and/or communication channels can be exchanged. Higher-order process calculi can be seen as concurrent variants of the λ -calculus. In fact, the reduction rule for communication in these formalisms is reminiscent of well-known β -reduction in functional calculi. In the grid setting, higher-order (or process passing) concurrency naturally models the fact that user tasks -typically, arbitrarily complex descriptions of computational behaviors-need to be exchanged among different grid components in order to achieve their execution. In particular, we rely on the higher-order π-calculus (HOπ) [15], a core language which enhances the name passing abilities of the π-calculus with process passing. HOπ specifications can represent forms of code mobility, therefore allowing for flexibility in descriptions of concurrent communications. Moreover, useful proof techniques based on behavioral equivalences are well-understood for (variants of) HOπ (see, for instance, [16]).
The main contribution of this work is a formal model of GC infrastructures, with a focus on the resource assignment facility that is central to them. Our model distills the main features of GC systems, as informally discussed in the literature (see, e.g., [6]) and as identified in our own exchanges with GC experts. The model is divided into static and dynamic components. The static component, defined in first-order logic, formalizes the essential pre-conditions and invariants that should hold for the different grid subsystems. Using HOπ processes, the dynamic component captures the (concurrent) execution sequences associated to potentially many users interacting simultaneously with the grid. These components are intended to be complementary: building upon the relations defined by the static component, the dynamic component accounts for the main agents present in real GC infrastructures, such as users, tasks, administative domains, virtual organizations, and resources. Our model also considers user and resource proxies, which facilitate user interaction with the GC system and resource management (see Sect. 2).
While simple, our formal model already provides a good basis for obtaining more detailed descriptions of GC systems and for reasoning about their correctness properties. Examples of such properties are authentication and authorization guarantees: they are intended to ensure that users only access and use the administrative domains and resources for which they can prove their identity/permissions. An extension of our current model with suitable cryptographic elements (using, e.g., the higher-order language in [9]) would be a step in this direction. Another relevant property concerns the balanced assignment of administrative domains and their use of resources. To this end, process specifications of different scheduling and assignment policies may be necessary -this issue is largely orthogonal to the model given here. Other properties of interest for GC modelers involve task termination and resource delivery aspects. By adapting known results on termination and reachability properties for calculi such as CCS [3] and for variants of HOπ [10,8], our model could offer an alternative for investigating such properties. tervention, and the rôle of user and resource proxies in resource assignment and task execution. In [13], Abstract State Machines (ASM) are used to give a declarative characterization of GC systems; this characterization formally describes some of the main attributes that a GC system should support. The GC elements are modeled as universes (sets); their behavior is represented using rules over universes. The only grid agents considered in [13] are tasks (there called processes); there are also user and resource mapping agents. Each agent executes the rules over the defined universes. In contrast to our work, in the model of [13] concurrent interactions among GC components are not explicitly represented; also, such a model does not consider the key concept of virtual organizations and the rôle of user and resource proxies. Finally, in [1,4], high-level and colored Petri nets were used to analyze grid architectures and grid workflows. A 3-layer grid architecture and the interaction between GC components in these layers is modeled. However, these approaches do not consider virtual organizations, administrative domains, and security requirements -all of these being central elements in resource assignment.
Organization. The rest of this paper is organized as follows. Sect. 2 briefly recalls the main features of GC systems. In Sect. 3 we present the syntax and semantics of the higher-order π-calculus. Sect. 4 gives a brief description of our GC formalization, and Sect. 5 illustrates it via a small example. Finally, future work is discussed in Sect. 6. A full description of our formal process model is available in [14].

Grid Computing: A Brief Overview
Grid computing broadly refers to the coordinated resource sharing and problem solving in dynamic, multi-institutional virtual organizations. GC systems often require interoperability features and support for heterogeneous environments. Other typical requirements are decentralized control, security, access transparency, scalability, availability, and reconfigurability [6]. Sharing in GC systems not only refers to data and information but also to direct access to all kinds of resources which may be required for executing complex tasks (computing power, storage, software applications, data). Each administrative domain (AD in the following) establishes what resources are shared and their access and usage policies. A virtual organization (VO in the following) is a set of ADs defined by such policies. The participants in a VO share resources in a controlled way in order to cooperate in executing a specific task. VOs vary in their purpose, scope, size, duration, structure, community, and sociology [6].
In GC systems, users can transparently share or access resources-they do not need to know (or be aware of) what resources they are using, where such resources are physically located or that they may have previously failed and recovered. This transparency is achieved by the so-called grid middleware. This is a software layer that (i) implements the protocols and services that enable the seamless sharing of heterogeneous resources, and (ii) provides key functionalities for enabling task execution and VOs establishment [18]. In this way, the middleware allows users to access resources while satisfying security policies such as authentication, authorization, delegation, and single sign-on. To this end, the grid middleware includes user and resource proxies [7]. While a user proxy is an entity that is given permission to act on behalf of a user for a fixed period of time, a resource proxy serves as interface between the middleware and a resource, thus simplifying (i) the authentication between user proxy and the resource and (ii) the mapping between grid users and the local users which are valid in the resource. Grid Resource Assignment Protocol. As our interest is in an interaction-based approach to GC systems, below we present a protocol which describes the interaction sequence among the main grid components (users, ADs, VOs, resources, proxies). The protocol is described as a sequence diagram in Fig. 1; 1. A user sends its credentials to a grid node in order to authenticate. In the figure, this step is represented by the message login(user cred) from User to VO.
2. If the authentication is successful then the user is granted to access the grid. Otherwise, the user must revise its credentials. For simplicity, the figure shows only the case in which authentication is successful; this step is represented by message ok from VO to User.
3. The authenticated user sends a proxy creation request, and a task with its requirements to the grid node. The task may be a complex object; in particular, it may be structured in terms of subtasks which follow some process logic. In the figure, these steps are represented by messages userproxy creation() (from User to VO), create() (from VO to User Proxy), and request(Task) (from User to VO).
4. The user proxy sends to the grid node the requirements of each subtask. In the figure, this step is represented by the message submit(reqs, Task ′ ) from User Proxy to VO.

5.
The node selects an AD in the VO with available resources to satisfy the subtask requirements. This subtask is assigned and sent to the selected AD. In Fig. 1, this is represented by messages determineAd(Task ′ ) (inside VO), submitTask(Task ′ ) (from VO to AD), and queue(Task ′ ) (inside AD).
6. The AD assigns appropriate resources for this subtask according to some scheduling strategy. In the figure, this step is represented by the message assignRes(Task ′ ) inside AD.
7. The user proxy authenticates into the resource proxies of assigned resources. If authentication is successful then the subtask is executed. Otherwise, the subtask is sent back to the grid node. In the figure, these steps are represented by messages auth res(user cred) (from User Proxy to Resource Proxy), ok (from Resource Proxy to User Proxy), sendJob() (from Resource Proxy to Resource), and job exec() (inside Resource).
8. When the subtask has finished (message f inish(res), from Resource to its Resource Proxy), it is detected if there are more subtasks (condition Task ′ = null in the loop). If yes then the result of the previous subtask is transmitted to the next subtask and the previous subprotocol is executed again (message submit(reqs, Task ′ )). Otherwise, if the just executed subtask is the last one, then the result is stored and the protocol finishes (message store(res) from User Proxy to AD).
A Representative GC Scenario. We now describe a small, representative example of a GC system. Depicted in Fig. 2, our scenario draws inspiration from the one given in [6]. It contains three ADs (denoted d 1 , d 2 , and d 3 ) and two VOs (denoted v 1 and v 2 ); in the figure, they are depicted as ovals and rectangles, respectively. VO v 1 (blue background) groups participants in an aerospace design consortium and v 2 (dotted background) links participants for sharing spare computing cycles. AD d 1 is member of both v 1 and v 2 . Also, ADs d 1 and d 2 participate in v 1 and AD d 3 participates in v 2 . We also consider users u 1 and u 2 : while u 1 belongs to v 1 , user u 2 belongs to u 2 . Both u 1 and u 2 have a task to execute in the grid, denoted Task1 and Task2 in the figure, respectively. To perform, Task1 requires one resource of type (or descriptor) k 1 and one resource of type k 2 . Similarly, Task2 requires three resources, distinguished by types k 1 , k 2 , and k 3 . Resources are located in appropriate ADs: AD d 1 owns three resources: r 1 (type k 1 ), r 2 (type k 1 ), and r 3 (type k 2 ); AD d 2 owns two resources: r 4 (type k 1 ) and r 5 (type k 2 ); and AD d 3 owns three resources: r 6 (type k 1 ), r 7 (type k 2 ), and r 8 (type k 8 ). While resources of d 1 are shared by v 1 and v 2 , resources of d 2 are available only to v 1 , and resources of d 3 are available only to v 2 .

The Process Model: Syntax and Semantics
This section briefly presents the syntax and semantics of the higher-order π calculus, HOπ. Our presentation closely follows [15]. In HOπ, both names (communication channels) and processes may be passed around by synchronization on names; communication can be thus loosely assimilated to β -reduction in the λ -calculus. We assume a set of names/channels ranged over x, y, z, . . . and a set of process variables ranged over X ,Y, Z, . . .. We write o to denote a finite tuple of elements o 1 , . . . , o k .
Definition 3.1. The language of HOπ processes is given by the following syntax: We have two prefixes, ranged over α, α ′ , . . .. An input prefix x( U ) (resp. output prefix x K ) denotes an atomic input action (resp. output action) on a name x. Above, K and U denote tuples of names and processes, and of names and variables, respectively. Process ∑ i∈I α i .P i represents the non-deterministic choice among prefixed processes α i .P i . The operational semantics ensures that only one of them will be executed, discarding the rest. When I = / 0 we write 0; when I = |2| we write α 1 .P 1 + α 2 .P 2 . Also, we simply write α to refer to process α.0. Process P 1 | P 2 stands for the parallel composition of processes P 1 and P 2 . We write ∏ j∈J P j as a shorthand notation for process P 1 | . . . | P |J| . Process (νx)P declares the name x private to process P. That is, the scope of x is P; this scope may be enlarged by communication to other processes (scope extrusion). The conditional if [x = y] then P 1 else P 2 is based on equality of names x and y: if x = y then the process continues as P 1 ; otherwise it continues as P 2 . By taking inputs and restriction as binders, notions of free and bound names/variables arise as expected. We identify processes up to consistent renaming of bound names/variables, writing ≡ α for this congruence.
One way of specifying infinite process behavior is via parametric definitions. Notation D K denotes the application of a constant identifier D with parameters K. We assume each D has a unique definition where U is composed of all free names or variables in P, i.e. names or variable which occur out the scope of any binding. Then, X K denotes the application of parameters K to process variable X .
We endow our process language with a reduction semantics. Intuitively, a reduction P −→ Q denotes a single evolution step from process P to Q, without interaction from its surrounding environment. Fig. 3.

Definition 3.2. Reduction, P −→ Q, is the binary relation on processes defined by the rules in
As usual, we write =⇒ to denote the reflexive, transitive closure of −→. The rules in Fig. 3 formalize process communication and reduction under parallel composition and restriction. In rule (COM), notation P{ K/ U } stands for process P in which all free occurrences of names/variables in U have been substituted by names/processes in K. We assume arity in communications is consistent, i.e., the length of U must be equal to the length of K, with one-to-one correspondence among elements of both tuples. By means of rule (STR), reduction is closed under a structural congruence relation, written ≡, which is used to promote process interactions. It is defined as follows: Structural congruence, written P ≡ Q, is the smallest process congruence such that

A Formal Model of Grid Interaction
We now give an overview of our formal model of GC systems; a full description can be found in [14]. The model is intended as a formal counterpart of the informal interaction protocol given in Sect. 2. As already discussed, the model is divided into static and dynamic components. While the former is given in terms of invariants (first-order logic formulas), the latter is specified using HOπ processes. The two components play complementary rôles in our model. On the one hand, the invariants and conditions in the static part are used to: − Define the actors in the system (e.g. users, administrative domains, resources, tasks) and useful relationships between them; − Describe the initial configuration of the system; − Define well-formedness conditions for the processes of the dynamic part.
On the other hand, the dynamic part focuses on representing: − How the grid assigns resources to each task; − The start of task execution; − The state of tasks and their assigned resources.
It is worth highlighting that processes of the dynamic component cannot add new tasks, resources or users. Although these capabilities are present in some real grid systems, in the current development we focus on systems in which those elements cannot be added at runtime.

Static Component: Base Sets and Invariants
In order to formalize the key components of GC systems, we first relate such components to base reference sets. Then, we state associated invariant properties by defining static predicates over elements of such sets. Table 4 summarizes our notation for these base sets. The intuitive meaning of most of them

GC Component Base set GC Component Base set
should be clear from the description given in Sect. 2. We consider that each VO is associated to a group of access points (nodes) which are contained in the base set N. Observe that we distinguish between task definitions (which belong to base set T ) and task instances, which are submitted by users (and belong to base set S). We assume that task definitions are built using the next grammar: Above, J k 1 , . . . , k m denotes a basic task J with resources of type k 1 , . . . , k m , respectively (m ≥ 1). Building upon basic tasks, more complex ones can be defined, using sequential and parallel composition (denoted T.T and T T, respectively) and non-deterministic choice (T ⊕ T). We also assume a termination task, denoted end. As discussed above, we assume that each user is associated to a single task. This is not a limitation, for tasks may involve several subtasks in parallel and sequential composition. As for the invariants, based on informal descriptions in the literature [6], we have identified the elements that we consider essential to GC systems. Using first-order logic, we formalize such elements in terms of predicates over the elements of the reference sets. Some of such invariants are the following: − Each user is member of exactly one VO. Using predicate member(u, v), which holds if user u ∈ U is member of VO v ∈ V , we may state this invariant as: − Each user is associated to exactly one task to be executed in the GC system. Using predicate task(u, S), which holds if user u ∈ U is the owner of task S ∈ S, we may state this invariant as: − Each resource belongs to exactly one AD. Using predicate belongsTo(r, d), which holds if resource r ∈ R belongs to AD d ∈ D, we may express this invariant as: − Every AD can participate in one or more VOs. Using predicate participate(d, v), which holds if AD d ∈ D participates into VO v ∈ V , we may state this invariant as: ∀ d∈D , ∃ v∈V . participate(d, v).
Additional invariants concern access points (nodes), resource descriptors, task states, resource states, and task logs; they are given in terms of appropriate base sets, and are omitted here for the sake of space.

GC Component
HOπ Process Intuitive Description Grid system Grid ω,µ δ ,η Represents the whole GC system User (u ∈ U) u, S c,y = User( c, S t,e , y) Models the behavior of u to authenticate and submit its task S ֒→ UsrMonitor( c, g, a, y, P) Monitors tasks submitted by u Node (n ∈ N) n v,y, d = AP(y, d) Models the interaction of n with users to authenticate ֒→ AP-UsrHandler(ch 1 , ch 2 , ce) Models the user proxy creation and task submission ֒→ AP-ProxyHandler(ce, d) Represents the interaction with the user task Models the AD with its resources, proxy resources and management elements ֒→ AD-RecReq(b, d) Receives the tasks assigned to the AD and puts them in the queue ֒→ AD-AsgRes(b, d, ch) Dequeues tasks and assigns appropriate resources to them ֒→ AD-LRM( s, x, w, ch, d) Supervises the state of resources, and determines the available resources for a task Resource (r ∈ R) r r,q = AD-Resource(r, q) Models a resource's behavior when is used by a task User Proxy (a ∈ A) a ce,p,t,g = AP-UserProxy(ce, p,t, g) Models the task management, the request of execution of subtasks and the authentication with resource proxies Res. Proxy (x ∈ X) x x,q,r,w = AD-ResourceProxy(x, q, r, w) Acts as a mediator between GC components and a resource Log (l ∈ L) AP-Log(g r , g w , st, z) Interacts with GC components to register the changes in the task state and result Task (T ∈ T ) ⌈T⌉ t,e definition Represents the behavior of a task User Task (S ∈ S) S = ⌈T⌉ t,e Models a task instance corresponding to a user task Descriptors (k ∈ K) Names k 1 , . . . , k κ Models the different types of resources

Dynamic Component: Model in the HOπ calculus
In addition to specifying the main system components and the valid relations among them, our model should unambiguously describe how the system may evolve as a result of the interaction of its components. In the light of the protocol given in Sect. 2, such interactions may follow intricate patterns and must adhere to basic correctness and trustworthiness criteria. We would like formal mechanisms to ensure that models indeed satisfy such criteria. As we wish to describe GC systems compositionally, precisely specifying the interacting mechanisms and their relationships, first-order logic is not the most appropriate formalism for this task. We then appeal to specifications expressed as HOπ processes: they offer a basis on which interaction features in GC systems can be succinctly represented, and potentially verified using reasoning techniques over interacting processes. We thus extend the static description overviewed above so as to define in HOπ the behavior of GC components and their interactions according to the invariants and predicates of the static representation. Fig. 5 summarizes the correspondence between the elements in the static description and their respective process representation in the dynamic component of the model. In the figure, we use the symbol ֒→ to represent sub-processes which are triggered as part of the execution of a main process. Complete descriptions of the processes mentioned the figure can be found in [14]. Next we briefly describe process representations for some grid components (users, middleware, ADs) mentioned in Fig. 5. We use ω, µ, δ , and η to denote, respectively, the number of VOs, users, ADs, and nodes (access points) in the system. Also, we rely on standard process representations of queues (and associated operations) which can be easily encoded in HOπ via name passing (see, e.g., [17]). It is worth highlighting that the HOπ representations of the GC components are related to the invariants and other elements of the static component of the model. This means that process interactions do not concern arbitrary elements of the base sets; rather, they involve elements which may be subject to invariants. For example, our process representation for users only can interact with the process representation of a node that corresponds to a VO where such a user is member. Interestingly, key elements of the process language (notably, the exchange of fresh channels and scope extrusion) turn out to be useful to enforce the static invariants in the dynamic specification, and to rule out undesirable interferences among components (as in, e.g., two users which concurrently access a VO). This way, sensible correctness/consistency properties are ensured by construction. Establishing a formal correspondence between the static and dynamic components is part of ongoing work (see Sect. 6).
Grid system. A grid system is modeled as the composition of processes representation of users, ADs, and access points. These are denoted u, S c,y , d , and n v,y, d , respectively, which are used as intermediate notations for processes User( c, S t,e , y), AD(d), and AP(y, d), respectively. This structure promotes interaction: while user processes interact with access point processes through private channels y 1 , . . . , y η , AD processes communicate with access point processes in private channels d 1 , . . . , d δ . This way, our process model of a GC system, parametric on ω, µ, δ , and η, is the following: where I = {1, . . . , µ}, H = {1, . . . , η}, and L = {1, . . . , δ } are index sets over users, access points, and ADs, resp. In process User( c, S t,e , y) (defined below), S t,e is a process representation of task T (where S is a instance of T) that depends on names t and e: while t is used to send subtasks requirements to the appropriate user proxy, e is used to signal task completion. Given i ∈ I, we write node(u i ) to denote the index of the access point for user u i . Name d in AD(d) is used for interaction between the AD and access point processes. In AP(y, d), name y is used to interact with user processes, while d stands for a tuple with the access channel of the ADs in the VO associated to the access point. We write vo(n h ) to denote the VO associated to node n h .
Users. The process model for users, denoted User( c, S t,e , y), is parametric on a tuple of user credentials c, a task process S t,e (explained above), and a name y, which is used to access a grid node (an instance of process AP(y, d)). Process User( c, S t,e , y) interacts with node process AP y, d in order to authenticate to the grid, create a user proxy, and submit/monitor her task. More precisely, we have:  ( k, m, a, g).(AP-ProxyHandler ce, d | d j k, m, a, g )) Above, the first output on y represents an authentication request against a service deployed at AP(y, d). This service returns name ok (resp. denied) if the authentication is successful (resp. failed). We write u(ch 1 , −, m) to denote a reception of three arguments along u, in which the second one is not relevant. Name ch 1 is a private name communicated by AP(y, d): this enables the interference-free communication between user process and a subprocess of the grid node process. Also, ch 1 is used for user proxy creation and task submission: proxy creation is requested by an output signal on ch 1 ; then, a name a (to be used to access the user proxy) is received on ch 1 ; subsequently, the task can be sent: this is represented by the (higher-order) output prefix ch 1 S t,e . Once the task has been sent, a channel associated to the log of the submitted task is received on ch 1 , and process UsrMonitor( c, g, a, y, P) is launched: it abstracts the user interaction with her access point for monitoring the task just submitted. The last parameter for UsrMonitor, process P S , specifies the user behavior that is executed upon reception of the final result of her task. Such a process may correspond to, e.g., a query that stores such a result into a remote database.
Middleware. The middleware is represented as the composition of access point processes AP(y, d).
For each VO in the grid, there are some instances of access point processes associated to it. An instance of AP(y, d) interacts with an instance of User( c, S t,e , y) for authentication purposes, user proxy creation, and task submission/monitoring, as just explained. Then, process AP(y, d) launches a process AP-ProxyHandler(ce, d), given in Fig 6, which interacts with the user proxy process.
Process AP-ProxyHandler(ce, d) is parametric on (i) name ce, which is used to receive the task requirements from the user proxy process; and (ii) tuple d, which contains the names associated to the ADs of the VO of the access point. Once AP-ProxyHandler(ce, d) has received on ce the tuple k which represents the descriptors of the required grid resources, it selects the appropriate ADs for the requested resources. We abstract this selection by processes AP-Search K and AP-Acc. Given a tuple/set of resources descriptors K, each instance of process AP-Search K searches among the resources shared by an AD with resources satisfying the requirements in K. Once a suitable AD has been found, AP-Search K sends the access channel of that AD to AP-Acc, which records all such access channels. Once all instances of AP-Search K have completed the search, AP-Acc sends such ADs to process AP-ProxyHandler(ce, d) along name b. Then, AP-ProxyHandler(ce, d) non-deterministically selects an AD.
Administrative domains. As mentioned above, an AD is represented as process AD(d), which consists of the parallel composition of processes in charge of receiving, queuing, and attending task execution requests. Also, AD(d) comprises process models of resources and resource proxies (see below). For the sake of space, we only present the process AD-AsgRes(b, d, ch), which is in charge of assigning the appropriate resources for the subtasks assigned to the AD. This process, given in Fig. 7, is parametric Observe how also AD-AsgRes(b, d, ch) features higher-order communication in its interaction with task process S t,e . In fact, using a higher-order process communication on name o (not shown), the task process S t,e is expected to send a job to AD-AsgRes(b, d, ch)-which is denoted by process variable X . As soon as the reception on o takes place, process AD-AsgRes(b, d, ch) will execute the involved job.
User and Resource Proxies. We represent user proxies as instances of a process which receives the requirements of the subtasks of the user task process S t,e and submits such requirements to an access point process. Moreover, a user proxy process interacts with process AD-AsgRes(b, d, ch) which sends it the channels of the resource proxies of assigned resources. Finally, the user proxy process communicates with resources proxies process in order to authenticate and obtain the direct access to resources. Resource proxies are abstracted as a process which interacts with its associated resource process and instances of user proxy process. The interaction with its associated resource process allows the resource proxy to keep track of the state of the resource, as a resource notifies its proxy when a task has been completed.
Other components. In addition to the components described above, our process models also includes representations for other components in the GC system, namely logs processes, resource processes, and queue processes. There is a log process for each user task: it is in charge of registering the current state and the result of a task. Middleware processes (access points) interact to read the log when the user process requests it. In fact, processes AP-ProxyHandler(ce, d) and AP-UserProxy(ce, p,t, g) interact with the log process to register a new state and/or the final result. Resource processes abstract the behavior of actual grid resources. They interact with resource proxy process and task process S t,e . Finally, the queue process is a process representation of a queue structure. There is a queue process for each AD, which is used to store the subtasks requests of resources assigned to the AD.

Formalizing a Representative Grid Scenario
We now illustrate our formal model by instantiating it with the scenario presented in Sect. 2 (see also Fig. 2). The following table summarizes some of the corresponding base sets: User tasks For the sake of space, we do not present the static component of the model. Still, the description of the scenario given in Sect. 2 should provide an intuitive idea of the key valid relationships between the main grid components. We only highlight the fact that user tasks S 1 and S 2 are instances of task definitions T 1 and T 2 , respectively. As for the dynamic component of the model, following the notation given in Fig. 5, our scenario is represented by the following HOπ process: where ω = 2, µ = 2, δ = 2, and η = 2. By expanding the definitions of u, S c,y , n v,y, d , and d 1 , the above process can be equivalently stated as follows: Grid ω,µ δ ,η = (ν y 1 , y 2 ) (ν t 1 , e 1 ) User c 1 , S 1 t 1 ,e 1 , y 1 | (ν t 2 , e 2 ) User c 2 , S 2 t 2 ,e 2 , y 2 | To illustrate process evolution, we now describe a particular reduction sequence that originates from Grid ω,µ δ ,η . Precisely, we show the interactions that occur when the user u 1 accesses the grid for executing task S 1 . Clearly, (concurrent) interactions related to user u 2 are also possible, but below we restrict to comment on the reductions related to the process representation of u 1 .
First, we have a sequence of reductions Grid ω,µ δ ,η =⇒ GRID 1 , that represents the steps in which User c 1 , S 1 In process AP 1 (S 1 ) above, private name g w1 is used by processes AP-UserProxy ce 1 , a 1 ,t 1 , g w1 and AP-ProxyHandler ce 1 , d 1 , d 2 to register the changes in the state of task S 1 . Name ce 1 stands for the private channel on which these two processes may interact. At this point, we have the reduction sequence GRID 1 =⇒ GRID 2 , which represents reductions corresponding to the AD selection in the VO and the task submission to such an AD. In this case, we assume the AD d 1 is selected for the execution of the task. Process GRID 2 is as follows: GRID 2 ≡ (ν y 1 , y 2 ) UsrMonitor c 1 , g r1 , a 1 , y 1 , P | (ν t 2 , e 2 )User c 2 , S 2 t 2 ,e 2 , y 2 | where AP 2 (S 1 ) and AD 1 d 1 stand for residual processes for the access point and for the representation of AD d 1 , respectively. As above, RestSystem 2 stands for the composition of processes for the remaining components. In process AD 1 d 1 , the interaction between the task process and the user proxy process has evolved to S 1 1 and AP-UserProxy 1 , respectively. Processes AP 2 (S 1 ) and RestSystem 2 are as follows: AP 2 (S 1 ) ≡ S 1 1 | (ν g w1 , ce 1 )(AP-Log g w1 , g r1 , queued, null | e 1 ( r).g w1 state, finished .g w1 result, r | AP-UserProxy 1 | AP-ProxyHandler ce 1 , d 1 , d 2 )

Future Work
The process model of GC systems presented here describes basic interactions among grid main components, abstracting and enforcing essential static and dynamic properties of such systems. Establishing an operational correspondence result connecting the invariants in the static description and the HOπ reductions of the dynamic representation is part of ongoing work. We conjecture that HOπ processes representing the dynamic part preserve by construction the invariants defined by the static part. Slightly more formally, we conjecture that if process P respects the static invariants, and P −→ P then either (a) P ′ preserves the static invariants, or (b) there is a P ′′ such that P ′ =⇒ P ′′ and P ′′ preserves the static invariants. One of the challenges in the proof consists in giving a unified treatment to all invariants. Our current model does not take into account certain aspects typical of GC infrastructures, such as time. Still, as already mentioned, we think our current model is already a good basis for extensions: the inherent compositionality of process specifications should ease orthogonal improvements and refinements. In this sense, as future work, we plan to refine the model with locations (i.e., computation sites) and process failures. To this end, an initial approach would be using a calculus of adaptable processes [2], which enables to incorporate forms of runtime adaptation over located, interacting processes.
A strong motivation for pursuing a process calculi model of GC systems is that of exploiting the proof techniques over processes (behavioral equivalences, type systems) so as to reason about grid systems. That is, we would like to explore how our process model allows us to reason about correctness properties of GC systems. This involves, for instance, exploiting our model's compositionality and well-established theories of behavioral equivalence to reason about arbitrary behaviors in the grid setting. Also, we would like to reason about task termination and resource delivery in the grid setting. These properties are intrinsically related to reachability problems, and to issues of deadlock-and cycle-detection. We believe that a process calculi model offers a suitable basis also for investigating such problems.