Linas Kaminskas
email: linaskmnsks@gmail.com

Alberto Lluch Lafuente

Aggregation Policies for Tuple Spaces

Keywords: secure coordination, policy languages, privacy models, tuple spaces, aggregate programming

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Privacy is an essential part of society. With increasing digitalization of infrastructures grows their attack surface and the possibilities for abuse. It is therefore necessary to include privacy models that can scale with the complexity of those infrastructures and their software components, in order to protect information stored and exchanged while still ensuring information quality and availability. With EU GDPR regulation [START_REF]679 of the european parliament and of the council of 27 april 2016 on the protection of natural persons with regard to the processing of personal data and on the free movement of such data, and[END_REF] being implemented in all EU countries, regulation on how data acquisition processes handle and distribute personal information becomes enforced. This affects software development processes and life cycles as security-by-design choices will need to be incorporated. Legacy systems will also be affected by GDPR compliance. With time, these legacy systems will need to be replaced, not only because of technological advancements, but also due to political and social demands for higher quality infrastructure. No matter the perspective, the importance of privacy-preserving data migration, mining and publication will remain relevant as society advances.

Aggregation, privacy and coordination Aggregate programming methods are used for providing privacy guarantees (e.g. by reducing the ability to distinguish individual data items), improving performance (e.g. by reducing storage size and communications) and even as the basis of emergent coordination paradigms (e.g. computational field and aggregate programming based on the field calculus [START_REF] Viroli | A calculus of self-stabilising computational fields[END_REF][START_REF] Beal | Aggregate programming for the internet of things[END_REF] or the SMuC calculus [START_REF] Lluch-Lafuente | Asynchronous distributed execution of fixpoint-based computational fields[END_REF]). Basic aggregation functions (e.g. sums, averages, etc.), do not offer enough privacy guarantees (e.g. against statistical attacks) to support the construction of trustworthy coordination systems. The risk is that less users will be willing to share their data and, as a consequence, the quality of infrastructures and services based on data aggregations may degrade. More powerful privacy protection systems are needed to reassure users and foster their participation with useful data. Fortunately, aggregationbased methods can be enhanced by using well-studied privacy models that allow policy makers to trade between privacy and data utility. We investigate in this work how such methods can be easily integrated in a coordination model such as tuple spaces, that in turn can be used as the basis of aggregation-based systems. Motivational examples Of our main motivations is to address systems where users provide data in order to improve some services that they themselves may use. In such systems it is often the case that: (i) A user decides how much privacy is to be sacrificed when providing data. Data aggregation is performed according to a policy on their device and transmitted to a data collector. (ii) A data collector partitions data by some quality criterion. Aggregation is then performed on each partition and results are stored, while the received data may be discarded. (iii) A process uses the aggregated data, and shares results back to the users in order to provide a service.

A typical example of such systems are Intelligent Transport System (ITS), which exploit Geographic Information Systems (GIS) data from vehicles to provide better transportation services, e.g. increased green times at intersections, reduction of queue and congestion or exploration of infrastructure quality. As a real world example, bicycle GIS data is exploited by ITS systems to reduce congestion on bicycle paths, while maintaining individuals privacy. Figure 1 shows user positional data in different stages: (a) raw data as collected, (b) data after aggregating multiple trips, and (c) aggregated data with addition of noise to protect privacy. This aggregated data can then be delivered back to the users, in order to support their decision making before more congestion occurs. Depending on the background knowledge and insights in a service, an adversary can partially or fully undo bare aggregation. By using privacy models and controlling aggregate functions, one can remove sensitive fields such as unique identifiers and device names, and add noise to give approximations of aggregation results. This gives a way to trade data accuracy in favor of privacy. Fig. 2: A distance gradient field Another typical example are selforganizing systems. Consider, for instance, the archetypal example of the construction of a distance field, identified in [START_REF] Beal | Building blocks for aggregate programming of self-organising applications[END_REF] as one of the basic self-organization building blocks for aggregate programming. The typical scenario in such systems is as follows. A number of devices and points-of-interests (PoI) are spread over a geographical area. The main aim of each device is to estimate the distance to the closest PoI. The resulting distributed mapping of devices into distances and possibly the next device on the shortest path, forms a computational field. This provides a basic layer for aggregate programming applications and coordinated systems, as in e.g. providing directions to PoIs. Figure 2 shows an example with the result of 1000 devices in an area with a unique PoI located at (0, 0), where each device is represented by a dot and whose color intensity is proportional to the computed distance. The computation of the field needs to be done in a decentralized way, since the range of communication of devices needs to be kept localized. The algorithm that the devices use to compute the field is based on data aggregations: a device iteratively queries the neighbouring devices for their information and updates its own information to keep track of the closest distance to a PoI. Initially, the distance d i of each device i is set to the detected distance to the closest PoI, or to ∞ if no device is detected. At each iteration, a device i updates its computed distance d i as follows. It gets from each neighbour j its distance d j , and then updates d i to be the minimum between d i or d j plus the distance from i to j. In this algorithm, the key operation performed by the devices is an aggregation of neighbouring data, which may not offer sufficient privacy guarantees. For instance, the exact location of devices or their exact distance to a PoI could be inferred by a malicious agent. A simple case where this could be done is when one device and a PoI are in isolation. A more complex case could be if the devices are allowed to move and change their distances to a PoI gradually. By observing isolated devices and their interactions with neighbours, one could start to infer more about the behaviour of a device group.

Challenges Engineering of privacy mechanisms and embedding of these directly into large software systems is not a trivial task, and may be error prone. Therefore, it is crucial to separate privacy mechanisms from an application, in such a way that the privacy mechanisms can be altered without having to change the application logic. For example, Listing 1.1 shows a policy that a data hosting service will provide, and a program willing to use the data. The policy controls the aggregate query (aquery) of the program. It only allows to average (avg) some data and, in addition, it uses a add noise function to the result before privacy_policy:

noisy_average: aquery avg, data altered by result func add_noise ... Fig. 3 an assignment in the program occurs. In this manner, a clear separation of logic can be achieved, and multiple queries of the same kind can be altered by the same policy. Furthermore, it allows policies to be changed at run-time, in order to adapt to changes in regulations or to optimize the implementation of a policy. Separation of concerns provides convenience for both developers and policy makers alike.

Contribution Our goal is to develop a tool-supported policy language providing access control for which well-studied privacy models, aggregate programming constructs, and coordination primitives could be used to provide non-intrusive data access in distributed applications. We wanted to focus on an interactive setting where data is dynamically produced, consumed and queried, instead of the traditional static data warehousing that privacy models implementations tend to address. Our first contribution is a novel policy language in Section 2 to specify aggregation policies for tuple spaces. The choice of tuple spaces has been motivated by the need to abstract away from concrete data storage models and to address data-oriented coordination models. Our approach to the language provides a clean separation between policies that need to be enforced, and application logic that needs to be executed. The presentation abstracts away from any concrete tuple-based coordination language and we focus on aggregated versions of the traditional operations to add, retrieve and remove tuples.

Our second contribution (section 3) is a detailed description of how two well-studied privacy models such as k-anonymity and (ε, δ)-differential privacy can be expressed in our language. For this purpose, those models (which are usually presented in a database setting) have been redefined in the setting of tuple spaces. To the authors knowledge, this is the first time that the definition of those models has been adapted to tuple spaces.

Our third and last contribution (section 4) is an open-source, publicly available implementation of the policy language and its enforcement mechanism in a tuple space library for the Go programming language, illustrated with an archetypal example of a self-organizing pattern used as basic block in aggregate programming approaches [START_REF] Beal | Building blocks for aggregate programming of self-organising applications[END_REF], namely the above presented computation of a distance gradient.

A policy language for aggregations

We start the presentation of our policy language by motivating the need of supporting and controlling aggregate programming primitives, and present a set of such primitives. We then move into the description of our policy language, illustrate the language through examples, and conclude the section with formal semantics.

Aggregate programming primitives

The main computations we focus in this paper are aggregations of multiset of data items. As we have discussed in section 1, such computations are central to aggregate programming approaches. The main motivation is to control how such aggregations are performed: a data provider could want, for instance, to provide access to the average of a data set, but not to the data set or any of its derived forms. Traditional tuple spaces (e.g. those following the Linda model) do not support aggregations as first-class primitives: a user would need to extract all the data first and perform the aggregation during or after the extraction. Such a solution does not allow to control how aggregations are performed, and the user is in any case given access to an entire set of data items that needs to be protected. However, in databases, aggregate operators can be used in queries, providing thus a first-class primitive to perform aggregated queries, more amenable for access control. A similar situation can be found in aggregate programming languages that provide functions to aggregate data from neighbouring components: the field calculus offers a nbr primitive to retrieve information about neighbouring devices and aggregation is to be performed on top of that, whereas the SMuC calculus is based on atomic aggregation primitives.

We adapt such ideas to tackle the necessity of controlling aggregations in tuple spaces by proposing variants of the classical single-data operations put / out , get / in and qry / read . In particular, we extend them with an additional argument: an aggregation function that is intended to be applied to the multiset of all matched tuples. Typical examples of such functions would be averages, sums, minimum, concatenation, counting functions and so forth. While standard tuple space primitives allow to retrieve some or all tuples matching some template, the primitives we promote would allow to retrieve the aggregated version of all the matched tuples. More in detail, let's introduce the following aggregate programming primitives: aqry λ D ,U : This operation works similarly to an aggregated query in a database and provides an aggregated view of the data. In particular, it returns the result of applying the aggregation function λ D to all tuples that match the template U . aget λ D ,U : This operation is like aqry , but removes the matched data with template U . aput λ D ,U : This operation is like aget , but the result of the aggregation is introduced in the tuple space. It provides a common pattern used to atomically compress data.

It is worth to remark that such operations allow to replicate many of the common operations on tuple spaces. Indeed, the aggregation function could be, for instance, the multiset union (providing all the matched tuples) or a function that provides just one of the matched tuples (according to some deterministic or random function).

Syntax of the language

The main concepts of the language are knowledge bases in the form of tuple spaces, policies for expressing how operations should be altered, and aggregate programming operators. The language itself can be embedded in any host coordination language, but the primary focus will be in expressing policies. The language is defined in a way that is reminiscent of a concrete syntax for a programming language. Although, the point is not to force a particular syntax, but to have a convenient abstraction for describing the policies themselves. Further, the language and aggregation policies do not force a traditional access control based model by only permitting or denying access to data: policies allow transformations thus giving different views on the same data. This gives a choice to a policy maker to control the accuracy of the information released to a data consumer. Subjects (e.g. users) and contextual (e.g. location) attributes are not part of our language, in order to keep the presentation focused on the key aspects of aggregate programming. Yet, the language could be easily extended to include these attributes. The syntax of our aggregation policy language can be found in Table 1. Let Ω denote the types which are exposed by the host language and a type be τ ∈ Ω. For the sake of exposition we consider the simple case {int, float, string} ⊆ Ω. T is a knowledge base represented by a tuple space with a multiset interpretation, Tuple Space : where the order of tuples is irrelevant and multiple copies of the identical tuples are allowed. For T , the language operator ; denotes the multiset union, \ is the multiset difference and is the multiset symmetric difference. T contains labelled tuples, i.e. tuples attached a set of labels, with each label identifying a policy. A tuple is denoted and generated by u, and an empty tuple is denoted by ε. Tuples may be primed u or stared u to distinguish between different types of tuples. The type of a tuple u is denoted by τ u = τ u1 ×τ u2 ×. . .×τ un . In Section 3, individual tuple fields will be needed, and hence we will be more explicit and use u = (u 1 , . . . , u i , . . . , u n ), where u i denotes the i th tuple field with type τ ui . When dealing with a multiset of tuples of type τ u (e.g. a tuple space), the type τ * u will be used. For a label set V , a labelled tuple is denoted by V : u. Similarly as for a tuple, the empty labelled tuple is denoted by ε. A label serves as a unique attribute when performing policy selection based on an action A. A template U can contain constants c and types τ ∈ Ω and is used for pattern matching against a u ∈ T . As with tuples, we shall be explicit with template fields when necessary and use U = (U 1 , . . . , U i , . . . , U n ), where U i denotes the i th template field with type τ Ui . There are three main aggregation actions derived from the classical tuple space operations ( put , get , qry ), namely: aput , aget and aqry . All operate by applying an aggregate operator λ D on tuples u ∈ T that matches U . Aggregate functions λ D have a functional type λ D : τ * u → τ u and are used to aggregate tuples of type τ u into a tuple of type τ u . The composable policy Π is a list of policies that contain aggregation policies π. An aggregation π is defined by a policy label v and an aggregation rule H, where v is used as an identifier for H. An aggregation rule H describes how an action A is altered either by a template transformation D U , a tuple transformation D u , and a result transformation D a , or not at all by none . A template transformation D U is defined by a template operator λ U : τ U → τ U , and can be used for e.g. hiding sensitive attributes or to adapt the template from the public format of tuples to the internal format of tuples. A tuple transformation D u is defined by a tuple operator λ u : τ u → τ u . This allows to apply additional functions on a matched tuple u, and can be used e.g. for doing sanitization, addition of noise or approximating values, before performing the aggregate operation λ D on the matched tuples A result transformation D a is defined by a tuple operator λ a : τ u → τ u . The arguments of λ a are the same as for tuple transformations λ u , except the transformation is applied on an aggregated tuple. This allows for coarser control, say, in case a transformation on all the matched tuples is computationally expensive or if simpler policies are enough.

T ::= ∅ | V : u | V : u ; T Policy Label : v Policy Labels : V ::= ∅ | v | v , V Tuple : u ::= ε | c | u1 , u2 Template : U ::= ε | c | Ω | U1 , U2
Examples and comparison with a database Observe that λ D and any of the aggregation actions in A can provide all of the aggregate functions found in commercial databases, but with the flexibility of exactly defining how this is performed in the host language itself. The motivation for doing this comes from the fact that: (i) there is tendency for database implementations to provide non-standardized functionalities, introducing software fragmentation when swapping technologies, (ii) user-defined aggregate functions are often defined in a different language from the host language. In our approach, by allowing to directly express both the template for the data needed and aggregate functionality in the host language, helps reducing the programming complexity and improves readability, as the intended aggregation is expressed explicitly and in one place. Moreover, the usage of templates allows to specify the view of data at different granularity levels. For instance, in our motivational example on GIS data, one could be interested in expressing:

1. Field granularity where U contains concrete values only, but access is provided to some fields only. Listing 1.3 shows how to allow access to a specific data source by using U = ("devices", "gps", "accelerometer", "gyroscope") as a template of concrete devices. Here, id is the identity function, first is an aggregation function which returns the first matched tuple, and nth 2 selects the second field of the tuple.

1 accelerometer-data-only: 2 aqry first, "devices", "gps", "accelerometer", "gyroscope" 3 altered by 4 template func id 5 tuple func id 6 result func (fun x -> nth 2 x)

Listing 1.3: Example of field granularity policy.

2. Tuple granularity where U contains concrete values and all fields are provided. Listing 1.4 shows how a policy can provide access to a specific trip. In this case, it is specified by a trip type and trip identifier U = ("bike-ride", 1). Formal semantics Before presenting the formal semantics, we provide a graphical and intuitive presentation using A = aqry λ D , U and some T and Π as an example shown in Figure 5. The key idea is: 1. Given some action A, determine the applicable policy π. There can be multiple matches in Π; 2. extract the first-matching policy π with some label v; 3. extract template, tuple and result operators from transformations D U , D u , and D a respectively; 4. extract the aggregate operator λ D and apply U = λ U (U ); 5. based on the tuples V : u from T that match U and have v ∈ V : perform tuple transformation with λ u , aggregation with λ D , and result transformation with λ a .

The formal operational semantics of our policy enforcement mechanism is described by the set of inference rules in table 2, whose format is

P1 . . . Pi . . . Pn T , Π A → T , Π R
Fig. 5: Semantics of an aggregate action A given an applicable policy π.

where P 1 , . . . , P n are premises, T is a tuple space subject to Π, A is the action subject to control, and the return value (if any) is modelled by R. The return value may then be consumed by the host language. The absence of a return value denotes that no policy was applicable.

The semantics for applying a policy that matches an aggregate action aput λ D , U , aget λ D , U and aqry λ D , U is respectively defined by rules Agg-Put-Apply, Agg-Get-Apply and Agg-Query-Apply. For performing put V : u, Put-Apply is used. All three rules apply such transformation and differ only in that aget and aput modify the tuple space. A visual representation of the semantics of aput λ D , U , aget λ D , U and aqry λ D , U can be seen in Figure 5.

The premises of the rules include conditions to ensure that the right operation is being captured and a decomposition of how the operation is transformed by the policy. In particular, the set T 1 represents the actually matched tuples (after transforming the template) and T 2 is the actual view of the tuple space being considered (after applying the tuple transformations to T 1 ). It is on T 2 that the user-defined aggregation λ D is applied, and then the result transformation λ a is applied to provide the final result u a . Rules named Unmatched, Priority-Left, Priority-Left, and Priority-Unavailable take care of scanning the policy as list. It is up to the embedding in an actual host language to decide what to do with the results. For example, in our implementation, if the policy enforcement yields no result, the action is simply ignored.

Put-Apply:

Π = vπ : put U altered by result func λa match(u, U ) vπ ∈ V ua = λa(u) T = T ; V : ua T , Π put V : u → T , Π V : ua
Agg-Put-Apply:

Π = vπ : aput λ D , U altered by template func λ U tuple func λu result func λa match(U, U ) T1 = {V : u ∈ T | match(u, λ U (U )) ∧ vπ ∈ V } T = T \ T1 T2 = {V : λu(u) | V : u ∈ T1} ua = λa(λ D ({u | V : u ∈ T2})) T = T ; {vπ} : ua T , Π aput λ D , U → T , Π {vπ} : ua
Agg-Get-Apply:

Π = vπ : aget λ D , U altered by template func λ U tuple func λu result func λa match(U, U ) T1 = {V : u ∈ T | match(u, λ U (U )) ∧ vπ ∈ V } T = T \ T1 T2 = {V : λu(u) | V : u ∈ T1} ua = λa(λ D ({u | V : u ∈ T2})) T , Π aget λ D , U → T , Π {vπ} : ua
Agg-Query-Apply:

Π = vπ : aqry λ D , U altered by template func λ U tuple func λu result func λa match(U, U ) T1 = {V : u ∈ T | match(u, λ U (U )) ∧ vπ ∈ V } T2 = {V : λu(u) | V : u ∈ T1} ua = λa(λ D ({u | V : u ∈ T2}))
T , Π aqry λ D , U → T , Π {vπ} : ua

Unmatched:

Π = vπ : none ∨ (Π = vπ : A2 altered by D U Du Da ∧ A1 = A2) ∨ Π = 0 T , Π A1 → T , Π
Priority-Right:

T , Π1 A → T , Π1 T , Π2 A → T , Π 2 V : u T , Π1 ; Π2 A → T , Π1 ; Π 2 V : u Priority-Left: T , Π1 A → T , Π 1 V : u T , Π1 ; Π2 A → T , Π 1 ; Π2 V : u Priority-Unavailable: T , Π1 A → T , Π1 T , Π2 A → T , Π2
T , Π1 ; Π2 A → T , Π1 ; Π2

Privacy models

The design of our language has been driven by inspecting a variety of privacy models, first and foremost k-anonymity and (ε, δ)-differential privacy. We show in this section how those models can be adopted in our approach. The original definitions have been adapted from databases to our tuple space setting.

k-anonymity The essential idea of k-anonymity [START_REF] Samarati | Protecting privacy when disclosing information: kanonymity and its enforcement through generalization and suppression[END_REF][START_REF] Sweeney | k-anonymity: A model for protecting privacy[END_REF][START_REF] Machanavajjhala | l-diversity: Privacy beyond k-anonymity[END_REF] is to provide anonymity guarantees beyond hiding sensitive fields by ensuring that, when information on a data set is released, every individual data item is indistinguishable from at least k -1 other data items. In our motivational examples, for instance, this could be helpful to protect the correlation between devices and their distances from an attacker that can observe the position and number of devices in a zone and can obtain the list of distances within a zone through a query. k-anonymity is often defined for tables in a database, here it shall be adapted to templates U instead. We start by defining k-anonymity as a property of T : roughly, kanonymity requires that every tuple u cannot be distinguished from at least k -1 other tuples. Distinguishability of tuples is captured by an equivalence relation = t . Note that = t is not necessarily as strict as tuple equality: two tuples u and u may be different but equivalent, in the sense that they can be related exactly by the same, and possibly external, data. In our setting, k-anonymity is formalized as follows.

Definition 1 (k-anonymity). Let k ∈ N + , T be a multiset of tuples, and let = t be an equivalence relation on tuples. T has k-anonymity for = t if:

∀u ∈ T .|{u ∈ T U | u = t u}| ≥ k
In other words, the size of the non-empty equivalence classes induced by = t is at least k. We say that a multiset of tuples T has k-anonymity if T has kanonymity for = t being tuple equality (the finest equivalence relation on tuples). k-anonymity is not expected to be a property of the tuple space itself, but of the release of data provided by the operations aqry , aget and aput . In particular, we say that k-anonymity is provided by a policy Π on a tuple space T when for every query based on the above operations the released result u a (cf. Figure 5) has k-anonymity. Note that this does only make sense if the result u a is a multiset of tuples, which could be the case when the aggregation function is a multiset operation like multiset union. Policies can be used to enforce k-anonymity on specific queries. Consider for instance the previously mentioned example of the attacker trying to infer information about distances and positions of devices. Assume the device information is stored in tuples (x, y, i, j, d) where (x, y) are actual coordinates of the devices, (i, j) represents the zone in the grid and d is the computed distance to the closest PoI. Suppose further that we want to provide access to a projection of those tuples by hiding the actual positions and providing zone and distance information. Hiding the positions is not enough and we want to to provide 2-anonymity on the result. We can do so with the following policy:

2-anonymity: aqry mset_union, float, float, int, int, float altered by tuple func (fun x y i j d -> if anonymity(2) (i j d) else nil))

Listing 1.7: Example of k-anonymity for k = 2.

where anonymity(k) checks k-anonymity on the provided view T 2 (cf. Figure 5), according to Definition 1. Basically, the enforcement of the policy will ensure that we provide the expected result, if in each zone there are at least two devices with the same computed distance, otherwise the query produces the empty set.

(ε, δ)-differential privacy Differential privacy techniques [START_REF] Dwork | The algorithmic foundations of differential privacy[END_REF] aim at protecting against attackers that can perform repeated queries with the intention of inferring information about the presence and/or contribution of single data item in a data set. The main idea is to add controlled noise to the results of queries so to reduce the amount of information that such attackers would be able to obtain. Data accuracy is hence sacrificed for the sake of privacy. For instance, in the motivational example of the distance gradient, differential privacy can be used to the approximate the result of the aggregations performed by the gradient computation. This is done in order to minimize leakage about the actual positions and distance of each neighbouring device. Differential privacy is a property of a randomized algorithm, where the data set is used to give enough state information in order to increase indistinguishably. Randomization arises from privacy protection mechanisms based on e.g. sampling and adding randomly distributed noise. The property requires that performing a query for all possible neighbouring subsets of some data set, the addition (or removal) of a single data item produces almost indistinguishable results. Differential privacy is often presented in terms of histogram representations of databases not suitable for our purpose. We present in the following a reformulation of differential privacy for our setting. Let P[A(T ) ∈ S] denote the probability that the output A(T ) of a randomized algorithm A is in S when applied to T , where S ⊆ R(A) and R(A) is the codomain of A. In our setting A should be seen as the execution of an aggregated query, and that randomization arises from random noise addition.

(ε, δ)-differential privacy in our setting is then defined as the following property.

Definition 2 ((ε, δ)-differential privacy). Let A be a randomized algorithm, T be a tuple space, e be Euler's number, and ε and δ be real numbers. A satisfies (ε, δ)-differential privacy if and only if for any two tuple spaces T 1 ⊆ T and T 2 ⊆ T such that T 1 T 2 τu ≤ 1, and for any S ⊆ R(A), the following holds:

P[A(T 1 ) ∈ S] ≤ e ε • P[A(T 2 ) ∈ S] + δ
Differential privacy can be enforced by policies that add a sufficient amount of random noise to the result of the queries. There are several noise addition algorithms that guarantee differential privacy. A common approach is based on the global sensitivity of data set for an operation and a differentially private mechanism which uses the global sensitivity to add the noise. Global sensitivity measures the largest possible distance between neighbouring subsets (i.e. differing in exactly one tuple) of a tuple space, given an operation. The differentially private mechanism uses this measure to distort the result when the operation is applied. To define a notion of sensitivity in our setting, assume that for every basic type τ there is a norm function • : τ u → R which maps every tuple into a real number. This is needed in order to define a notion of difference between tuples. We are now ready to define a notion of sensitivity for a given aggregate operator λ D .

Definition 3 (Sensitivity). Let T be a tuple space, λ D : τ u → τ u be an aggregation function, and p ∈ N + . The p th -global sensitivity ∆ p of λ D is defined as:

∆ p (λ D ) = max ∀ T1,T2 ⊆ T T1 T2=1 p i∈{0,..,|τ u |} | λ D (T 1 ) i -λ D (T 2 ) i | p (1)
Roughly, Equation ( 1) is expressing that the sensitivity scale of an aggregate operator is determined by the largest value differences between all fields of the aggregated tuples. The global sensitivity can then be used to introduce Laplace noise according to the well-known Laplace mechanism, which provides (ε, 0)differential privacy.

Definition 4 (Laplace noise addition). Let T be a tuple space, λ D : τ * u → τ u be an aggregation function, ⊕ : τ u × τ u → τ u be an addition operator for type τ u , ε ∈ ]0, 1], p ∈ N + , and Y = (Y 1 , . . . , Y i , . . . , Y n ) be a tuple of random variables that are independently and identically distributed according to the Laplace distribution Y i ∼ L (0, ∆ p (λ D )/ε). The Laplace noise addition function laplace T ,λ D ,ε is defined by:

laplace T ,λ D ,ε (u) = u ⊕ Y (2)
Note that the function is parametric with respect to the noise addition operator ⊕. For numerical values ⊕ is just ordinary addition. In general, for ⊕ to be to be meaningful, one has to define it for any type. For complex types such as strings, structures or objects this is not trivial, and either one has to have a well-defined ⊕ or other mechanisms should be considered for complex data types. Consider again our motivational example of distance gradient computation, we can define a policy to provide differential privacy on the aggregated queries of each round of the computation as follows:

edp: aqry minD, float, float, int, int, float altered by result func (fun x y i j d -> (laplace minD 0.9 (x, y, d)))

Listing 1.8: Example of (ε, 0)-differential privacy policy.

The policy controls queries aiming at retrieving the information (x, y) coordinates, (i, j) zone and distance d of the device that is closest to a PoI, obtained by the aggregation function minD. The query returns only the coordinates of such device and its distance, after distorting them with Laplace noise by function laplace, implemented according to Definition 4 (with the tuple space being the provided view T 2 , cf. Figure 5). More in general, the enforcement of policies of the form aquery λD, U altered by template func DU tuple func Du result func (fun u -> (laplace λD ε u))

Listing 1.9: Schema for (ε, 0)-differential privacy policies.

provides (ε, 0)-differential privacy on the view of the tuple space (cf. T 2 in Figure 5) against aggregated queries based on the aggregation function λ D .

Aggregation policies at work

To showcase the applicability of our approach to aggregate computing applications, we describe in this section a proof-of-concept implementation of our policy language and its enforcement mechanism in a tuple space library (cf. Section 4.1), and the implementation of one of the archetypal self-organizing building blocks used in aggregate programming, namely the computation of a distance gradient field, that we use also to benchmark the library (cf. Section 4.2).

Implementation of a proof-of-concept library

The open-source library we have implemented is available for download, installation and usage at https://github.com/pSpaces/goSpace. The main criteria for choosing Go was that it provides a reasonable balance between language features and minimalism needed for a working prototype. Features that were considered important included concurrent processes, a flexible reflection system and a concise standard library. The goSpace project was chosen because it provided a basic tuple space implementation, and had the fundamental features, such as addition, retrieval and querying of tuples based on templates, and it also provides derived features such as retrieval and querying of multiple tuples. Yet, goSpace itself was modified in order to provide additional features needed for realizing the policy mechanism. One of the key features of the implementation is a form of code mobility that allows to transfer functions across different tuple spaces. This was necessary to serve as a foundation for allowing user-defined aggregate functions across multiple tuple spaces. Further, the library was implemented to be slightly more generic than what is given in Section 2 and can in principle be applied to other data structures beyond tuple spaces and aggregation operators on tuple space. Currently, our goSpace implementation supports policies for the actions aput , aget and aqry but it can be easily extended to support additional operations.

Protecting privacy in a distance gradient

We have implemented the case study of the distance field introduced in Section 1 as a motivational example. In our implementation, the area where devices and PoIs are placed, is discretized as a grid of zones; each device and PoI has a position and is hence located in a zone. The neighbouring relation is given by the zones: two devices are neighbours if their zones are incident. Devices can only detect PoIs in their own zone and devices cannot communicate directly with each other: they use a tuple space to share their information. Each device publishes in the tuple space their information (position, zone and computed distance) labelled with a privacy policy. The aggregation performed in each round uses the aqry operation with an aggregation function that selects the tuple with the smallest distance to a PoI. Different policies can be considered. The identity policy would simply correspond to the typical computation of the field as seen in the literature. Basically, all devices and the tuple space are considered to be trustworthy and no privacy guarantees are provided. Another possibility would be to consider that devices, and other agents that want to exploit the field, cannot be fully trusted with respect to privacy issues. A way to address this situation would be to consider policies that hide or distort the result of the aggregated queries used in each round.

Fig. 7: Gradient with noise

We have performed several experiments with our case study and we have observed, as expected, that such polices may affect accuracy (due to noise addition) and performance (due to the overhead of the policy enforcement mechanism). Some results are depicted in Figure 2, Figure 6 and Figure 7. In particular the figures show experiments for a scenario with 1000 devices and a discretization of the map into a 100 × 100 grid. Figure 2 shows the result where data is not protected but is provided as-it-is, while Figure 6 shows results that differ in the amount of noise added to the distance obtained from the aggregated queries. This is regulated by a parameter x so that the noise added is drawn from a uniform distribution in [-x * d, x * d], where d is the diameter of each cell of the grid (actually √ 10 * 10). In the figures, each dot represents a device and the color intensity is proportional to the distance to the PoI, which is placed at (0, 0). Highest intensity corresponds to distance 0, while lowest intensity corresponds to the diameter of the area ( √ 200). The results with more noise (bottom-right of Figure 6) make it evident how noise can affect data accuracy: the actual distance seems to be the same for all nodes. However, Figure 6, which shows the same data but where the color intensity goes from 0 to the maximum value in the field, reveals that the price paid for providing more privacy does not affect much the field: the gradient towards the PoI is still recognizable.

Conclusion

We have designed and implemented a policy language which allows to succinctly express and enforce well-understood privacy models in the syntactic category such as k-anonymity, and in the semantic category such as (ε, δ)-differential privacy. Aggregate operations and templates defined for a tuple space were used to give a useful abstraction for aggregate programming. Even if not shown here, our language allows to express additional syntactic privacy models such asdiversity [START_REF] Machanavajjhala | l-diversity: Privacy beyond k-anonymity[END_REF], t-closeness [START_REF] Li | t-closeness: Privacy beyond k-anonymity and l-diversity[END_REF][START_REF] Soria-Comas | t-closeness through microaggregation: Strict privacy with enhanced utility preservation[END_REF] and δ-presence [START_REF] Nergiz | δ-presence without complete world knowledge m. ercan nergiz[END_REF]. Our language does not only allow to adopt the above mentioned privacy models but it is flexible enough to specify and implement additional user-defined policies. The policy language and its enforcement mechanism have been implemented in a publicly available tuple space library. The language presented here has been designed with minimality in mind, and with a focus on the key aspects related to aggregation and privacy protection. Several aspects of the language can be extended, including richer operations to compose policies and label tuples, user-dependent and contextaware policies, tuple space localities and polyadic operations (e.g. to aggregate data from different sources as usual in aggregate computing paradigms). We believe that approaches like ours are fundamental to increase the security and trustworthiness of distributed and coordinated systems.

Related work

We have been inspired by previous works that enriched tuple space languages with access control mechanism, in particular SCEL [START_REF] De Nicola | The SCEL Language: Design, Implementation, Verification[END_REF][START_REF] Margheri | Linguistic abstractions for programming and policing autonomic computing systems[END_REF] and Klaim [START_REF] Hankin | Advice from belnap policies[END_REF][START_REF] Bruns | Access-control policies via belnap logic: Effective and efficient composition and analysis[END_REF]. We have also considered database implementations with access control mechanisms amenable for the adoption of privacy models. For example, [START_REF] Colombo | Fine-grained access control within nosql documentoriented datastores[END_REF] discusses the development strategies for FBAC (fine-grained access control) frameworks in NoSQL databases and showcases applications for MongoDB, the Qapla policy framework [START_REF] Mehta | Qapla: Policy compliance for database-backed systems[END_REF] provides a way to manipulate DBMS queries at different levels of data granularity and allows for transformations and query rewriting similar to ours, and PINQ [START_REF] Mcsherry | Privacy integrated queries: An extensible platform for privacypreserving data analysis[END_REF] uses LINQ, an SQL-like querying syntax, to express queries that can apply differential privacy embedded in C#. With respect to databases our approach provides a different granularity to control operations, for instance our language allows to easily define template-dependent policies. Our focus on aggregate programming has been also highly motivated by the emergence of aggregate programming and its application to domains of increasing interest such as the IoT [START_REF] Beal | Aggregate programming for the internet of things[END_REF]. As far as we know, security aspects of aggregate programming are considered only in [START_REF] Casadei | Combining trust and aggregate computing[END_REF] where the authors propose to enrich aggregate programming approaches with trust and reputation systems to mitigate the effect of malicious data providers. Those considerations are related to data integrity and not to privacy. Another closely related work is [START_REF] Floriano | Providing privacy on the tuple space model[END_REF] where the authors present an extension to a tuple space system with privacy properties based on cryptography. The main difference with respect to our work is in the different privacy models and guarantees considered.

Future Work One of the main challenges of current and future privacy protection systems for distributed systems, such as the one we have presented here, is their computational expensiveness. We plan to carry out a thorough performance evaluation of our library. We plan in particular to experiment with respect to different policies and actions. It is well known that privacy protection mechanism may be expensive and finding a right trade-off is often applicationdependent. Part of the overhead in our library is due to the preliminary status of our implementation where certain design aspects have been done in a naive manner to prioritize rapid prototyping over performance optimizations, e.g. use of strong cryptographic hashing, use of standard library concurrent maps and redundancies in some data structures. This makes room for improvement and we expect that the performance of our policy enforcement mechanism will be significantly improved. More in general, finding the optimal k-anonymity is an NP-hard problem. There is however room for improvements. For instance, [START_REF] Kenig | A practical approximation algorithm for optimal kanonymity[END_REF] provides an approximation algorithm. This algorithm could be adapted if enforcement is needed. An online differentially private algorithm, namely private multiplicative weights algorithm, is given in [START_REF] Dwork | The algorithmic foundations of differential privacy[END_REF]. Online algorithms are worth of investigation since interactions with T are inherently online. Treatment of functions and functional data in differential privacy setting can be found [START_REF] Hall | Differential privacy for functions and functional data[END_REF]. We are currently investigating online efficient algorithms to improve the performance of our library.

Fig. 1 :

 1 Fig. 1: Different stages of GIS data.

Listing 1 . 1 :Listing 1 . 2 :

 1112 An aggregation policy that adds noise to average-based queries An aggregated query subject to the policy in Listing 1.1.

  (a) Aggregated put: aput. (b) Aggregated get: aget. (c) Aggregated query: aqry.

Fig. 4 :

 4 Fig. 4: Aggregation primitives.

  Composable Policy : Π ::= 0 | π | π ; Π Aggregation Policy : π ::= v : H Aggregation Rule : H ::= none | put U altered by Da | A D altered by D U Du Da Action : A ::= A S | A D Simple Action : A S ::= put V : u Aggregate Action : A D ::= aput λ D , U | aget λ D , U | aqry λ D , U Template Transformation : D U ::= template func λ U Tuple Transformation : Du ::= tuple func λu Result Transformation : Da ::= result func λa Aggregate operator : λ D ::= sum | avg | min | max | . . . Template operator : λ U ::= id | pseudo i | collapse i | . . . Tuple operator : λu ::= id | collapse i | noise X | . . .

Fig. 6 :

 6 Fig. 6: Distance gradients with aggregation policies based on noise addition.

Table 1 :

 1 Syntax for policies and aggregate programming operators.

  Mixed granularity where U contains a mix of concrete values and types. Listing 1.5 shows how this could be used to protect user coordinates expressed as a triplet of float's encoding latitude, longitude, elevation while allowing a certain area. In this case, the copenhagen area is exposed, and computation of the average elevation with avg is permitted.

	2	aqry first, "bike-ride", 1 altered by
	3	template func id
	4	tuple func id
	5	result func id
		Listing 1.4: Example of tuple granularity policy.
	3. 1 alices-trips:
	2	aqry avg, "copenhagen", float, float, float altered by
	3	template func id
	4	tuple func (fun x -> nth 4 x)
	5	result func id
		Listing 1.5: Example of mixed granularity policy.
	1 map-partition:
	2	aqry count, float, float altered by
	3	template func id
	4	tuple func (fun (x y) -> area(x,y))
	5	result func id
	1 single-ride:

4. Tuple-type granularity where U contains only types. Listing 1.6 shows how this could be used to count how many points there are in each discretized part of a map, where area maps coordinates into areas. Listing 1.6: Example of tuple-type granularity policy. With respect to databases, the aforementioned granularities correspond to: 1. cell level, 2. single row level, 3. multiple row level, and 4. table level. Combined with a user-defined aggregate function λ D and transformations D U , D u and D a , one can provide many different views of a tuple space in a concise manner.

Table 2 :

 2 Semantics for action A under Π including the semantics format.


Eva Kühn
email: eva.kuehn@tuwien.ac.at

Sophie Therese Radschek
email: sophie.radschek@tuwien.ac.at

Nahla Elaraby
email: nahla.el-araby@tuwien.ac.at

Distributed Coordination Runtime Assertions for the Peer Model

Keywords: Coordination model, runtime assertions, distributed systems, tuple space

Major challenges in the software development of distributed systems are rooted in the complex nature of coordination. Assertions are a practical programming mechanism to improve the quality of software in general by monitoring it at runtime. Most approaches today limit assertions to statements about local states whereas coordination requires reasoning about distributed states. The Peer Model is an event-based coordination programming model that relies on known foundations like shared tuple spaces, Actor Model, and Petri Nets. We extend it with distributed runtime invariant assertions that are specified and implemented using its own coordination mechanisms. This lifts the concept of runtime assertions to the level of coordination modeling. The concept is demonstrated by means of an example from the railway domain.

Introduction

The development of coordination is complex because of the asynchronous nature of distributed systems. Coordination models like the Actor Model [START_REF] Agha | ACTORS: A Model Of Concurrent Computation In Distributed Systems[END_REF], Petri Nets [START_REF] Petri | Kommunikation mit Automaten[END_REF], Reo [START_REF] Arbab | Reo: A Channel-based Coordination Model for Component Composition[END_REF] and the Peer Model [START_REF] Kühn | Reusable Coordination Components: Reliable Development of Cooperative Information Systems[END_REF] are well suited to model the interactions in concurrent systems. They allow reasoning about coordination at a certain abstraction level. Such a model-driven approach has the advantage to specify the system unambiguously, and to support the verification of system properties. Assertions are a practical programming mechanism to improve the quality of software in general by monitoring it at runtime. Most approaches today limit assertions to statements about local states whereas coordination requires reasoning about distributed states.

The objective of this paper is to introduce event-based, asynchronous, and distributed runtime assertions to a coordination model. This approach shall lift the concept of runtime assertions to the level of coordination modeling. A main problem is to find a good tradeoff between a very costly mechanism and a good quality of verification. A further requirement is to provide a notation that is well integrated into the notation of the coordination model so that developers need not learn a different language. This way, the assertions can be directly added to the model of the application using the same modeling concepts. Keeping the number of concepts that a developer has to comprehend small contributes to usability [START_REF] Scheller | Automated measurement of API usability: The API Concepts Framework[END_REF].

We use the Peer Model (see Section 3) as reference coordination model notation and introduce an assertion mechanism based on its own modeling language. Checking of distributed assertions can in turn be considered a coordination problem. We propose therefore model transformation algorithms that automatically translate the assertion specifications into coordination constructs of the model. Thus they become part of the application model and can be implemented with the same mechanisms. In this way, the extended Peer Model is a contribution towards verification of practical distributed systems.

The paper is structured as follows: Section 2 summarizes related work on distributed assertion mechanisms. Section 3 gives an overview of the Peer Model. In Section 4 we extend the Peer Model by distributed runtime invariant assertions that are specified and implemented using its own coordination mechanisms. In Section 5 the concept is demonstrated by means of an example from the railway domain. Section 6 summarizes the results and Section 7 gives an outlook to future work.

Related Work

Proper assertions for verification of coordination models should be declarative, event-driven and distributed. Assertions express correctness properties that must hold in all system states. Coordination model assertions should be model-based and use the same or similar notation of the model to keep the number of concepts small. For concurrent distributed systems, run time assertions [START_REF] Din | Runtime assertion checking and theorem proving for concurrent and distributed systems[END_REF] provide high confidence that the properties to be verified are fulfilled. However, assertions in this case should be of asynchronous nature so that they neither disturb the execution nor interfere with user code and data by any means. They should be bootstrapped for implementation with native model mechanisms.

[9] introduces a solution for coordinating activities of multiple intelligent agents using the tuple space computational model. The tuple space-based problem solving framework is implemented on an Intel Hypercube iPSC/2 allowing multiple rule-based systems concurrently performing their dedicated interrelated tasks. Their approach to build a rule-based system resembles our approach towards distributed assertions, but on a different level of reasoning.

A language for determining correct behavior in distributed systems is described in [START_REF] Tjang | A: An assertion language for distributed systems[END_REF]. This approach succeeds to verify distributed systems but introduces a different language and notation. Also, waiting states for operators' actions add much overhead to the run time check which is not acceptable in most systems, especially those of safety-critical nature.

Reusable assertions were developed in [START_REF] Kasuya | Verification methodologies in a tlm-to-rtl design flow[END_REF], where the assertions can be used at different abstraction levels. The approach handles the timing but does not provide asynchronous assertions for distributed system modules.

In [START_REF] Khosravi | Modeling and analysis of reo connectors using alloy[END_REF] a lightweight modeling language (Alloy), based on first-order relational logic is used to model and analyze Reo connectors. Reo [START_REF] Arbab | Reo: A Channel-based Coordination Model for Component Composition[END_REF] is a coordination language based on components and connectors. The model presented in this work preserves the original structure of the Reo network, avoiding a complex translation effort. The approach handles basic channel types, compositional construction of more complex connectors, constraints on the environment, and networks exposing context-sensitive behavior. However, in Alloy, no asynchronous assertion mechanism is provided and the properties are defined in terms of first-order predicates, and not in the same model notation. [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF] investigates runtime verification where the properties are expressed in linear time temporal logic (LTL) or timed linear time temporal logic (TLTL). Runtime verification is identified in comparison to model checking and testing. A three-valued semantics (with truth values true, false, inconclusive) is introduced as an expressive interpretation indicating whether a partial observation of a running system meets an LTL or TLTL property. For LTL, a minimal size deterministic monitor is generated identifying a continuously monitored trace as either satisfying or falsifying a property as early as possible, similarly for TLTL. The approach is successful and provides foundation for real-time monitoring of system properties. The approach does not provide asynchronous assertions and uses a different notation from the model.

Mining of the simulation data as an effective solution for generation of assertions is presented in [START_REF] Chao | On evaluating and constraining assertions using conflicts in absent scenarios[END_REF]. The research provides an efficient way to develop a highly trusted set of assertions and solves the incompleteness problem of Assertion Based Verification (ABV). The assertions are not based on the model notation and need effort of the developer to integrate them into the runtime. Distributed asynchronous mechanisms for assertions are not provided.

The work presented in [START_REF] Newsham | Intersert: Assertions on distributed process interaction sessions[END_REF] investigates the realization of infrastructures to maintain and access data and use it in assertions. Assertions can be managed across distributed system to support sophisticated assertions for intercommunications in distributed systems. A tool-chain is provided for programming assertions on interaction history written in regular expressions that incorporate inter-process and inter-thread behavior amongst multiple components in a distributed system. The mechanism is promising but not model-based.

A novel approach described in [START_REF] Wang | Assertion recommendation for formal program verification[END_REF] uses machine learning for automatic assertion generation. The approach releases the burden of manually specifying the assertions, which is a time-consuming and error-prone process. Similarly the authors of [START_REF] Pham | Assertion generation through active learning[END_REF] also deal with the problem of insufficiently written assertions and propose an automatic approach for assertion generation based on active learning. The approach targets complex Java programs, which cannot be symbolically executed. Test cases are used as a base for assertion generation and active learning to iteratively improve the generated assertions is applied. Both approaches are runtime-based and automatic, but they are not applicable for distributed systems where coordination needs to be defined and asserted asynchronously to validate the system functionality.

[8] introduces runtime verification as a complementary validation technique for component-based systems written in the BIP (Behavior, Interaction and Priority) framework. The proposed solution dynamically builds a minimal abstraction of the current runtime state of the system so as to lower the overhead. Monitors are directly generated as BIP components where the C code generator of BIP generate actual monitored C programs and remain compatible with previously proposed runtime verification frameworks. However, an adaptation layer is needed to adapt monitors generated by other existing tools.

A general approach to monitor the specifications of decentralized systems is presented in [START_REF] El-Hokayem | Monitoring decentralized specifications[END_REF]. The specification is considered as a set of automata associated with monitors attached to different components of the decentralized system. A general monitoring algorithm is developed to monitor the specifications. Execution History Encoding (EHE) data structure is introduced as a middle ground between rewriting and automata evaluation. Rewriting is restricted to Boolean expressions, parameters are determined and their respective effect on the size of expressions and the upper bounds are fixed. A similar decentralized algorithm for runtime verification of distributed programs is introduced in [START_REF] Mostafa | Decentralized runtime verification of ltl specifications in distributed systems[END_REF]. The technique works on asynchronous distributed systems, where a global clock is not assumed. The specification language used is full LTL so that temporal properties can be monitored. The algorithm can also determine the verification verdict once a total order of events in the system under inspection can be constructed. The presented algorithm addresses shortcomings in other algorithms as it does not assume a global clock, is able to verify temporal properties and is sound and complete. However, the main concern is the large number of monitoring messages introducing an increased communication and memory overhead. [START_REF] Kamburjan | Session-based compositional analysis for actor-based languages using futures[END_REF] proposes a session-based verification framework for concurrent and distributed ABS models. Applications are categorized with respect to the sessions in which they participate. Their behaviors are partitioned based on sessions, which include the usage of future. The presented framework extends the protocol types through adding terms suitable for capturing the notion of futures, accordingly the communication between different ABS endpoints can be verified by the corresponding session-based composition verification framework. Timing is handled but not in an asynchronous way.

In summary, none of the listed approaches provides assertions that are specified at the model level, are runtime-based, asynchronous and distributed, and the implementation of which can be bootstrapped with native model mechanisms. The motivation was therefore to use the Peer Model (see Section 3) as reference coordination model notation and to provide a full set of assertions that can be translated to the same model notation, whereby all mentioned requirements for assertions are fulfilled. This way, the intent is to extend the Peer Model to become capable to trustfully monitor distributed systems.

The Peer Model in a Nutshell

The Peer Model [START_REF] Kühn | Reusable Coordination Components: Reliable Development of Cooperative Information Systems[END_REF] is a coordination model that relies on known foundations like shared tuple spaces [START_REF] Gelernter | Generative Communication in Linda[END_REF][START_REF] Gelernter | Coordination Languages and Their Significance[END_REF][START_REF] Kühn | Introducing the Concept of Customizable Structured Spaces for Agent Coordination in the Production Automation Domain[END_REF], Actor Model [START_REF] Agha | ACTORS: A Model Of Concurrent Computation In Distributed Systems[END_REF], and Petri Nets [START_REF] Petri | Kommunikation mit Automaten[END_REF]. It clearly separates coordination logic from business logic and is well suited to model reusable coordination solutions in form of patterns. It provides a refinementbased modeling approach where you start with the highest abstraction layer of your application model, and stepwise improve the model3 . The main concepts are briefly explained in the following.

Peer. A peer relates to an actor in the Actor Model [START_REF] Agha | ACTORS: A Model Of Concurrent Computation In Distributed Systems[END_REF]. It is an autonomous worker with in-and outgoing mailboxes, termed peer input container (PIC) and peer output (POC) container.

Container. A container is a sub-space in the tuple space that stores entries that are written, read, or taken (i.e., read and removed) in local transactions.

Entry. Entries are the units of information passed between peers. An entry has system-and application-defined properties, which are name/value pairs. Examples for system-defined properties are e.g.: ttl (time-to-life; if it expires, the entry becomes an exception entry that wraps the original entry), and fid (flow id). All entries with the same fid belong to the same flow, i.e., they logically belong together. An exception entry is a special system-defined entry. If it is caused by the expiration of an entry ttl it inherits the fid of the entry causing the exception, and "wraps" the original entry in a property termed entry. The type of the exception is stored in the excType property.

Link. A link transports entries between two containers c1 and c2. It selects entries from c1 using a query. Link operations are move (take entries from c1 and write them to c2), copy (read entries from c1 and write them to c2), test (read entries from c1), delete (read and remove entries from c1), create (create entries of given type and count and write them to c2), and no operation specified (no container access; this link serves solely to perform tests on variables). A link can set or get variables (see below) and set or get properties of entries (if an operation was used that selected entries from c1). In these expressions also system-defined functions like head() (get first element of a list), tail() (get rest of a list) can be used. Finally, a link may have system-defined properties, e.g., dest (peer to whose PIC all selected entries shall be sent), and mandatory (flag whether the link is obligatory).

Wiring. The coordination behavior of a peer is explicitly modeled with wirings, which have some similarity with Petri Net transitions [START_REF] Petri | Kommunikation mit Automaten[END_REF]. All wiring specifications are executed concurrently in so-called wiring instances. Each instance has an internal container termed Wiring Internal Container (WIC), which serves as a temporary, local entry collection. Each wiring instance is a local transaction [START_REF] Kühn | Flexible transactional coordination in the peer model[END_REF] that transports entries between containers with help of links. A link from a PIC or POC to the WIC is termed "guard" (G) and a link from the WIC to a PIC or POC is termed "action" (A). The operational behavior of a wiring instance is the sequential execution of guards, and actions. The arrival of entries in peer space containers triggers the execution of guards. A wiring is triggered if all of its guard links are satisfied. Wirings also have system-defined properties. Each instance of a wiring obtains a new WIC. Wirings can treat exceptions.

Query. A query consists of: (1) entry type (mandatory), ( 2) an integer number (default is 1) specifying how many entries shall be selected, or ALL (all entries in the container that can be read or taken, possibly 0), and (3) a selector expression. It is fulfilled when enough entries with specified type match the selector. It selects entries with same type and of compatible flows [START_REF] Kühn | Reusable Coordination Components: Reliable Development of Cooperative Information Systems[END_REF]. The first link of a wiring determines the flow. All further links select only entries with same fid, or not fid set. A selector can use AND, OR and NOT operators.

Variable. There exist application-and system-defined variables. The former are denoted with "$" and used in the scope of a wiring instance. The latter are denoted with "$$" and set by the runtime, e.g., $$PID (id of the current peer), $$WID (id of the current wiring), $$CNT (number of entries selected by a link query), and $$FID (current flow id of the wiring instance).

Fig. 1 shows the graphical notation of the core concepts. It depicts one peer with id P1 and one wiring termed W1. The wiring possesses two guard links (G1, G2), and two action links (A1, A2) -represented by arrows. G1 (connecting PIC and WIC) depicts the general notation: Operation, query and the access to variables and entry properties are located above the respective arrow and properties are denoted below. Guard links are directed towards the WIC, and action links are pointing in the other direction. If entries are read (and removed) from a container, then the arrow base is connected to it; if entries are written into a container, then the arrow head is connected to it. Otherwise, a vertical bar is used on the respective side to indicate that no entries "go through".

G2 shows a guard link that takes one entry of type status from the PIC, using a selector specifying that the val property of the entry must be set to free, and writes the entry into the WIC. It stores the from and to properties of the selected entry in local variables $from and $to. In action link A1 the wiring takes the above mentioned status entry from the WIC, swaps its to and from properties with help of the local variables, and writes it back to the PIC. A2 creates one new entry of type info, and as the link property dest is set, the entry is sent to the PIC of the destination address, in this case the Operator peer. If dest is set, the arrow of the link goes through the POC. All system-defined terms are written in type writer style.

Introducing Peer Model Assertions

To improve the quality of specifications at the modeling level, the Peer Model is augmented with declarative invariant assertions. The goal of the assertion mechanism is to detect model inconsistencies at runtime. The trade-off between interference with normal execution, network traffic, and strict evaluation of assertions should be configurable. The mechanism shall be distributed, asynchronous and event-driven, assuming neither reliable nor ordered communication.

Assertions are statements about container states, because the shared coordination state of the distributed system is manifested in them. They follow the same principles as the Peer Model concepts (see Section 3), e.g., they have properties, are flow sensitive, and cause exception entries to be treated by the application. The consideration of the flow is fundamental, because the scope of each assertion check is restricted to one flow. This has the advantage that the correlation of distributed events can fully rely on the Peer Model's native flow mechanisms. Peers are assumed to report about assertion violations to one or more coordinators, which are peers in charge of controlling the assertion checking for a particular flow. Reporting considers actual and past states; liveness is out of scope of this mechanism.

We differentiate between assertions referring to containers of one single peer only (intra-peer assertions) and assertions involving multiple (local or distributed) peers (inter-peer assertions). For the former, violations are checked autonomously by the peer itself, for the latter, violation checking is understood as a distributed coordination problem. The proposed mechanism includes a translation of the declarative assertions to existing Peer Model constructs by a model translation algorithm (MTA) (see Section 4.1). For intra-peer assertion checks, respective wirings are statically added to the meta-model of the peers that monitor their local container states and create assertion exception entries on violation. The inter-peer assertion mechanism relies in principle on the same wiring type, but instead of exceptions, report entries are created and sent to coordinators, which in turn decide if exceptions must be created based on the status of received reports. Therefore, the overall assertion check can be reduced to an analogous wiring that checks a derived and normalized intra-peer assertion about these reports, generated by the MTA.

The required overhead consists only of carrying out the required tests when a new relevant event is received, storing the current reporting state and (in the inter-peer case) sending one report message to each coordinator on a new assertion violation. However, not all violations can be detected in case of communication failures. To cope with these issues and to support assertions about past states, a history of the relevant events can be maintained in a dedicated internal peer container termed HIC. This history is created by extending the existing application wirings to capture all local changes and deletions of entries referenced by assertions in the HIC, which creates a certain overhead. However, the overhead can be reduced by deleting events that cannot be referenced any more by active assertions (e.g. a flow has expired), assigning time-to-live properties and introducing bounds on the depth of the history.

The expressiveness of the mechanism can be further enhanced by introducing variables shared between different sub-assertions (see below) of inter-peer assertions. This produces additional message overhead, as reports about property changes in relevant entries must be sent to all respective wirings that reference these properties by means of these variables. Variable reports are only sent, if the corresponding assertion is not violated, because -like in failing optional links -variables can only be assumed to have meaningful value, if the expression that sets them was successful. In addition, assertion wirings depend on variable reports to be present and are activated by each new variable report. The mentioned trade-off between strictness and expressiveness versus overhead is controlled by the assertion model. Namely, avoiding inter-peer variables, and not using assertions about the past and not demanding a history reduces the overhead to a minimum. The coordinator(s) for inter-peer assertions are specified by means of assertion properties. Default is no coordinator, meaning that each sub-assertion creates local exceptions instead of sending reports to coordinators; the logic of how to handle them can be explicitly modeled. Here, the trade-off is between many coordinators with a larger message overhead and fewer coordinators leading to a potential bottle-neck and single point-of-failure.

The syntax of assertions is given in Tab. 1 and their operational semantics is defined with existing Peer Model constructs. An assertion is either a simple one (SAss) or a complex one (CAss), i.e., sub-assertions connected with logic operators AND, OR, NOT and → (equivalent to ∧, ∨, ¬ and =⇒ ). Sub-assertions of inter-peer assertions are intra-peer assertions and sub-assertions of intra-peer assertions are container assertions. Container assertions are satisfied, if the container contains exactly quantor entries of type that satisfy the query selector sel. Note that type sel and set/get refer to the Peer Model's link notation (see Fig. 1). Intra-and inter-peer assertions are satisfied if the propositional formula corresponding to the assertion -in which the propositions are the sub-assertions -is satisfied.

Model Translation Algorithm (MTA)

Intra-peer assertions are translated into single wirings located in the peer(s) corresponding to the context. Each assertion corresponds to a wiring that checks its truth value and raises an exception on violation. Such assertion wirings define and use all variables used in the corresponding assertion and overhead variables to evaluate the truth value of the assertion. These overhead variables are: 1 variable for each container sub-assertion to store the evaluation value, 2 variables Table 1. EBNF for Assertion Notation.

for each container sub-assertion to store the number of entries that fit the type and query, 1 to store the overall assertion value and 1 to store whether a violation must be reported. The assertion and overhead variables are initialised on a dedicated mandatory guard. Each container sub-assertion is tested using 3 guards: (1) tests how many entries there are in the container that fulfil the query of the assertion and saves the number in a variable; this guard also sets the variables used by the assertion. (2) tests how many entries there are in the container that fulfil the type of the assertion. (3) compares the quantities for (1) and ( 2) according to the quantor in the container sub-assertion and sets the corresponding truth variable to true if it is fulfilled. ( 1) and ( 2) are mandatory, (3) is only executed if the sub-assertion is asserted. The truth value of the overall assertion is set to true on an optional guard according to the logic formula of the intra-peer assertion. If the overall intra-peer assertion is violated and no report has yet been issued, a report is created in the peer input container (PIC) and an exception is raised in the peer output container (POC). Each intra-peer assertion creates an overhead of k wirings with 3n + 2 variables and 3n + 5 links each (n . . . # of container sub-assertions and k . . . # of peers in the context). For each violation, 2 additional entries are created.

Fig. 2 shows the translated wiring of an intra-peer assertion. G1 defines a variable $q i for the result of each ContainerAss (see Tab. 1), a variable $q for the result of the entire PeerAss, a variable $report to reflect whether the assertion has already been reported, and initializes all application variables of the wiring, if any. G1 is created once per wiring. Gj.k (j = 2, ..., n+1, k = 1 , 2, 3) are generated for each of the n ContainerAss: Gj.1 tests all entries fulfilling type and sel (see Fig. 1) of the assertion query and saves their count in the variable $c j . Gj.2 counts all entries that fulfill the type of the assertion query and saves the value in the variable $ca j which is needed for the quantifier check. Gj.3 checks whether the right quantity of entries satisfies the sel by comparing $c j , $ca j and the quantor in the ContainerAss as follows: (quantor == ALL AND $c j = $ca j ) OR (quantor == NONE AND $c j == 0 ) OR ($c j == quantor ). Gn+2 sets the variable $q to the result of the overall assertion based on the values of $q 1 , . . ., $q n . Gn+3 checks whether an assertion violation has already been reported for this wiring and flow, which is the case if an assReported entry exists in the PIC. If the assertion is violated and has not been reported yet, A1 creates an assReported entry for the wiring and flow in the PIC. If the assertion is violated and has not been reported yet, A2 creates an exception with type ASSERTION for the wiring and flow in the POC.

Inter-peer assertions are translated analogously: Sub-assertions (intra-peer assertions) are treated individually and the overall inter-peer assertions evaluated by coordinators based on the evaluation value of the sub-assertions.

The sub-assertions are translated into intra-peer assertion wirings. But instead of raising exceptions, they send violation reports to coordinators when the evaluation value might cause the overall assertion to fail. The differences are reflected in A2, which creates an assReport entry and sends it to all coordinators, and in the selector of Gn+2, which is inverted for negated assertions with quantor ALL and non-negated assertions with quantor NONE in the context.

The overall assertion is evaluated in dedicated wirings in coordinators that collect the corresponding sub-assertion values and combine them according to the propositional formula of the overall assertion. The resulting wiring is analogous to an intra-peer assertion wiring where the sub-assertions are checks on the number of assertion reports sent by other peers. Variable initialization, evaluation of the propositional skeleton, keeping track of violations and raising of exceptions is analogous to intra-peer wirings. For each sub-assertion, the number of reports sent by peers is counted (G2.1) and the numbers are compared ac- cording to the quantor and the variable set to true if the sub-assertion is fulfilled (G2.2). See Fig. 3 for the corresponding wiring.

Inter-peer assertions introduce c overall evaluation wirings (c . . . # of coordinators) with 2m + 5 links and 2m + 2 variables each (m . . . # of sub-assertions) and m 1 k i intra-peer assertion wirings (k i . . . # of peers in the context for each sub-assertion) with 3n i + 5 links and 3n i + 3 variables (n i . . . # of container subassertions in the respective sub-assertions). For each violation at most m 1 k i messages are sent and 2c + m 1 2k i entries are created. The use of HIC adds additional links to each wiring that modifies or deletes entries for which a HIC entry is assumed: The wiring gets additional links to retrieve, update and write back sequence numbers from the HIC for an overall sequence number (os) and a type sequence number (ts). ( 1) if the entry is taken from the container, modified and written back or written to another container, a copy of the entry as seen in the WIC is written to the history with ts and os set, and (2) if the entry is deleted, the delete is replaced by a move and it is subsequently moved into the HIC with ts and os set. All history entries of a wiring instance are assigned the same sequence numbers. l + 4 additional links and 2 new variables are added to each wiring that modifies or deletes entries that must be kept in the history (l . . . # of links that modify or delete entries relevant for the history).

Variables can be shared between sub-assertions. In that case, the wiring for the assertion that sets the variable, must get additional logic to report the values. The wirings for assertions that read the variables, must treat the variable reports and set their local wiring variables accordingly. For positive sub-assertions in the CNF, reports are sent if the corresponding assertion did not fail, for negated ones, they are sent if the assertion failed. Variables shared between contexts introduce an overhead of

Proof-of-Concept: Railway Use Case

The selected use case refers to the reservation of rails (cf. [START_REF] Abrial | Train Systems[END_REF], [START_REF] Reichl | Using formal methods for verification and validation in railway[END_REF]). A block is either a track or a point (see Fig. 4). It has a unique identifier (id). A track has 2 connectors. A point has 3 connectors. A connector references a connector of another Block. A signal refers to a main signal; its value is red or green. It is valid at the exit of the Block and associated with a connector (dependent on the direction). A route is a sequence of connected Blocks. A reserved route is a route where all Blocks are exclusively reserved for this route.

Three scenarios are selected: (1) Reserve Route: Mark all Blocks Block 1 , . . ., Block N for a route in the specified order. Check that the neighbor Blocks are physically connected via connectors, and set their direction appropriately. (2) Set Signals: Set signals on Blocks of a reserved route.

An example for a physical configuration of tracks is shown in Fig. 5. Each Block knows to which neighboring Blocks it is connected. The challenge is that there may exist many train Operators who try to reserve routes concurrently (see red and blue routes in Fig. 5). It must not happen that a safety constraint is violated (see informal specification of required assertions in Tab. 2). These assertions for the example use case were provided by a railway expert.

We assume that the Operator defines a ttl within which the route must be reserverd. If not, the reservation fails, and the Operator issues the freeing of the already reserved Blocks of the route. The reservation of a route, the setting of signals of Blocks of the reserved route, and the freeing of the route belong to the same flow.

The Model

The Peer Model based representation is presented in the following using the graphical notation. Entries: The entries used in the example are categorized into entries that represent the state of the distributed system, and entries that represent events which are sent between the peers as requests and answers. "bid" stands for Block id, and "cid" for connector id.

State Entries:

config:

• btyp: track or point • b1: bid of neighbor Peers: We define two kinds of peer roles: Block and Operator. Each track and point is modeled as a Block with unique block id. It accepts commands to change status, set signals and direction. The task of an Operator is to issue the setting of Block directions, the reservation and freeing of routes, and the setting of signals on reserved routes. All Operators act concurrently. Wirings: Figures 67show the wirings of Block peers. Init: The initialization wiring (Fig. 6) is enabled exactly once when the Block peer is created. It creates entries to hold the local status (A1), signals (A2), and config (A3) and writes them to the peer's PIC. Initially the status is free and does not belong to a flow, all signals are set to red, and the configuration of the Block is set based on the given peer's configuration parameters.

SetSignals: This wiring (Fig. 6) sets the signals, provided that the Block is reserved for the current flow. It is triggered by receipt of a setSignals entry which it deletes from the PIC (G1). In (G2) it tests that its status says that it is reserved for this flow. In (G3) it takes the signals entry from the PIC and in (A1) writes the updated signals entry back to the PIC.

The marking of a route consists of the following wirings. Depending on the action of markRoute, the Blocks are either reserved of freed within a flow.

ReserveRoute (see Fig. 7) reacts on the receipt of a markRoute event in its PIC. We assume that a markRoute entry sent by an operator contains a valid route and has its ttl (time-to-live) property set. It checks that it has not been treated yet (i.e., the done flag is false), that the action is to reserve the route, remembers the sender in the variable $s, the next Block of the route in the variable $snext (G1), and initializes two variables $f and $t to empty. It takes its status entry (G2) from PIC, tests that in its configuration the val property equals free (G2). G3 tests the existence of one config entry in the PIC and remembers its properties in local variables termed $b1, $b2 and $b3. G4 initializes the local variables $f and $t to contain the connector id of the sender (if it was not the operator, i.e., sender is empty), and to the connector id of the next block. It updates the value of the status entry to be reserved, sets its flow id to the current flow, and the from and to properties to the respective connector ids (A1). Finally, it sets the done flag on the markRoute entry to true (A2) to denote that the status has been updated.

FreeRoute frees a reserved route. Its model is similar to ReserveRoute, with the only difference that it needs not check that the block was free before and updates the signals entry. It is therefore not shown.

EndOfRoute (see Fig. 7) fires after the Block's status has been set by Re-serveRoute (i.e., done is true) and if the route has been completely treated, i.e., the route is empty (G1). It sends the reply entry ackRoute to the requesting Operator, provided that the action was to reserve the route. Otherwise no reply is sent (A1). Therefore the action link is not mandatory.

ContinueRoute (see Fig. 7) fires after the Block's status has been set by ReserveRoute and recursively processes the rest of a not yet empty route (G1). It sends the directive to mark the rest of the route to the next Block found in the route (A1), i.e., the head of the current route.

RouteTimeout (see Fig. 7) treats the ttl exception of the markRoute entry (G1), and sends as reply nackRoute to the Operator (A1), if the action was to reserve the route, using the flow id of the markRoute entry, which is inherited by the exception entry.

CleanUp (not shown) deletes outdated markRoute entries that want to free the Block. --2: There must exist exactly one config entry at each Block.

Assertions

--3: There must exist exactly one signals entry at each Block.

--4: markRoute is received from "from" neighbor or from Operator.

--5: The next Block of the route is the "to" Block neighbor.

--6: A Block receiving setSignal is reserved within the same flow id.

--7: If a Block is free then all its signals are red.

--8: If a Block status is free then the flow id of its status must be null.

--9: Reserved Blocks were free before.

-x 10: Block freeing requires Operator to have received ack/nackRoute.

-x 11: nackRoute is only sent after TTL of markRoute has expired.

-x 12: If Operator got ackRoute, all Blocks of the route are reserved.

x -13: Signals are set after the Operator has received ackRoute for the flow. x x Tab. 2 describes the major assertions for the use case in an informal way. All of them were successfully modeled with the presented assertion mechanism, Table 3. Railway use case assertions (formal specification).

1: [ALL] Block { PIC { status } } 2: [ALL] Block { PIC { config } } 3: [ALL] Block { PIC { signals } } 4: [ALL] Block { PIC { markRoute <$s = sender> } -→ ( PIC { status <$f = from> } AND PIC { config label($f) == $s } ) } 5: [ALL] Block { PIC { markRoute <$next = head(route)> } -→ ( PIC { status <$t = to> } AND PIC { config label($t) == $next } ) } 6: [ALL] Block { PIC { setSignal } -→ PIC { status val == "reserved" } } 7
: [ALL] $O IN Operator { PIC { ackRoute } } -→ ( $O { PIC { markRoute <$r = route> } } AND [ALL] Block { $$PID IN $r -→ PIC { status val == "reserved" } } ) [ coordinators = { [ALL] Operator } ] 13: [ALL] Block { PIC { setSignal } } -→ [1] Operator { HIC { ackRoute } } [ coordinators = { [ALL] Block } ]
translated with MTA, and tested with the runnable specification of the Peer Model. The resulting Peer Model assertions are shown in Tab. 3. Of these, assertions 12 and 13 show the specification of the assertion property excType.

For assertion 12 we specify that all Operators shall act as coordinators, and in assertion 13 all Blocks serve as coordinators. MTA Application.

As an example for applying the developed model translation algorithms to the defined assertions, the resulting implementation of assertion 7 is shown in Fig. 8, which is an intra-peer one with two sub-assertions.

Overhead Evaluation.

We calculate the overhead by assuming one distributed railway application that has all shown example assertions. The introduced overhead is categorized by number of additional wirings and links. In average per assertion 1,08 more wirings and 11,15 links per Block, and 0,46 more wirings and 6,08 links per operator were needed as shown in Tab. 4.

Conclusion

In this paper we have presented an asynchronous runtime assertion mechanism for the Peer Model, which is an event-driven coordination model. Assertions are formulated in a declarative notation that relies on the query mechanism of the Peer Model. While their concept and syntax are new, they are closely related those of the link and do not pose an entirely new mechanism as the use of a separate tool or language would. The proposed mechanism allows for lazy and strict assertion checking. In the former case, it might happen that certain errors are not detected due to race conditions. In the latter case, all errors can be detected during runtime, however, with the trade-off that a history of certain events must be kept.

Without history and shared variables, overhead is linear in the number of assertions to be checked and an the sizes of context they must be applied to. History imposes an overhead linear in the number of modifications to each entry type to be kept in history and shared variables increase the overhead quadratic in the size of the contexts and linear in the number of variables and sub-assertions.

In a first step, the application model is transformed so that the event history can be maintained, if required by assertions. In a second step, the assertions are implemented by mapping them to the concepts of the Peer Model, so that they become an integral part of the application model and can be understood as a coordination solution themselves.

In contrast to model checking, the proposed assertion mechanism is useful at both model definition and runtime. It makes no assumptions about the environment and can serve models of arbitrary size and distribution without encountering the state explosion problem.

The lazy mechanism is completely orthogonal to the application. The communication overhead depends on the distribution and number of the assertions. The strict mechanism causes additional computation in the wirings, however, only those events need to be captured in the history container that are referred to by (sub)assertions, that are newly obtained in a peer container, or updated or deleted by guards.

While the MTA is specific to the Peer Model, its concepts can be applied to assertion checking in coordination models or distributed systems in general. I.e., states are evaluated locally and evaluations compared instead of collecting global states, only evaluations and variable assignments that influence the overall evaluation of the assertion are shared and the mechanism is highly configurable.

As a proof-of-concept we have specified the major assertions for a use case from the railway domain and demonstrated that all could be captured.

Future Work

In future work, the MTA will be implemented and integrated into Peer Model implementations. Its correctness will be proven and its performance evaluated systematically. We will work on optimizations for overhead minimization produced by the model translation algorithm, investigate assertions that also refer to future events and dynamic changes of the meta model to support dynamic injection of assertions.

Fig. 1 .

 1 Fig. 1. Graphical notation for the main artifacts of the ground model.

  Ass ::= CAss '[' properties ']' | SAss '→' Ass assertion CAss ::= SAss | CAss 'AND' CAss | CAss 'OR' CAss | ('NOT' CAss) complex assertion SAss ::= Ctx '{' PeerAss '}' simple assertion Ctx ::= pid | QCtx | var context QCtx ::= '[' quantor ']' [ var 'IN' ] '<' type '>' quantified context PeerAss ::= PeerCAss | PeerSAss '→' PeerAss peer assertion PeerCAss ::= PeerSAss | PeerCAss 'AND' PeerCAss | PeerCAss 'OR' PeerCAss | ('NOT' PeerCAss) peer complex assertion PeerSAss ::= Container '{' ContainerAss '}' | ' ' sel ' ' peer simple assertion Container ::= 'PIC' | 'POC' | 'HIC' container ContainerAss ::= ['[' quantor ']'] type [' ' sel ' '] ['<' set/get '>'] container assertion properties ::= (* list of properties of form label = value *) property list quantor ::= (* ALL, NONE, or a number (default = 1) *) quantification var ::= (* local variable referring to a peer *) variable pid ::= (* id of a concrete peer *) peer id

Fig. 2 .

 2 Fig. 2. Corresponding wiring for a intra-peer assertion.

Fig. 3 .

 3 Fig. 3. Corresponding wiring for the evaluation of inter-peer assertions.

m 1 ( 1 k i oi 1 k

 111 2o i * k i + k 2j ) additional links and at most m 2j additional messages (m . . . # sub-assertions, k i . . . size of context setting a variable, k 2j . . . size of context reading a variable).

Fig. 4 .

 4 Fig. 4. Two tracks (left) and one point (right) with set direction and signals.

Fig. 5 .

 5 Fig. 5. Sample configuration. Two routes: red and blue.

Fig. 6 .

 6 Fig. 6. Block Peer: Initialization, and setting of signals.

Fig. 7 .

 7 Fig. 7. Block Peer: Marking a route as reserved.

Fig. 8 .

 8 Fig. 8. MTA applied to assertion 7 (see Tab. 2 and Tab. 3).

Table 2 .

 2 Railway use case assertions (informal description). N. . .assertion number, D. . .distributed assertion, P. . .refers to past

	N Assertion

  : [ALL] Block { PIC { status val == "free" } -→ PIC { signals s1 == "red" AND s2 == "red" AND s3 == "red" } }

8: [ALL] Block { PIC { status val != "free" OR fid == "" } } 9: [ALL] Block { HIC { status val == "reserved" <$ts = ts> } -→ HIC { status ts == $ts-1 AND val == "free" } } 10: [ALL] Block { PIC { markRoute action == "free" } } -→ [1] Operator { HIC { ackRoute } OR HIC { nackRoute } } 11: [ALL] Operator { PIC { nackRoute } -→ HIC { exception type == TTL AND entryType == markRoute } } 12

Table 4 .

 4 Calculation of the overhead.

	assertion	# wirings per	# wirings per	# links per	# links per
	number	Block	Operator	Block	Operator
	1	1	0	8	0
	2	1	0	8	0
	3	1	0	8	0
	4	1	0	14	0
	5	1	0	14	0
	6	1	0	11	0
	7	1	0	11	0
	8	1	0	8	0
	9	1	0	24	0
	10	1	1	8	24
	11	1	1	0	17
	12	1	3	12	30
	13	2	1	19	8
	Total	14	6	145	79
	Average	1,08	0,46	11,15	6,08
	Median	1,00	0,00	11,00	0,00

There exists an Event-B-based model checker for the Peer Model[START_REF] Radschek | A usable formal methods tool chain for safety critical concurrent systems design[END_REF].

Acknowledgements. The authors would like to thank Anita Messinger for the discussions on train systems, and Stefan Craß for commenting this paper.