Converting Reconfigurable Petri Nets to Maude

Model checking is an important aim of the theoretical computer science. It enables the verification of a model with a set of properties such as liveness, deadlock or safety. One of the typical modelling techniques are Petri nets they are well understood and can be used for a model checking. Reconfigurable Petri nets are based on a Petri nets with a set of rules. These rules can be used dynamically to change the net. Missing is the possibility to verify a reconfigurable net and properties such as deadlocks or liveness. This paper introduces a conversion from reconfigurable Petri net to Maude, that allows us to fill the gap. It presents a net transformation approach which is based on Maude's equation- and rewrite logic as well as the LTLR model checker.

Motivation
The first approach to convert reconfigurable Petri net to Maude (see [Schulz, 2014]) is designed as extension for ReConNet. It uses the implementation of ReConNet to get all possible matches for a set of rules and a given Petri net. This approach results in a dependency of the current net state and the algorithm of ReConNet. Hence, that the model-checking process has only one-step application of a rule may be wrong if a rule is used twice, because an error may occur after the second usage.
The new approach is based on the algebraic structure of reconfigurable Petri nets. The main task was to create a structure which can be read similar to the mathematical notation of a reconfigurable Petri net. It includes the possibility to simulate the net. This implies a solution for a transition that defines the activation and firing. Maude has been chosen as the appropriate language to implement this definition.
Moreover, the rules need to be implemented within the new structure. In contrast to the first approach it should be able to detect a match itself.
The following sections contain an overview of all relevant parts of this approach. The first section gives a short overview of the background for this work. The next section focuses the new modules, which contain the data-types for the resulting Maude specification of a converted reconfigurable Petri net. Finally, an evaluation shows the performance of the current implementation based on a test net.

Background
First we introduce reconfigurable Petri nets. They extend Petri nets with a set of rules, that can modify the net at runtime. Moreover, Maude is introduced since it is the result the conversion aims at. Finally, a short survey of related works is presented.

Reconfigurable Petri nets
One of the most important models for concurrent systems and some software engineering parts are the Petri nets, based on Carl Adam Petri's dissertation [Petri, 1962].
A marked Petri net can be formally described as a tuple N = (P, T, pre, post, M 0 ) where P is a set of places and T is a set of transitions. pre is used for all pre-conditions of transitions, which describes how many token are required for firing. On the other hand, post holds all information of the post-conditions for all transitions. Finally, M 0 shows all initial tokens on the places for this net N [Meseguer a. Montanari, 1990;Juhas et al., 2007].
Further, based on a Petri net are reconfigurable Petri nets important because they can modify themselves with a set of rules [Ehrig et al., 2007;Kahloul et al., 2010]. A reconfigurable Petri net can be describe a tuple of a reconfigurable Petri net RN = (N, R). This definition uses the Petri net tuple and a set R of rules, which are given by rule r = (L ← K → R) [Padberg, 2012;Ehrig et al., 2009]. L is the left-hand side (LHS), which needs a morphism to be mapped to a net N . K is an interface between L and R. R is the part which is inserted into the original net. To realise this replacement a matching algorithm needs to be defined that finds L within the source net N . This match includes a mapping between the elements in the Petri net and the left side of the rule (L). Basically, this algorithm finds the same structure (form L) within the Petri nets [Blumreiter, 2013].
Reconfigurable Petri nets are also comprises capacities and labels for transitions/places [Padberg, 2012]. A limitation for place is realised via a capacity, that contains a value which describes how much token can be stored on a place. The function cap : P → N w + assigns for each place a natural number as capacity. Further, two label function (pname and tname) refer for each place or transition a name from a name space (pname : P → A P and tname : R → A T ).
ReConNet is shown in Figure 1 with an example net N 1 and rule R 1 . The configurations such as node names or markings as well as the control elements for firing and transformation are presented in the upper region of the graphical interface. A graphical illustration of reconfigurable Petri nets is in the remaining interface. First, a net which models a cycle is composed of three places and transitions as well as one token. Wider, a rule which changes the arc direction of a transition is displayed under the net. In both editors are activated transitions marked as black transitions instead of grey normal transitions. Colours for places in rules are used to ensure the common bond.

Maude
Maude has been developed at the Stanford Research Institute International (SRI International) for the last two decades. The equation and rewriting logic, which supports a powerful algebraic language, is used as a base [Escobar et al., 2009;Clavel et al., 2002]. Based on these two kinds of logics Maude models a concurrent state systems that used for semantic analysis such as deadlock discovery via LTL-model-checking-module [Katoen a . Baier, 2008;Eker et al., 2004].
Maude consists of a core which is named " Maude Core". On top of its core every other part is written in Maude itself. Actually, Maude is distributed in version 2.6 form the website 1 [Clavel et al., 2011].
A program in Maude is based on one or many modules where every part of the system looks like a clear to read abstract data type (ADT). A module contains a set of types, which are used with the " sort"-keyword. It is also possible to define more than one type with the plural form " sorts". Each type describes a property for the module. For example types for a Petri net can be described with: sort P laces T ransitions M arkings .
If this operator has to be associative (in Maude with a short version: " assoc") and commutative (short with: " comm") properties, Maude defines this in the end of this line. Hence, we obtain a multiset of markings by this operator. The notation allows these properties in box brackets, so that it can be written as: Maude uses the equation logic to define the validity for an operator (axioms). This can be exemplified with the initial marking from a Petri net. This marking is a representation of the initial state of the Petri net. Based on this information we can define an operator that describes the initial state of a Petri net. After that, the validity with an equation can added.
If we have a Petri net with only one marking with an " A" label we obtain these two lines: eq initial = A .
Types are defined as " sort", operators as functors and equations as the validity of operators.
The rewrite rules can be used to replace one multiset with another multiset. So all terms are immutable as in many functional languages. A replacement rule consists of two multisets, where the first set is replaced with the second one. These two termsets are separated with a double arrow, as shown in the following example, where a term A is replaced with a new term B: Based on this example an implementation of the token game of Petri nets can be realised.
The two multisets can be seen as pre-and post-set of a transition. Hence, a rule can be used to describe a firing step with this two sets. This replacement rule can be modelled with the following graphical representation:

Related Work
The basic example for a Petri net to Maude conversion uses a shop system, where a user can buy an apple or candies. The mapping into Maude uses the term replacement system to model the firing steps of this net. Based on this Maude-structure it is possible to add a model-checking possibility, which can be used to verify a deadlock or safety properties [Clavel et al., 2011].

Figure 3: Shop example with apple and candy
A more complex example of this modelling (see Figure 3) is shown with high level nets in [Stehr et al., 2001]. It presents a conversion of the banker problem where two credits are handled by the net structure. The focus of the work lays on the soundness and correctness for this conversion approach. A formal definition of the model and the operators as well as the firing of a transition is given. Further, the paper presents an approach for a coloured Petri net (CPN). It extends the previous approach with more complex operators for the firing replacement rules. The conversion of transitions is realised via Maudes replacement rules and operators which contain the coloured tokens.
Automatic mapping for UML-models to a Maude-specification (see [Chama et al., 2013]) is similar to this paper's idea of converting reconfigurable Petri nets. In [Chama et al., 2013] the authors present three steps modeling, analysing and converting to Maude modules.
The first step focuses on subject-specific modeling within UMLs class, state or components diagrams. After that step, the tool AtoM is used to convert the model into a Pythoncode representation. This code will be used to solve some constrains inside the UML-model components and some diagram specific parts. Lastly, the final step transfers all data into a Maude-specification, which can be used to verify some properties for example deadlocks.
In [Barbosa et al., 2011] Petri nets are also converted into Maude-modules. As a base an Input-Output Place/Transition net (IOPT net) is used and saved in a PNML-file. These files are the origin for the conversion process. Further, PNML is used as a well-known markup-language for Petri nets. This process divides all components of a Petri net in special Maude-modules (net, semantic and initial markings) which can be used to verify in a same way as in [Chama et al., 2013].
A use case for the resulting Maude structure is presented in [Bjørk, 2006] [Stehr et al., 2001]) which are simulations with one step commands. After one step the tool is capable to present the results.

Data type
A reconfigurable Petri net N 1 consists of a tuple which is separated in a Petri net N and a set of rules R. It can be written with N 1 = (N, R). Furthermore, a Petri net can be formally described as a tuple N = (P, T, pre, post, M, cap). Where P is a set of places, T is a set of transitions, pre and post are functions which maps T → P ⊕ and finally M is the initial marking. Additionally, a function cap : P → N ω can be used to model a capacity of a place P with a value N ω [Padberg, 2012].
An example of a Petri net is shown in Figure 4. Each blue circle is a place and each rectangle is a transition. The arrows between these elements describe the arcs, which can connect a place with a transition and vice versa. The two black points are tokens which can be consumed by a transition. The example in Figure 5 shows a rule which changes the direction of an arc for a transition T . The change is realised by two steps. At first, the match of the left-hand side ensures that the rules can be applied. And finally, the right-hand side contains the information to be used.
This example contains a transition which connects the places in reverse order (arc colour black). However, the mapping net contains both transitions. The arc inversion is realised by a deleting one transition and adding a new transition with reversed arcs. The aim of this work is to create Maude modules, which provides the possibility to create a formal writing of a reconfigurable Petri net. The example net in Figure 4 can be formally indicated as: First, all sorts are defined. A sort can be understand as a type which contains the semantic.    which are a mapping between a transition and a multi-set of places. Finally, the markingoperator contains a multi-set of Places. The content is separated with an additional symbol as the linear sum in the mathematics definition in Figure 6.
The example in Figure 6 can be written in Maude as in Listing 2. It separates all operators and the included multi-sets with commas. Each multi-set is wrapped with curved brackets.
A place is modelled as tuple with p(<label> | <identifier> | <capacity>). Labels are defined as a string, identifier and capacity as numbers. Transitions are based on the tuple t(<label> | <identifier>). Each type has the same type as for the place.
Listing 2: Maude module for a Petri net

Activation and Firing
A transition t is activated, written by m[t , when the following two conditions are satisfied.
The first condition consists of the pre-set of this transition. The net marking has to contain at least as many tokens, as described it in the pre-set (see Equation 7). Furthermore, all post places have to satisfy the capacity condition. Adding more tokens than a place can store is not possible (see Equation 8).
If both conditions are satisfied, the transition t can fire. One firing step is written with where m is the current marking and m is the following marking. The calculation of m is described in Equation 9. First, the pre-set is deducted from the current marking.
Now the post-set of t can be added to the result. The source code consists of the helper method leeqth with . This operator tests the capacity of a place multi-set and a single place. The third parameter is used to count the occurrence of a token in the multi-set. In case that the counter is bigger than the capacity it returns false. All other cases results with true. Listing 4: Capacity proof of each place in the post-set

LTL Properties
The aim of this work is to verify properties such as deadlocks, liveness or reachability for a reconfigurable Petri net. To realise this Maude's LTLR implementation is used. It is based on an implementation of the linear temporal logic (LTL). The implementation itself uses a Kripke structure, which is realised on the basis of the equation and rewriting logic, basically a finite transition system [Eker et al., 2004].
The following examples in Listing 15 ff. are using the operators defined in Listing 5. It contains an operator for the reachability of a marking. The enabled-operator includes the activation of a transition as well as the ability to apply a rule. Finally, the last three lines in Listing 5 include a standard equation, which is used when no other equation can be used.
The implementation starts with a sub sorting of the Configuration-type. This is necessary because the Kripke structure is based on these informations. It means that all Configurationobjects are relevant for the construction of the states of the Kripke structure. In terms of this work a Configuration-object contains a snapshot of a reconfigurable Petri net. At the beginning it includes the initial marking and the primal state of the net without any transformation with rules. All other following conditions include the further interactions of the net (in this case the Configuration with firing steps and rule treatments).

Matching of Rules
A reconfigurable Petri net consists of a net and a set of rules R. Each rule contains three sub-nets, which contain a net L for matching, a net R for the replacement and a net K that maps between the two nets.
The first project [Schulz, 2014] is based on ReConNet. This tool provides the capability to find non-deterministic matches for a net and a set of rules [Blumreiter, 2013]. The aim of the first project is an extension that enables ReConNet to verify a net with a given set of rules. The verification process is realised by a conversion to a Maude specification. In order to realise this process, an interface is designed for using ReConNet to find a match. Due to this constellation, only the initial state of a net and all rules can be verified with the LTL-process.
The new aim is to ensure that the Maude specification finds the matching itself. This implies a possibility to define a rule in this specification as well as the dangling-condition (see section 3.4). Further, the meta-data configuration (such as current highest identifier) should adapt a net and a set of rules.
The definition of a rule and the meta configuration can be found in Listing 6. First, the sorts Rule, LeftHandSide and RightHandSide are defined. This models the two sides of a rule. The mapping net K is not included, because it is not relevant for matching of a rule.
Further, the Configuration consists of a net, a multi-set of rules and a global ID-count. The net contains all information as places, transitions, markings and pre-as well as post-sets.
Each rule multi-set entry contains a left and right side. At last the ID-count is used for each insertion step, where a new transition or a place will be added. The whole rule is written as a condition replacement. If the conditions satisfied with the current net, the rule can be applied. Due to the replacement, the left-hand side of the rule is replaced with the right-hand side. Furthermore, a rule is working with a configuration object. It uses a net, a multi-set of rules as well as an ID-count.
The example in Listing 7 shows the left side of the rule in Figure 5. The net which should be found, consists of two places with the label A. Further, it contains a transition T which connects the two places. A description of the arcs can be found in the pre-and post-set. At last it contains a marking on the place A. All these elements are part of the net in the rule.
It only differs in the ID, which are not given as concrete numbers. Each Irule<number> is a variable that is used for finding a structural match. If the net has the same structure, but other ID's for the places and transitions, this rule is also activated. This is possible because Maude maps the ID's internal with each variable. Moreover, each set contains a variable for possible residual elements. For example, in this net the set places contains more than two places. The remaining place's are mapped into the variable P Rest, so this rule is still activated. If a multiset has no more elements the identities (id) is used (for a definition see Listing 1). Each id itself is the empty-set constant operator (such as emptyPlace, emptyTransition, emptyMappingTuple or emptyMarking).
It calculates the new identifier which is detailed described in subsection 3.5.

Dangling-Condition
A special part of a rule matching is the gluing condition. This condition is separated into the identification and dangling condition. The identification condition requires that no place or transition is specified to be simultaneously added and deleted. Further, the dangling condition defines that a place can only be deleted if there are only arcs to transitions, that are deleted as well. Transitions are not relevant for dangling condition.
The example net N 2 in Figure 7 shows a short example, where a place A (the red place) should be deleted with rule r 3 in Figure 8. The rule has only one match because the bottom part of the net differs in an addition transition. This transition injured the dangling condition and the rule cannot be used at this point.

A T A
A T A T

Multi-Set for used Identifiers
One problem of Maude is the missing garbage collection 2 . This can result in an overflow if a rule inserts a node (place or transition), because each new node gets an identifier.
To solve this problem a multi-set of unique identifiers is used. It requires a modification of the Configuration definition which is introduced in Listing 6. Now it contains an integer for the maxID and for the defined step size. Further, it has two sets for the place and transition identifiers. The implementation can be found in Listing 11.

Transformation
This section includes the architecture of the conversion process as well as the results of some model checking formula.

Architecture
The output base of ReConNet consists an extension of PNML 3 . PNML is a XML-based standard for the Petri net export. The graphical editor ReConNet uses this standard for the persistence of developed nets. In addition to the pure PNML-standard, a rule is stored with its three net in a PNML file.
Based on PNML, this work uses XSL to realise the conversion. The result uses the Maude modules which are defined before the conversion.The sorts for Places, Transitions and the net itself are previously defined. And further it contains the logic of firing or the identification of the dangling condition (see also the definition of all modules in the listings above).
The XSL process is designed with the separation of the global types as places, transitions, pre or post. Further, it has the specific sub xsl-templates for the conversions as in the net, rules, prop or rpn. The structure is summarized in Figure 9. The global types are defined above the specific modules that are grouped together in separate packages. The difference to the first project is that this approach is independent of ReConNets implementation. The first project uses the persistence-module of ReConNets to load PNML-files (net or rule) [Schulz, 2014]. This approach is superior because it is built up directly on the PNML data. The conversion process is written with XSL, which provides a well known language. The interface between this approach and ReConNet is realised through an export to the PNML files that can be used with a net or few rules.

Results
Based on the result of the conversion process it is possible to use Maude's LTL implementation. The prop.maude-module includes all the necessary code for the LTL process (see Listing 14). It subsorts the Configuration-typ under state, which is required (for the Configuration-typ see Listing 6).

Listing 14: Sub sorting of Configuration with State
In the first example, the deadlock freedom of example Figure 4 will be shown. The formula is based on the box-and diamond-operator. In total it describes the semantic of liveness.
It means that a property is globally (box) repeatedly (diamond) true. To write the liveness property for the reconfigurable Petri net modules, the following line can be used: marking{p("A" | 17 | 2147483647)}))) 26 28 10 aidPlace{26, (27,(28,(29,(30,(31,(32,(33,(34,(35,( 30 36))))))))))} aidTransition{26, (27,(28,(29,(30,(31,(32,(33,(34,(35,(36))))))))))} 32 ,deadlock}) Listing 15: Counterexample of a deadlock The meaning of this counterexample is that the rule consists of this marking. It is possible that all tokens are on one place. Furthermore, this place has only incoming arcs which results in a deadlock. The net-state with this deadlock is modelled in Figure 10. Figure 10: State of N 1 with a deadlock (r 1 can not be applied) In assumption that the markings were changed on the places within the rule (see Figure 11) the result is varied, shown in Listing 16. It shows, that the net N1 and rule r2 are deadlock free. The new rule prevents the situation in Figure 10, where the marking can be located on one place which has only incoming arcs. Hence, two situations are possible. First, the rule is not enabled when a marking is at a place, where all arcs are starting. The net itself can fire. On the other hand, a marking will be placed on a place where one or more arcs are incoming. For this case, the rule can be used. The result is that a transition is enabled now and will also continue to be used for the token game. In either situation, an operator of Listing 5 is enabled since the enabled-operator is defined for the firing and transformation step. The reachable-operator is designed to find a given marking. The formal definition of this operator is: Therefore, it is possible to test one or many tokens. In the example bellow (see Listing 18) two tokens (A 3 and A 3 ) are searched in N 1 . Maude's result describes a situation where it found a deadlock with two tokens on A 2 .

Evaluation
This section presents a first step of the performance evaluation of this approach. The evaluation is based on two steps. At first, a net is converted into the Maude modules. And after that step it is tested with the liveness formula (see the first formula in section 4.2).
The conversion uses a net which is build as a circle and the rule r 1 (see Figure 5). Further, it contains one token at place P 1 . The structure connects a place with two transitions (one for the pre and vice versa). Hence, it is possible to build a test which shows the performance of a net which can be scaled with the size of nodes (places and transitions).
For this work four net sizes are used, which allow to make a meaningful statement. Each net has the same semantic and should return true. Hence, only the runtime meta-data such as rewrite count and time are different. The conversion process runs in each case with nearly the same time (see Table 1). Further, the rewrites are grown linear with the size of nodes.
It takes 109 rewrites for 10 places and transitions. If the net has twice as many nodes as in the first example, it takes 209 rewrites. Only the used time grows exponentially. It changes from 13 ms to 23994 ms. If the net receives only 4 new nodes, it grows to 189939 ms (see Table 2). The resulting state-space explosion was expectable as a well known issue of LTL [Valmari, 1998].

Future Work
An outlook of the following work is shown in this section. The formal founding represents the essential part of the conversion from a reconfigurable Petri net to Maude. The aim is the verification of the soundness and correctness for the conversion and target representation of the net in Maude.
Furthermore, an integration of parts from a reconfigurable Petri net such as negative application conditions (NACs) (see [Rein et al., 2008]) or decorations (see [Ede et al., 2012]) should be realised. This enables the verification of the nets and rules from the Living Place Hamburg [Ede et al., 2012].
Finally, a benchmarking is necessary between this approach and a tool such as Charlie 7 to obtain a meaningful statement. This implies a way which converts a reconfigurable Petri net into a net that can be used from other verification tools. The main challenge is to realise a conversion which contains the net and all possible rule conditions.

Reconfigurable Petri Nets -NET.maude
mod NET is 2 including PROP .


extfieldsofstudy: Biology Medicine

s2fieldsofstudy:
Computer Science
Environmental Science

text:
rAvis: An R-Package for Downloading Information Stored in Proyecto AVIS, a Citizen Science Bird Project

Citizen science projects store an enormous amount of information about species distribution, diversity and characteristics. Researchers are now beginning to make use of this rich collection of data. However, access to these databases is not always straightforward. Apart from the largest and international projects, citizen science repositories often lack specific Application Programming Interfaces (APIs) to connect them to the scientific environments. Thus, it is necessary to develop simple routines to allow researchers to take advantage of the information collected by smaller citizen science projects, for instance, programming specific packages to connect them to popular scientific environments (like R). Here, we present rAvis, an R-package to connect R-users with Proyecto AVIS (http://proyectoavis.com), a Spanish citizen science project with more than 82,000 bird observation records. We develop several functions to explore the database, to plot the geographic distribution of the species occurrences, and to generate personal queries to the database about species occurrences (number of individuals, distribution, etc.) and birdwatcher observations (number of species recorded by each collaborator, UTMs visited, etc.). This new R-package will allow scientists to access this database and to exploit the information generated by Spanish birdwatchers over the last 40 years.

Introduction
During the past several decades, developers have focused their attention on constructing web repositories to store and share biological information. On the one hand, there are online repositories with information generated by scientists, like specimens collected for museums and herbariums, fossil records or genetic data (e.g. GBIF: http://gbif.org, NOW: http://helsinki.fi/ science/now/, GeneBank: http://ncbi.nlm.nih.gov/genbank/). On the other hand, there are web sites that store biological information collected by non-scientists, or so-called 'citizen science'.
Citizen science has proven to be an appropriate method to provide researchers with valuable information [1][2][3], and is increasingly used as an adequate way to sample species occurrences and distributions [4], to collect data to investigate urban ecology [3,5,6], or to collect data on bird biology, ecology and diversity [7][8][9]. In our case, data stored in Proyecto AVIS, our citizen science project to collect data from amateur Spanish ornithologists, show the same general patterns described by scientists based on their own samples and field experiments. Power law distributions of species/area [10] and species/ abundance [11] have been detected (Figure 1), suggesting that the data stored in Proyecto AVIS have similar properties to the data collected by scientists.
One of the main characteristics of the citizen science databases is that they are huge. For instance, birdwatchers' observations stored in the eBird database reached 100,000,000 observations and over 10,000 species (http://ebird.org). As a result, there are terabytes of information about species occurrences (latitude, longitude, altitude, time, habitat, diet, alleles, etc.) stored in online databases that follow different formats and standards of data storage [12], and the challenge now is developing easy strategies to use this information for research [13].
Currently, there are ongoing projects to generate tools to standardize the information stored in those databases (e.g. http:// ecodataretriever.org) and to develop R-packages to connect online biological databases to the R-environment (http://ropensci.org/). As a consequence, large international databases are now being made available through R using packages like rebird [14], rfishbase [15], rgbif [16] or rvertnet [17] (connecting R with eBird, Fishbase, GBIF and VertNet databases, respectively). All of these new data exponentially increase our capabilities to answer questions about species conservation, global change, macroecology and biogeography.
R is an open source and collaborative framework (http://.rproject.org/), and is one of the most used environments for analyzing biological data and for developing scientific software [18]. Many young scientists are becoming advanced R-users (but see [19]). Thus, R is becoming a standard environment for developing easy-to-use (and re-use) functions and for sharing them with the academic community. For all of these reasons, we decided to build an R package to directly download the information stored in Proyecto AVIS from the R environment, in order to promote the use of the data stored in this database within the growing scientific R-community.

Proyecto AVIS
Each citizen science project stores singular and, consequently, important information [6,9,[20][21][22]. Proyecto AVIS (http:// proyectoavis.com) is a citizen science project born in August 2005 with the idea of collecting the data stored in the field notebooks of amateur Spanish ornithologists and sharing them with both other amateur ornithologists and the scientific community. More than one hundred collaborators, including several NGOs, have been actively participating in the project uploading their bird observations. Overall, the database contains records over 40 years , stores 82,503 records, totalling 4,739,171 individuals from 413 species, which represents 90% of the total number of species recorded in Spain. In addition, it contains information from 1,717 different UTMs (squares of 10610 km), representing 30% of the Spanish territory (query to the database: November 2013).
The Proyecto AVIS database and web page were built using open source software (MySQL, Perl, Apache) and free GIS layers. Proyecto AVIS requires five mandatory fields for each bird observation: 'species', 'number of individuals', 'observation period', 'date' and 'UTM 10610 km square', plus several optional fields that include variables like 'hour', 'sex', 'age' or 'habitat'. To standardize the taxonomy, the bird species list follows the Bird List of Spain from SEO/BirdLife [23]. Bird occurrences in the Proyecto AVIS database are georeferenced using the projected UTM 10610 km square system and the MGRS labelling convention (Military Grid Reference System). The UTM/MGRS is the standard system for mapping species occurrences in Spain and is the system used by the Spanish bird atlases [24,25]. To help users identify the UTMs in which they recorded the species, the web application includes an easy-to-use tool to geo-referenced the observations based on a Google Maps TM routine.
The Proyecto AVIS web page (http://proyectoavis.com) includes several user-friendly tools for exploring the database, like summaries of the bird observations or graphics of the species records throughout the year, and it allows registered users to download detailed information about the species observations to Excel files. However, although the database is already available on the Internet, its use for research has not been properly exploited. Proyecto AVIS lacks a specific package to connect the web repository with the R-environment, and we believe that this fact has prevented scientists from using Proyecto AVIS information.
Description of the package rAvis exclusively contains R code, which maximizes its portability across platforms, and it works in Unix-like and Windows operating systems. The rAvis functions have been optimized following the standards criteria for software quality [26,27] and they are accessible through GitHub (https://github. com/javigzz/rAvis). Bugs can be reported using GitHub; https:// github.com/javigzz/rAvis/issues. rAvis is freely available on the Comprehensive R Archive Network; CRAN (http://cran.rproject.org/) and complete information about rAvis, its functions and their parameters is available in the package help. rAvis uses functions from other R-packages to get and plot the data stored in Proyecto AVIS. Namely, R-libraries stringr [28], XML [29], tools [30], RCurl [31], scrapeR [32] and gdata [33] are used to download the bird observations; maptools [34], raster [35] and rgdal [36] to plot the GIS files; and, finally, scales [37] is used to plot bird occurrences with a transparency.
Exploring Proyecto AVIS. We developed several functions to explore the database in an easy and visual way and other functions to download the selected information (see Table 1 and run the example). First, avisSpeciesSummary allows users to download a table with a summary of the records stored in Proyecto AVIS aggregated by species: number of observations of each species, number of individuals recorded, number of different UTMs (10610 km) with observations, number of birdwatchers that recorded the species. Second, avisContributorsSummary returns a table with a general summary of the records stored in the database Finally, avisHasSpecies checks if a species name exists in Proyecto AVIS and then, avisMapSpecies allows users to explore the distribution of the observations of the species by setting the name of the species and selecting the type of map; administrative boundaries ('admin') or physical map ('phys') ( Figure 2).
For constructing the plots we used free GIS layers. We downloaded the Spanish administrative map from http://.divagis.org/, the Spanish UTM map from the Spanish government online map repository http://bscw.rediris.es/pub/bscw.cgi/ 524254?client_size = 13666580, and the Spanish physical map from http://.openstreetmap.org/ using the R-library Open-StreetMap [38].
Advanced queries to Proyecto AVIS. We constructed two main functions to set flexible queries about the species occurrences and the birdwatcher observations: avisQuerySpecies and avisQuer-yContributor, respectively. These functions download the information stored in Proyecto AVIS, and are intended to be tuned by the users in relation to their specific objectives. Also, we programmed avisQuery as a flexible function to pass any argument allowed in Proyecto AVIS database. We decided not to predefine queries or to pre-process the data because this would narrow the possibilities for research [12]. Instead, we allow the users to set their own queries to Proyecto AVIS. Arguments include taxonomic levels, like species, family, order; individual characteristics, like age, sex, breeding status; temporal filters, like year and month; or environmental filters, like habitat. Moreover, we added a UTMlatlong conversion to all queries. Thus, the position of the observations is given in two different formats: projected UTMs 10610 km and geographic coordinates WGS84 (common latitude-longitude coordinates, which are not available in the current web application from Proyecto AVIS). We did not program more specific graphics or statistical analyses because we understand that the purpose of this package is to obtain the biological information stored in Proyecto AVIS and not to re-program statistical algorithms that are already available in other R-packages. We assume that R-users would employ different R-packages for calculating their own statistics and constructing their own plots (see the example).

Conclusions
We have programmed rAvis, an R-package designed to help researchers explore and download the information stored in Proyecto AVIS. Thus, biogeographers, macroecologists and ornithologists working in spatial ecology or temporal series, in addition to researchers working on citizen science can easily take advantage of the unique data stored in this database for their own research.


CALL-SLT: A Spoken CALL System Based on Grammar and Speech Recognition

We describe CALL-SLT, a speech-enabled Computer-Assisted Language Learning application where the central idea is to prompt the student with an abstract representation of what they are supposed to say, and then use a combination of grammar-based speech recognition and rule-based translation to rate their response. The system has been developed to the level of a mature prototype, freely deployed on the web, with versions for several languages. We present an overview of the core system architecture and the various types of content we have developed. Finally, we describe several evaluations, the last of which is a study carried out over about a week using 130 subjects recruited through the Amazon Mechanical Turk, in which CALL-SLT was contrasted against a control version where the speech recognition component was disabled. The improvement in student learning performance between the two groups was significant at p < 0.02.

Introduction and background
People have been building Computer-Assisted Language Learning (CALL) applications for several decades, and more recently it has become popular to include speech recognition as one of the components. The intuitive rationale is obvious: if the system has some ability to understand what the student is saying, then it may be better able to help them improve their spoken skills. The most common type of speech-enabled CALL system constructed to date has focussed exclusively on pronunciation practice. Many variants exist (an impressive and well-documented example is the EduSpeak R system (Franco et al., 2010)), but the basic scheme is simple: the system plays the student a recorded sentence, asks them to imitate it, and then rates them on the accuracy of their imitation, giving advice if appropriate on how to improve pronunciation or prosody. It is easy to believe that this is useful, but it is also very limited in scope: the student is given no opportunity to practice spontaneous spoken generation skills.
A more ambitious approach is to design an application where the student can respond flexibly to the system's prompts. The project we describe in this paper, CALL-SLT (Rayner et al., 2010), is based on an idea originating with (Wang and Seneff, 2007); a related application, described in (Johnson and Valente, 2009), is TLTCS. The system prompts the user in some version of the L1, indicating in an abstract or indirect fashion what they are supposed to say; the student speaks in the L2, and the system provides a response based on speech recognition and language processing. We have built several prototypes on this basic pattern, exploring different language-pairs and strategies. For example, in a minimal version configured to teach French to English-speaking students, a prompt might be the text string: REQUEST HAMBURGER and the student will be allowed to respond with any of the following alternatives: Je voudrais un hamburger J'aimerais un hamburger Puis-je avoir un hamburger ? Je prendrai un hamburger ... In more complex versions, the prompt may be presented in multimedia form, or appear as part of a simple dialogue between the student and the application. Irrespective of the modality used, the student, in order to respond correctly, must be able to pronounce the French words well enough to be understood by the speech recogniser; they also need to be able to construct a spoken French sentence whose meaning matches the content of the prompt.
In the rest of the paper, we first describe the core system ( §2) and the various types of content we have developed ( §3). We then present a number of evaluations ( §4), where the central question addressed is whether the application is in fact capable of helping students improve their language skills. The final section concludes.
2 System architecture 2.1 Overview of architecture The CALL-SLT system is based on two main components: a grammarbased speech recogniser and an interlingua-based machine translation system, both developed using the Regulus platform (Rayner et al., 2006). Each turn begins with the system giving the student a prompt, typically formulated in a simplified or telegraphic version of the L1, to which the student gives a spoken response; as already noted, it is in general possible to respond to the prompt in more than one way.
The system decides whether to accept or reject the response by first performing speech recognition, then translating to language-neutral (interlingual) representation, and finally matching this representation against the language-neutral representation of the prompt. A "help" button allows the student, at any time, to access a correct sentence in both written and spoken form. The text forms come from the initial corpus of sentences, which is supplied by the course designer; the associated audio files are collected by logging examples where users registered as native speakers got correct matches while using the system. Prompts are grouped together in "lessons" unified by a defined syntactic or semantic theme, and may optionally be linked together by a script to form a simple interactive dialogue.
The student thus spends most of their time in a loop where they are given a prompt, optionally listen to a spoken help example, and attempt to respond. If the system accepts, they move on to a new prompt; if it rejects, they will typically listen to the help example and repeat, trying to imitate it more exactly. On reaching the end of the lesson, the student either exits or selects a new lesson from a menu.
In the rest of this section, we describe the main components: grammar-based recognition and rule-based translation, lesson structure, user interface and web deployment.

Grammar-based speech and language processing
The speech and language processing components of the system are entirely rule-based. The same grammar is used both to provide the lan-guage model which constrains the speech recogniser, and to parse the result of performing speech recognition. The intent is to ensure that all speech recognition results will be within the coverage of the language processing components, which greatly simplifies the architecture by obviating the need for robust parsing and semantic interpretation.
The underlying platform is the Nuance Toolkit 1 , which provides facilities for defining context-free (CFG) grammars that can be compiled into language models and also used for parsing. It would be possible to write these grammars by hand, though doing so involves the usual problems, given that CFG is not a very expressive formalism; it is hard to model any non-trivial linguistic phenomena without producing an extremely large grammar that is in practice almost impossible to extend or maintain. A well-known method for addressing these issues is to specify the grammar in some higher-level formalism -most obviously, some kind of feature grammar -and compile this down to CFG form (Stent et al., 1999). This time, the problem is in another direction. Even if a substantial, linguistically motivated feature grammar can in principle be expanded out to a CFG grammar (this is of course by no means guaranteed), the resulting grammar will probably be so large that it exceeds the practical resource limits imposed by the speech recognition framework. For these reasons, grammars that can actually be used as language models need to be domain-specific; this, unfortunately, conflicts with the natural desire to make the grammars general and reusable.
The Regulus system steers a middle course between these alternatives. For each language, we construct a central resource grammar implemented using a feature-grammar formalism, but we do not compile this directly into a CFG language model. Instead, we first extract a domain-specific subgrammar using Explanation-Based Learning (EBL) methods driven by small corpora typically containing a few hundred examples. The scheme is explained in detail in (Rayner et al., 2006), which also includes a thorough description of the English resource grammar. Similar grammars have since been developed for French, German and Japanese. These have been further extended to cover related languages by a parameterization process. In particular, the French grammar has been extended into a shared grammar which covers French, Spanish and Catalan (Bouillon et al., 2007), and the English grammar has been similarly extended to cover both English and Swedish (Rayner et al., 2012b).
The Regulus resource grammars are also parameterized to support multiple types of semantic representation. In all the work reported here, the semantic formalism used is Almost Flat Functional Semantics (AFF; (Rayner et al., 2008)), a minimal formalism where clauses are represented as unordered lists of elements tagged with functional roles. For example, "Could you give me directions to the zoo?" is represented as the structure

Using interlingua to display prompts
The AFF representations produced by speech recognition and parsing are translated into a language-neutral form, also expressed using AFF. The minimal list-based format means that translation rules can be very simple: basically, they map tagged lists onto tagged lists, possibly conditional on the surrounding context. The details are provided in (Rayner et al., 2008). The space of possible interlingual forms is defined using another Regulus grammar, which associates each valid interlingual AFF representation with a surface form. In the context of the CALL-SLT system, the intention is that these interlingual representations form a reduced, simplified and abstracted version of the English grammar, while the surface form is used as part of the prompt given to the student. Thus, continuing the previous example, suppose that the system is configured with English as L1 and German as L2, i.e. to teach English to a German-speaking student. The AFF form corresponding to "Could you give me directions to the zoo?" is converted into the interlingual representation null= [utterance_type, request] arg2= [abstract, directions], to= [loc, zoo] using a set of translation rules of which the least trivial is the one which maps the elements corresponding to "Could you give me..." to the single element null=[utterance type, request].
We have experimented with several strategies for defining interlingua grammars: as usual, there are a number of competing requirements. On the one hand, we want the grammar to be structurally simple, so that the process of converting interlingual AFF representations to surface forms can be fast as possible. A second requirement is that the surface forms should be fairly natural-looking L1 expressions. A third is that it should be easy to port the system to support a new L1; in practice, this task is often carried out by people who have domain and L1 expertise but little knowledge of computational linguistics.
The compromise we have found best in practice is to define a minimal interlingua grammar parameterized in two ways. First, there are hooks allowing generic changes to the default Subject-Verb-Object word-order: for example, if the L1 is Japanese, we want the verb to be preceded by its complements, and for German we want the modifiers to come before the verb if it is not the main verb. The grammar is kept very simple to make it feasible to allow this kind of flexibility: for example, we do not have any kind of moved question construction, so the word order is "You want what?" rather than "What do you want?". The only concession to grammatical agreement is to add a formal affix to the verb, making it agree with the subject.
The second type of parameterization is to handle surface forms. The plain grammar produces surface forms using English words; a final processing step uses a set of surface rewriting rules to map English words into the final L1.
Although the scheme cannot be called elegant, it is easy to implement and maintain, and performs well in practice.

Providing help examples
When the student is uncertain how to answer a prompt, the system can provide them with an example of a correct response. Since every prompt is derived from an example taken from the L1 corpus, at least one example is always available. Given that the interlingua grammar used to define the prompts has less structure than the L1, and maps many L1 sentences onto the same prompt, there are typically several possible help examples available. By recording successful interactions made by users registered as native speakers of the L1, the system can also store spoken help examples. When a course is being created, the course designer usually arranges for a native speaker to cycle through all the examples until they have successfully completed each one, ensuring that both written and spoken help are always available. The user interface supports a special "recording mode" designed to support this task, where the system only offers the user prompts for which recorded examples examples do not yet exist. Each speech example is tagged with the words found by the speech recogniser when it was recorded, so that students can be offered both text and speech help. Since slightly incorrect responses can still be counted as successful matches (most often, an article is inserted or deleted), a second pass is required to correct erroneous transcriptions. This is done efficiently by creating an editable HTML table which includes both transcriptions and links to the associated speech files.

Lesson structure
For pedagogical reasons, it is desirable to group the examples into thematic units; we call these units "lessons". The most straightforward alternative is to divide up the corpus into a number of possibly overlapping sets, each set corresponding to a lesson. The unifying theme of a lesson will typically be either the language required to carry out a concrete task (booking a ticket, ordering at a restaurant, buying clothes), or one or more types of grammatical construction (numbers, dates, simple questions). In the latter case, it is also possible to define the content of each lesson by listing the semantic properties (grammar rules used, subtrees in the parse-tree, or lexical items).
Grouping examples into lessons creates structure and makes the activity of practicing with the system feel more focussed and meaningful. This suggested to us that introducing further structure might be worthwhile. To this end, the most recent version of the system allows the course designer to add a simple dialogue script to the lesson. The script, written in a minimal XML notation, defines a number of steps, typically about 10 to 20; the specification of each step includes a unique <!--Ask for number of nights --> <step> <id>ask_for_number_nights</id> <multimedia>how_many_nights</multimedia> <group>room_for_number_of_nights</group> <repeat>ask_for_number_nights</repeat> <limit>is_one_night_okay</limit> <success probability="25">not_available</success> <next_success>ask_type_of_room</next_success> </step> FIGURE 1 Example step from a lesson whose theme is "booking a hotel room". When the step is executed, the multimedia file how many nights shows a clip of a cartoon desk clerk asking the student how many nights they wish to stay for; the associated prompt will be taken from the group room for number of nights, and, rendered in the L1, will mean something like "request: room for three nights". The repeat tag says to repeat the step if the student's response is not accepted. If it is not accepted three times, the limit tag says to move to the step is one night okay, where the student is asked a simple yes-no question. Conversely, if the response is accepted, the two success tags say to move either to the step not available (25% probability) or otherwise to ask type of room. The step definition has been slightly simplified for expositional reasons.
ID, a group of prompts, a recorded multimedia file, and the steps to move to next depending on different conditions. Figure 1 shows a typical step.
Execution of a step proceeds as follows. The system plays the multimedia file and displays one of the prompts. The student responds (possibly after asking for help), and the system performs recognition, translation and matching to decide whether the response is accepted or rejected. Depending on the result, it either repeats the step or moves to a new one.

User feedback
The user feedback in the versions of CALL-SLT which we will describe here is the minimal possible: the system either accepts or rejects the student's response.
It would obviously be desirable in principle to provide more feedback, giving the student some idea of what they have done wrong when the system rejects. Unfortunately, experience shows that this information must be very reliable in order to be helpful, and that unreliable feedback is worse than useless. Simply rejecting is less confusing than rejecting and adding an explanation based on something that the student didn't actually say; highly reliable recognition of incorrect responses is, for obvious reasons, a challenging task.
Since doing the work reported in the current paper, we have carried out experiments with other versions of the system, which leave us guardedly optimistic that it may be possible to recognize certain specific types of incorrect response with high enough reliability. This idea is still at a preliminary stage, and will be reported elsewhere.

Web deployment and user interface
CALL-SLT is deployed over the web using a scalable architecture, developed by Paideia Inc, California and particularly designed for cloud-based computing. In common with similar platforms, like WAMI ( (Gruenstein et al., 2008); http://wami.csail.mit.edu) and the Nuance Mobile Developer Platform (NMDP; http://dragonmobile. nuancemobiledeveloper.com), it uses a client/server approach in which speech recognition is carried out on the server side; the Paideia architecture, however, goes further than these systems by performing dialogue management, application integration, and large-scale grammar-based language processing on the server, rather than just returning the results of recognition to the client. Another important difference is that speech is passed to the recognition processes in the form of files, rather than using streaming audio. Although this goes against the currently prevailing wisdom, we have found that there are compensating advantages, and that the performance hit, with a little care, can be reduced to only a couple of hundred milliseconds per recognition operation. Full details are presented in (Fuchs et al., 2012).
By moving almost all processing to the server, the client can be kept very simple. It only needs to be responsible for the graphical user interface, maintaining a small amount of state logic, performing recording and playback of audio, and requesting services from the remote peer. Versions of the client for standard browsers have been developed using Flash 11 in combination with ActionScript 3.0.
An important aspect of the GUI is the way the recognition button is used. Due to the limitations of the target platform (lack of an endpointing mechanism), we have adopted a push-and-hold solution, where the user has to keep the button pressed while speaking. The recorded audio packets are streamed to the server until the button is released. The latter signifies the end of the user speech, triggering the transition to the next step of the processing chain; recognising using the remote audio file, processing the result and returning a response to the client.

Designing content
We briefly describe the various types of content we have developed for use in CALL-SLT.
Early work, during the first year and a half of the project, was centred on the restaurant domain. We developed courses for several L2s, with most of the work focussing on English, French and Japanese. The courses were divided up into lessons by syntactic theme: for example, the French course (the most elaborate one), included lessons for singular and plural nouns, numbers, location expressions, different kinds of question construction, etc (Bouillon et al., 2011b).
Subsequently, work has diverged in several different directions. A basic tourist Japanese course was built together with Future University, Hakodate; here, the unusual idea was to focus on adjectives ("excellent", "difficult", "expensive" etc) to rapidly build up a basic communicative vocabulary. The course was tested over the Amazon Mechanical Turk (AMT), with some success (Rayner et al., 2011).
At the same time, a set of elementary French lesson was developed together with the University of Bologna, and tested in conjunction with one of their courses (Bouillon et al., 2011a); the topics covered included "greeting", "talking about my family" and "scheduling a meeting". A modified and abbreviated version of this course was adapted for use on mobile devices, and also tested over AMT; this work is described in detail in the next section.
Most recently, we have been developing an interactive multimedia course for teaching English to beginner German-speaking school students; some examples are shown earlier in §2.5. A first evaluation with real students was carried out in late 2013 and early 2014 .
In the next section, we describe in detail some of the more substantial evaluations we have carried out using the French L2 courses.

Evaluations
The central question we consider is an apparently simple one: does the system help students improve their generative language skills? Here, we summarise from this point of view the results of three concrete experiments carried out between 2011 and 2013.
One-day experiment using French/Chinese system A typical early study was the one described in (Bouillon et al., 2011b), where the subjects were 10 Chinese-speaking computer science students spending an exchange year in Tours, France. The students, who had previously done between one and two years of French in China and spent five months in France, were asked to use the French-for-Chinese version of the system, loaded with five sample lessons. They took part in two sessions, totalling about three hours in duration and yielding a total of 5245 recorded spoken interactions. Each spoken response was stored in recorded form, together with meta-data including the associated system prompt.
In the paper, we argued that the results provided evidence that subjects had learned from using the system. First, students had a higher proportion of utterances accepted by the system in the later utterances than in the earlier ones, this difference being statistically significant. Second, grammar and vocabulary tests carried out before and after the experiment showed large differences; most of the students appeared to have picked up some vocabulary, and there was also reason to believe that they had consolidated their knowledge of grammar.
Looking critically at the design, we can advance various objections against the validity of our conclusions. One obvious question is whether the fact that students have more utterances accepted by the system after they have used it for a while really does mean that they have improved their generative spoken language skills. Other explanations are a priori quite possible. In particular, they may only have become more skillful at using the interface, learning to speak in a way that is better adapted to the machine, but not necessarily better in itself.

Contrastive judging of data from first experiment
The follow-on experiments described in (Rayner et al., 2012a) were designed to investigate how much substance there was to these potential criticisms. To this end, we collated the data so as to find cases where a) the same student had responded more than once to the same prompt, and b) at least one example had been accepted, and at least one rejected. For each such group, we randomly selected one recorded file which had been accepted and one which had been rejected, giving us 413 pairs. An initial sampling of the data quickly revealed that, in many cases, the most important characteristic was that one or both files had been badly recorded. (Among other things, the experiment had been carried out in a small room with bad acoustics). We consequently divided judging into two rounds. During the first round, two system experts listened to all the pairs, and marked ones which exhibited recording problems: this accounted for 243 pairs, about 56% of the data.
The remaining 170 pairs were then judged by three French native speakers, all of whom had worked as French language teachers. None of them had previously been associated with the project or knew the exact point of the evaluation exercise: in particular, we were careful not to tell them that each pair consisted of one successful and one unsuccessful recognition match. Judges were asked to mark each pair to say which element, if either, was better in terms of speech (pronunciation/prosody), vocabulary and grammar. Judging was performed using AMT, with the judges paid a zero fee. This allowed us to distribute work efficiently over the Web and also simplified the task of writing the judging interface, which could be specified straightforwardly in HTML.

Judge
Agree  2 Agreement between system responses and human judgements on 170 well-recorded contrastive pairs. "Agree" means the judge(s) marked the element of the pair accepted by the system as better; "Disagree" means they marked it as worse; "Null" means no preference.
The results are shown in Table 2. For each judge, we list the number of pairs on which they explicitly agree with the system (i.e. the judge considered that the accepted element of the pair was better) and the number where they explicitly disagree (the judge preferred the rejected element). If the judge did not express a preference with respect to any of the specified criteria, we counted the pair as being neither an agreement nor a disagreement. We also list results for aggregated judgements that are "unanimous" (all three judges), "majority" (at least two out of three judges) and "at-least-1" (at least one judge).
The notion of "quality of spoken response" is slippery; since we refrained from giving detailed guidelines, we were not surprised to see a fair degree of disagreement between the three judges. Even with respect to vocabulary and grammar, which one might expect to be reasonably uncontroversial, we found many differing judgements. For example, one judge thought a full sentence was grammatically better than a nominal phrase, while the other two considered them equally good. However, when we look at the "majority" judgements, we find a reassuring correlation between the human and mechanical evaluations; the judges agreed with the recogniser three times as often as they disagreed with it (90 versus 30). It is also worth noting that there are few cases of unanimous disagreements, and that, even when all the judges unanimously disagree with the recogniser, they often do not disagree for the same reasons: for example, one judge may think that the rejected utterance was better due to pronunciation, and another due to grammar.

AMT-based evaluation using a control group
With the above results in mind, we decided to attempt a more ambitious evaluation that would address some of the issues that had arisen. We start by outlining the methodological problems, then describe the experiment itself.

Evaluation methodology
The experiment described immediately above suggests that there is a reasonable correlation between the quality of the students' speech and the frequency with which the system accepts their utterances; if students get more utterances accepted, this can thus reasonably be taken as evidence that they have improved their generative language abilities. Unfortunately, even if the results unambiguously show that the student has improved over a given period, it is still not clear what has caused the improvement. This problem is particularly acute when use of the system is integrated into a formal language course, as in (Bouillon et al., 2011a(Bouillon et al., , 2012; given that the student is also receiving other kinds of instruction, it is obviously possible that any improvement measured is independent of use of the system. Even if the student is only learning through use of the system, at least over the duration of the experiment, it is still unclear which aspects of the system are responsible for the improvement. In an application like CALL-SLT, the student spends a large part of their time listening and repeating, which may well be helpful for them. It remains to be shown that any of the more sophisticated system functionalities are useful in practice. In particular, the obvious question is whether we can find concrete evidence to show that speech recognition feedback, which can never be more than partially reliable, is actually assisting the learning process. The only straightforward way to demonstrate this is to find some way to compare a version of the system which has recognition feedback against one that lacks it, and find a clear difference. The question is how to organise an experiment to perform a comparison of this kind. A natural idea is to separate the students into two groups, a main group and a control; the first group uses the system with recognition, and the second the one without. Unfortunately, ex-perience has shown that there are many practical problems with this design, partly because motivation is always an important factor in language learning. For example, suppose, as in e.g. (Coyne et al., 2011), that we pick subjects randomly from one class, assigning half of them to the group using the system and the other half to the control. The two groups of students will talk to each other. If the system is perceived as useful, which the authors claim in the cited study, it is reasonable to wonder whether students in the control group felt correspondingly unmotivated; it is methodologically better if no subject is aware that any version exists except the one they are using.
If, on the other hand, we take the two groups from two different classes that have no contact with each other, not mixing them, it is impossible to know whether the classes are comparable. Most teachers we have asked say their experience suggests high variability between classes. Yet another possibility is to use a crossover methodology, letting students in the same class alternate between the two groups. Some clear successes have been claimed for this methodology, in particular by the LISTEN project (Poulsen, 2004, Reeder et al., 2007, Korsah et al., 2010; if the learning effect from using the system is large enough, as appears to be the case there, it is reasonable to hope for a clear result. There are however many known problems with crossover, since it is difficult to account correctly for the effect of using the main system and the control version in different orders. In the context of CALL, students may once again be disappointed if they like the main system and are then forced to use the inferior control, and react accordingly. For the kinds of reasons just given, it has often been argued that experiments with control groups are unproductive in CALL (Kulik et al., 1980), and that single-case design methodologies (Kennedy, 2005) are more appropriate. The central idea of the single-case methodology is that the student acts as their own control. There is an initial period where the student is exposed to the baseline condition; this needs to continue long enough for a rate of progress to be reliably estimated. The new condition is then introduced, and the critical measure is the difference in the student's rate of progress between the baseline period and the period where the new condition applies. Here, too, the experimental design is fraught with difficulties if we wish to apply it to a test of the kind we are considering. We would have to develop sufficient course material to allow students to use the baseline system for a period long enough to estimate their initial rate of progress; lack of uniformity of the material would mean that it had to be tried in many different orders; and it is not obvious how to correct for the fact that students who have become used to the baseline version are then obliged to reac-climatize to the enhanced one when they reach the crossover point. Note that the "AB" design (baseline followed by intervention) is the best case; versions in which intervention is followed by baseline are even more problematic, since students are likely to be disappointed by going back to a version they perceive as inferior.
It may seem that there is no satisfactory solution, and that the best we can do is rely on informal assessments based on subjective teacher impressions. Recently, however, the introduction of crowdsourcing platforms has opened up new possibilities (Jurcicek et al., 2011, Eskenazi et al., 2013. In a large, diverse online community, it is not unreasonable to hope that most subjects will have no contact with each other; under circumstances like these, the design with two separated groups becomes more like the "randomized clinical trial" design typical of medical studies, and is correspondingly more plausible.

Experiment
In the remainder of this section, we describe a crowdsourced experiment with two separated groups, carried out in early 2013 using a multimedia-enabled Android phone version of the French CALL-SLT system. We only set ourselves the modest goal of establishing that use of speech recognition feedback produced a significant difference in shortterm learning outcomes. A more elaborate experiment would also have investigated the question of how well subjects retained the knowledge they had acquired, but this would have required much greater resources than we had available.
The main content of the course used consisted of four lessons, aboutme (simple questions about the subject's age, where they live, etc); about-my-family (similar questions about family members); restaurant (ordering in a restaurant) and time-and-day (times and days of the week). Three additional lessons called overview-1, overview-2 and revision will be described shortly. The course was designed for students with little or no previous knowledge of French. It covered about 80 words of vocabulary and a dozen or so basic grammatical patterns.
We created four different versions of the basic system. Three of them differed only in the way the multimedia part of the prompt was realised: in video it had the form of a recorded video segment of a human speaker, in avatar it was an animated avatar, and in text it was a piece of text. The fourth version, no-rec, was the same as video, except that the student was given no feedback to show whether speech recognition and subsequent processing had accepted or rejected their response.
Subjects were recruited through AMT; we requested only workers from the US. After discovering during a previous study (Rayner et al., 2011) that experiments of this kind can easily attract scammers, we required all workers to have a track record of at least 50 previously completed Human Interface Tasks (HITs), at least 80% of which had been accepted.
The experiment was carried out in two cycles, each of which had the same sequence of eight HITs. In the first HIT, the task was to check that one version of the app (we chose no-rec) could be successfully run on an Android phone. Subjects who gave a positive response were then randomly assigned to the four different versions of the system and given different versions of the subsequent HITs. AMT "qualifications" were used so that subjects doing one version of a HIT were unable to see that HITs for other versions existed. The seven HITs were issued at 24-hour intervals; workers were paid $1.00 for the first HIT and $2.00 for each subsequent one, reasonable pay by AMT standards. The HITs had the following content: Pre-test: The student was asked to do overview-1 and overview-2, each of which consisted of a balanced selection of examples from the other lessons. During overview-1, they were encouraged to use the Help function as much as they wished, so the main skill being tested was ability to imitate. In overview-2, Help was switched off, so the main skill tested was generative ability in spoken French. Lessons 1-4: The student was asked to attempt each of the four lessons in turn, one lesson per HIT, with Help turned on. They were told to spend a minimum of 20 minutes practising, and speak to the system at least 25 times. Revision: The student was warned that the next HIT would be a test (they were not told what it was), and was asked to revise by doing the revision lesson, which contained the union of the material from the four main lessons, for at least 20 minutes.
Post-test: The student was asked to do overview-1 and overview-2 again. They were told that the intent was to measure how much they had learned during the course, and were asked to do the test straightforwardly without cheating.
In the first cycle, we started with 100 subjects. The second column of Table 3 shows the number of students left in play after each round of HITs. At the end of the cycle, there were 17 students who had completed both the pre-and post-tests. A preliminary examination of the results suggested that students performed similarly on the three versions which gave recognition feedback, but worse on no-rec; there was not, however, sufficient data to be able to draw any significant conclusions.
We decided that the most interesting way to continue the experiment was to collect more data for no-rec; in the second cycle, we consequently started with 30 subjects, assigning all of them to the norec group. The third column of Table 3 shows the number left after each round. At the end of the cycle, we had adequate data for 12 subjects in no-rec and 12 in the union of the three groups which included recognition feedback, which we will call rec.
The analysis in the next section focusses on exploring the difference between no-rec and rec, and our basic strategy is as follows. For each of the two versions, we compare student performance in the pre-and post-tests; we wish to determine whether this difference is significantly larger in rec than in no-rec. The pre-and post-tests are the same 2 and consist of two halves. The first half ("with-help", i.e. online help was available) contains 13 2 We wondered if it was methodologically sound to use the same items for the pre-and post-tests. Students were however going to take the two tests at least a week apart, during which they would practice many similar examples. We felt it was unlikely that they would remember the specific sentences from the pre-test, and that it was more important to give ourselves the option of performing a clear item-by-item comparison.
Prompt BETTER-SAME-WORSE, score rec no-rec Without help P14 3-8-0 27.3 4-7-1 25.0 P15 3-7-1 18.2 1-10-1 0.0 P16 3-5-2 10.0 4-6-0 40.0 P17 4-4-3 9.1 3-6-2 9.1 P18 1-10-0 9.1 2-9-0 18. 3-6-0 33.3 3-9-0 25.0 prompts; the second ("without-help", i.e. online help was not available) contains 15 prompts. We compare a given student's performance on each prompt by determining whether the system accepts the student's response or not. As already noted, this correlates reasonably with human judgements. Students can get BETTER (not recognised in pre-, recognised in post-), WORSE (recognised in pre-, not recognised in post-), or stay the SAME (identical outcomes in both tests). We can compare either across students or across prompts. The simplest way to compare across students is to take each student and count how many examples of BETTER/WORSE/SAME (B/W/S) they get. We can then look at the difference between BETTER and WORSE using the McNemar test to find how significant it is (Table 4); note that B + S + W does not always total to 28, since students sometimes omitted a few items from one or both tests. The comparison turns up four students in the rec group who get a significant difference, against three in no-rec; in the right direction, but obviously not strong evidence that rec is better. Other more complex tests also failed to show a statistically significant difference when we compared across all students, though some were close. It is however worth noting that we do get a significant difference on the two-tail t-test (t = 1.7, df = 11, p < 0.01) when we use only the subset of students, underlined in the table, who described themselves as beginners. The fact that some students in the control group improve should not be regarded as surprising, since one expects simple listening and repeating to be useful; this is, indeed, exactly why we need the control group (or some other kind of controlled methodology) in order to make claims about the utility of speech recognition feedback.
Comparing across prompts produces a convincing result even when we use all the students (Tables 5 and 6). This time, we look at all the B/W/S scores for a given prompt and version, using the measure (B − W )/(B + W + S). The value will be 100% if every example is BETTER, zero if BETTER and WORSE are equal, and -100% if every example is WORSE.
We can now perform a prompt-by-prompt comparison of rec and no-rec, contrasting the scores. For example, looking at prompt P11, we have under rec B = 4, S = 6 and W = 1, giving a score of (4 − 1)/(4 + 6 + 1) = 3/11 = 27%. Under no-rec, we have B = 3, S = 5 and W = 4, giving a score of -8.3%. Applying the Wilcoxon signedrank test to the whole set of prompts, the comparison between rec and no-rec on the above measure yields a difference significant at p < 0.02.

Summary and discussion
We have presented an overview of CALL-SLT, a spoken CALL application implemented using grammar and rule-based translation technologies. The current system has the status of a mature prototype; there are versions for several languages, over 50 lessons of content, and a stable web deployment. We have been able to use it to carry out substantial evaluations, which yield reasonable evidence that students who use it actually do learn compared with a simpler control system that lacks speech recognition capabilities.
When we talk to people who have used the system, our impression is that there are three main problems. First, recognition is currently too unforgiving; students often feel that they have pronounced the response adequately, but the system has still rejected them. This agrees well with comments we have seen from other people building spoken CALL systems, who generally report users as preferring false positives to false negatives. It is probably advisable to move the balance in this direction.
Second, there is not enough content; enthusiastic students (usually something between a quarter and a half of the whole group) finish all the existing lesson modules, and say they would happily do more if it was there. Without implementing more content, it is impossible to determine how useful the tool could be to them in the long term. The process of creating new lessons is still too slow and requires too much system expertise; as usual with grammar-based systems, some steps can only be performed by personnel who are intimately familiar with the grammar. The most feasible way to address this problem is to build up a large enough stock of examples that further content can be added using a copy-and-edit strategy. It is not yet clear how large the set of examples would need to be, but a reasonable guess is that it should at any rate be less than an order-of-magnitude increase compared to the current set.
Finally, the application is still experienced by many students, particularly younger ones, as boring and monotonous; it is largely due to feedback from evaluations on the 10 to 12 year old age group that we have started experimenting with script-based lessons that add a narrative flow to the learning experience. Initial results here have been very positive, and are reported in .