Gyorgy Csoka
email: csokagy@erti.hu

Aniko Hirka

Serap Mutun

Milka Glavendekic

Agnes Miko

Levente Szocs

Csaba Marton Paulin

Bela Eotvos

Csaba Gaspar

György Csóka

Anikó Hirka

Milka Glavendekić

Ágnes Mikó

; Levente Szőcs

; Márton Paulin

Csaba Béla Eötvös

Csaba Gáspár

Mariann Csepelényi

Ágnes Szénási

Milivoj Franjevic

Yuri Gninenko

Mirza Dautbašić

Osman Mujezinovic

Milan Zubrik

Constantin Netoiu

Andrei Buzatu

; Flavius Bălăcenoiu

Maja Jurc

Dusan Jurc

Iris Bernardinelli

Jean-Claude Streito

Dimitrios Avtzis

Boris Hrašovec

Spread and potential host range of the invasive oak lace bug [Corythucha arcuata (Say, 1832) -Heteroptera: Tingidae] in Eurasia

Keywords: Corythucha arcuata, host plants, non-native species, sentinel gardens, Quercus spp

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

Insects are among the most numerous invaders worldwide [START_REF] Kenis | Impact of alien terrestrial arthropods in Europe. Chapter 5[END_REF]Brockerhoff & Liebhold, 2017), and make up ca. 87% of the non-native arthropods introduced in Europe [START_REF] Roques | Taxonomy, time and geographic patterns[END_REF]. Non-native insect species have appeared at an alarmingly increasing rate in Europe in recent decades [START_REF] Roques | Taxonomy, time and geographic patterns[END_REF][START_REF] Kenis | Impact of alien terrestrial arthropods in Europe. Chapter 5[END_REF][START_REF] Csóka | Rovarglobalizáció a magyar erdőkben[END_REF][START_REF] Tuba | Inváziós rovarok fás növényeken[END_REF][START_REF] Smith | Recent trends in non-native, invertebrate, plant pest establishments in Great Britain, accounting for time lags in reporting[END_REF]. While some non-native insects spread slowly and do not cause detectable economic/ecological damage, others become invasive, rapidly expand their range and subsequently have rather severe effects within newly invaded area. Examples of recent rapid spreads within Europe are provided among many others by Obolodiplosis robiniae (Skuhrava et al., 2007), Harmonia axyridis [START_REF] Roy | The harlequin ladybird, Harmonia axyridis: global perspectives on invasion history and ecology[END_REF], Leptoglossus occidentalis [START_REF] Lesieur | The rapid spread of Leptoglossus occidentalis in Europe: a bridgehead invasion[END_REF] and Halyomorpha halys [START_REF] Vétek | The invasive brown marmorated stink bug (Halyomorpha halys) is now widespread in Hungary[END_REF]. Non-native species, on top of their potential of causing significant economic losses, may have impacts on natural processes in ecosystem functions [START_REF] Simberloff | Biological invasions -How are they affecting us, and what can we do about them?[END_REF][START_REF] Simberloff | How common are invasion-induced ecosystem impacts?[END_REF]Kenis et al., 2009;[START_REF] Wardle | Impacts of invasive biota in forest ecosystems in an aboveground-belowground context[END_REF][START_REF] Liebhold | Biological invasions in forest ecosystems: a global problem requiring international and multidisciplinary integration[END_REF].

One of the major determinants regarding a non-native insect's potential to become invasive is the availability of its hosts. If suitable hosts are absent or very rare in the newly invaded territory, the non-native insect species has limited chance to establish and become invasive.

The oak lace bug (Corythucha arcuata Say, 1832 -Heteroptera: Tingidae; abbreviated as "OLB" further on) is native and widespread in the eastern part of the United States and across southern Canada [START_REF] Barber | Light Environment and Leaf Characteristics Affect Distribution of Corythucha arcuata (Hemiptera: Tingidae)[END_REF]. The known host records from its native range are listed in Table 1. Surprisingly, only seven oak species out of more than 40 native to North America are named at the species level (Table 1). Most literature sources refer to the hosts of OLB as oaks, or slightly more accurately white oaks (section Quercus in genus Quercus). [START_REF] Morrill | Notes on the immature stages of some tingitids of the genus Corythucha[END_REF] also recorded "English oak" (Quercus robur) as a preferred host in Massachusetts, but he used the scientific name of this species incorrectly (he gave Q. rubra instead of Q. robur). Non-oak hosts include Castanea dentata, Acer spp., Malus spp., Pyrus spp., and Rosa spp. without accurate species names [START_REF] Connell | Life history and control of the oak lace bug[END_REF][START_REF] Drake | Lacebugs of the world: A catalog (Hemiptera: Tingidae)[END_REF][START_REF] Drew | Tingoidea of Oklahoma (Hemiptera)[END_REF].

OLB was first discovered in Europe, in northern Italy in 2000 [START_REF] Bernardinelli | Distribution of the Oak lace bug Corythucha arcuata (Say) in northern Italy (Heteroptera Tingidae)[END_REF][START_REF] Bernardinelli | Prima segnalozione di Corythucha arcuata (Say) (Heteroptera, Tingidae) in Europe[END_REF] This article is protected by copyright. All rights reserved.

flight interception trap in southern Switzerland [START_REF] Forster | Die amerikanische Eichennetzwanze Corythucha arcuata (Say) (Heteroptera, Tingidae) hat die Südschweiz erreicht[END_REF]. In the same year, OLB was found for the first time in Turkey, about 200 km east of Istanbul [START_REF] Mutun | First report of the oak lace bug, Corythucha arcuata (Say, 1832) (Heteroptera: Tingidae) from Bolu, Turkey[END_REF]. One specimen was found in Iran (Western Azerbaidjan) in 2005 (Samin & Linnavouri, 2011). By the summer of 2008, the distribution expanded significantly, reaching 28,000 km 2 only in Turkey [START_REF] Mutun | Invasion by the Oak Lace Bug, Corythucha arcuata (Say) (Heteroptera: Tingidae), in Turkey[END_REF]. This population build-up in western Asia most likely acted as a prolific source for the spread north through the Balkans. However, a human-mediated accidental introduction from northern Italy to other countries could not be excluded.

In July 2012, OLB was found in Bulgaria [START_REF] Dobreva | First record of Corythucha arcuata (Say) (Heteroptera: Tingidae) on Balkan Peninsula[END_REF]. One year later, it appeared in Hungary [START_REF] Csóka | A tölgy csipkéspoloska (Corythucha arcuata Say, 1832 -Hemiptera, Tingidae) első észlelése Magyarországon[END_REF], and was recorded at two distant (140 km in a straight line) locations almost at the same time. In 2013, it was also discovered in Croatia [START_REF] Hrašovec | Prvi nalaz hrastove mrezaste stjenice (Corythucha arcuata) u Hrvatskoj[END_REF] and Serbia [START_REF] Poljaković-Pajnik | Pojava velikih šteta od Corythucha arcuata (Say) (Heteroptera: Tingidae) u šumama hrasta u Vojvodini. XIII savetovanje o zaštiti bilja[END_REF][START_REF] Pap | Monitoring zdravstvenog stanja šuma na teritoriji Vojvodine u 2015[END_REF][START_REF] Glavendekić | Fauna i ekologija insekata koji naseljavaju invazivne i nativne ukrasne biljke u "Ukrasne i invazivne biljke u uslovima klimatskih promena -uticaji i adaptacije[END_REF]. In Russia, OLB was first found in Krasnodar in 2015 [START_REF] Neimorovets | First Documented Outbreak and New Data on the Distribution of Corythucha arcuata (Say, 1832) (Hemiptera: Tingidae) in Russia[END_REF]. OLB was detected for the first time in 2016, again in several countries: Albania (E. Cota's pers. comm.), at two locations in Romania, rather far (at least 400 km) from each other [START_REF] Don | Insect pests on the trees and shrubs from the Macea Botanical Garden[END_REF][START_REF] Chireceanu | First record of oak lace bug Corythucha (Tingidae: Heteroptera) in Romania[END_REF]. In autumn 2016, Jurc & Jurc (2017) also recorded it in Slovenia, close to the Croatian border. In Bosnia and Herzegovina, the first observation dates from 2017 [START_REF] Glavendekić | Prvi nalaz hrastove mrežaste stenice Corythucha arcuata (Say) (Hemiptera: Tingidae) u Bosni i Hercegovini i novi nalazi u Srbiji, Zbornik rezimea XI Simpozijuma entomologa Srbije[END_REF][START_REF] Dautbašić | Prvi nalaz hrastove mrežaste stjenice (Corythucha arcuata) u Bosni i Hercegovini[END_REF]. In the same year it was detected in southwestern France [START_REF] Streito | Corythucha arcuata (Say, 1832) et Stephanitis lauri Rietschel, 2014, deux espèces invasives nouvelles pour la faune de France (Hemiptera, Tingidae)[END_REF]. In 2017, it was also found in southern Ukraine (V. Meshkova's pers. comm.). In May 2018, OLB has been recorded in northeastern Greece (D. Avtzis' pers. comm.) and in June 2018, in southern Slovakia (Zúbrik et al., 2018). A screening in south-eastern Austria in September 2019 confirmed its occurrence at 21 sites (Sallmanshofer et al., 2019). Following the first records, fast range expansions were reported from almost all the countries (Csepelényi et al., 2017a;[START_REF] Simov | Rapid expansion of the Oak lace bug Corythucha arcuata (Say, 1832) (Hemiptera: Tingidae) in Bulgaria[END_REF]. It should also be mentioned that the temporal sequence of the first records in different countries does not necessarily reflect a real pattern of the spread relating to time. It is more likely related to the timing of the intensive search after the species appeared in the given country. The countries where and the years when OLB Although OLB adults can actively fly and they can also be passively dispersed by wind, their long-term dispersal is generally related to international road and rail traffic. The first infested locations in a

This article is protected by copyright. All rights reserved.

given region were often found at resting places near motorways or along rail lines (authors' unpublished observation).

By autumn 2016, the total area of invaded oak forests was about one million hectares in Russia, of which about 0.4 million was severely infested (oak crowns in large groups or in whole forest blocks suffered early discoloration exceeding 50% level). The total extent of the outbreak areas in 2017 exceeded 1.3 million hectares, in the oak forests of the Krasnodar Territory and the Republic of Adygea. Currently, the bug has spread to all the oak forests of the Black Sea coast, of the Krasnodar Krai region, from Anapa to the state border. There is still no indication that OLB has reached its potential distribution limits in Europe and Asia.

In this paper, we are summarising the present information available on the range expansion in Europe and the host range of the accidentally introduced and rapidly spreading invasive North American oak lace bug. In order to predict its further potential regarding hosts use in the invaded range, and the risk of its further area expansion, we checked 48 oak species in 20 sentinel gardens in seven countries between 2013 and 2018. These gardens can provide valuable data on the host range of non-native pests or pathogens [START_REF] Roques | Field guide for the identification of damage on woody sentinel plants[END_REF][START_REF] Vettraino | The sentinel tree nursery as an early warning system for pathway risk assessment: Fungal pathogens associated with Chinese woody plants commonly shipped to Europe[END_REF]. The data on potential host use is very important to to evaluate and predict the potential to spread and cause damage.

Methods

We have been collecting data intensively on host use since 2013 in 20 sentinel gardens (i.e. botanical gardens and arboretums) in seven countries (Croatia, Hungary, Italy, Romania, Serbia, Slovakia, Slovenia) and forest stands in eleven ones (Bosnia and Herzegovina, Bulgaria, Croatia, Hungary, Italy, Romania, Russia, Serbia, Slovakia, Slovenia and Turkey). A list of the sentinel gardens is given in Table 2 and shown in Figure 2.

A total of 15 sentinel gardens were located in an area already invaded by the oak lace bug, and five of them were outside of the presently known range. These five (two in Hungary, two in Slovakia and one in Slovenia) were also checked for the presence of OLB since we consider arboretums and botanical gardens as potential "hot spots" of non-native insects and early detection points. We assumed that invasive OLB might appear in such places even far from the core invaded area. We also collected information from the oak stands of the countries where OLB's presence was known for at least two years. Although the discolouration of the infested leaves is typical, we always checked the affected trees for presence of adults, moulted skins of larvae and egg clusters. These together can provide unequivocal signs of a plant being utilised as a host. We did not consider a tree species as a host if only adults were found on it. As an easily and passively spreading species, OLB can often land and be on plants which are not suitable hosts.

The overwintered adults can be found on the underside of leaves from April. Egg bunches are present from early May, larvae appear later in May. As OLB may have three overlapping generations per season, all developmental stages are noticed on the foliage from June until October.

The arboretums and botanical gardens in Hungary were visited two to six times, most of the sentinel gardens outside this country were visited once (see Table 2). The surveys (both in sentinel gardens and autochthonous oak stands) were made once a year from mid-July to late September. By this time, the symptoms become easily noticeable and unambiguous. Sample branches were regularly cut using long-handled loppers to check the presence of the different developmental stages.

The number of locations and of trees from different oak species varied depending on the species.

The oaks native in the region were regularly sampled (>10) and at many locations (>10), the most exotic ones were generally rare and restricted to few places. While specimens of Quercus robur, for example, were present as a number of individual trees in most of the botanical gardens/arboretums surveyed, only single individual trees of some other species (i.e. Q. aliena, Q. gambelii, Q. imeretina, etc.) were available at one site only. This fact would make the statistical analysis of host preference rather difficult.

Oak stands were also surveyed by the authors in ten countries (Bosnia and Herzegovina, Bulgaria, Croatia, Hungary, Italy, Romania, Russia, Serbia, Slovenia and Turkey). The levels of infestation were classified as described below. The number of oak stands that were surveyed cannot be given precisely, but the total area reaches several thousand hectares. In different native oak stands, regularly no survey of single trees was necessary, since in most cases larger groups of them or even whole stands were severely infested, providing easily detectable symptoms. We categorised the infestation level on a 0-3 scale. The scale is described as follows:

This article is protected by copyright. All rights reserved.

0:

No symptoms.

1:

Symptoms/different developmental stages of OLB are sporadic, restricted to single leaf or smaller groups of them and can only be found with targeted, intensive search.

2:

Symptoms/different developmental stages of OLB are found along whole branches that can easily be spotted on the tree.

3:

Symptoms/different developmental stages of OLB cover whole trees or groups of them, sometimes even extensive stands of many hectares. Heavily infested trees/stands can be safely spotted from larger distance, or for instance with drones.

Results

Oak Hosts

We checked 48 different oak species in 20 sentinel gardens in seven countries. Presence of OLB was recorded at 15 locations in five countries (Croatia, Hungary, Italy, Romania and Serbia). A total of 27 out of 48 oak species were proved to be suitable OLB hosts. They are listed in Table 3. Only the locations with recorded presence of OLB are included in it. Of these 27, 15 were globally new host records for OLB (underlined in Table 3). The share of each intrageneric taxonomic unit from genus

Quercus can be seen in Figure 3. Out of 29 species surveyed in section Quercus (white oaks), 23

(79.3%) can be hosts of the OLB, four out of the five ones (80%) belonging to section Cerris are suitable for it, and three of them were heavily infested at almost all locations. No symptoms were recorded on any of the North American red oaks within the section Lobatae and no species in the Ilex group (Mediterranean evergreen oaks) showed some of infestation (Table 3).

In forest stands of the ten countries involved in this study, we found 11 species of oaks (autochthonous in the given country) infested by OLB at different levels (Table 4 and Figure 4). All species showed signs of heavy infestation in some countries. So far, outbreak populations have most often been detected in Q. robur, Q. frainetto, Q. petraea, and Q. cerris stands.

This article is protected by copyright. All rights reserved.

Non-Oak Hosts

Thirty-three species of non-oak woody hosts belonging to ten plant families have been recorded in eight countries. These host records are provided in Table 5. Many of them are new host records.

Discussion

OLB's widely accepted host species belong to the two major sections of the genus Quercus (Quercus and Cerris). The taxonomic relatedness of the oak species included in this study seems to be a more important factor than their native ranges. White oaks (section Quercus) were infested almost independently from their native ranges, except for the North American ones, naturally present on the western coast of the USA. One species (Q. gambelii) showed a low level of infestation, the other one (Q. garryana) was not attacked. However, it should be mentioned that these species were represented by only single (and small) tree at only one botanical garden (Vácrátót, Hungary). Heavily infested species can be found both among the North American (Q. alba, Q. macrocarpa, etc.), European (Q. robur, Q. petraea, etc.) and even species with Far East origin (Q. dentata, Q. mongolica). Only one species from the section Cerris (Q. acutissima -native to Eastern Asia) was unattacked, but, this species was only surveyed at one place (Vácrátót, Hungary).

From our observations it is quite clear that the red oaks (section Lobatae) are not suitable hosts for OLB. None of these species (with one exception, see below) showed any signs of infestation, although most of them grow in a rather exposed environment, surrounded by heavily infested suitable hosts. We found only a very small (less than 1 cm 2 ) spot with symptoms on Q. imbricaria (Szarvas, Hungary, 2015), but dead larvae were surrounding it, therefore we do not consider this oak species a suitable host. These results coincide with the observations of [START_REF] Morrill | Notes on the immature stages of some tingitids of the genus Corythucha[END_REF], who reported three species of red oaks (Q. coccinea, Q. ilicifolia, Q. laurifolia) remained unaffected "although they stood so near to badly infested trees that their branches touched in some cases". [START_REF] Trieff | Composition of the Coleoptera and Associated Insects Collected by Canopy Fogging of Northern Red Oak (Quercus rubra L.) Trees in the Great Smoky Mountains National Park and The University of Tennessee Arboretum[END_REF] found OLB adults in the canopy of Quercus rubra during a knockdown fogging experiment in the USA.

However, presence of adults itself does not provide proof that Quercus rubra is a suitable host, as it was mentioned earlier. Our results are also similar to those of Bernardinelli (2006a, b) who found the North American Q. rubra as unsuitable, versus native European oaks that are.

This article is protected by copyright. All rights reserved.

None of the three oak species belonging to the Ilex group had any feeding symptoms in the arboretums and botanical gardens visited. However, in a sentinel experiment in Croatia (seedlings were placed under a heavily infested Q. robur stand), even these species (Q. ilex and Q. coccifera)

showed sporadic small symptoms of sucking. Therefore, it can be concluded that OLB's preferred hosts are present in the majority of the Europe. It should also be mentioned again that many central and even eastern Asian oaks (including natives of Japan, Korea and China) are suitable OLB hosts.

These are globally new host records for OLB, meaning that eastbound range expansion of OLB is unlikely to be restricted by host availability. In surveys at the stand level, not surprisingly, Q. cerris, Q. petraea, Q. pubescens and particularly Q. robur were recorded as being most heavily attacked in all countries. These species are widely distributed and are among the most abundant on trees in the surveyed region. Summed up, only these four species are covering together more than 10 million hectares of forested land in Europe.

Climate may influence significantly the establishment and further spread of the non-native invasive insects. The milder and shorter winters could do it on the higher overwintering survival and the timing of spring emergence resulting more generations per year [START_REF] Berzitis | Winter warming effects on overwinter survival, energy use, and spring emergence of Cerotoma trifurcata (Coleoptera: Chrysomelidae)[END_REF]Pap et al., 2018;[START_REF] Smith | Recent trends in non-native, invertebrate, plant pest establishments in Great Britain, accounting for time lags in reporting[END_REF][START_REF] Ward | Cold tolerance of the invasive larch casebearer and implications for invasion success[END_REF]. Bernardinelli (2006b) compared climatic conditions of the native North American range and Europe and concluded that most of the latter is likely to provide suitable conditions for the establishment of OLB. In a recent study (Csepelényi et al., 2017b), it was found that the relatively cold winter of 2016/2017 did not cause high overwintering mortality

(not exceeding 50%) at two locations in south-eastern Hungary.

The long-term impact of the OLB damage is not yet known, but there are good reasons to assume that the "chronic" infestations will negatively influence in a significant manner the growth, health status and fecundity of the oak stands which already suffer from both the direct and indirect effects of climate change [START_REF] Csóka | Increased insect damage in Hungarian forests under drought impact[END_REF][START_REF] Csóka | Az aszályosság hatása kocsánytalan tölgyeseink és bükköseink egészségi állapotára[END_REF]. The heavily attacked leaves lose most of the chlorophyll in their upper surface, while the one in their underside tissues remains relatively unharmed. This is particularly important in terms of photosynthesis since ca. 80% of this process takes place in the palisade clorenchyma of the leaf upper surface [START_REF] Lambers | Physiological Plant Ecology[END_REF]. According to a recent Serbian study, the rate of photosynthetic and transpiration activity as well as the stomatal conductance decreased by 58.84%, 21.66% and 35.71%, respectively, compared to non-infested plants [START_REF] Nikolić | Physiological responses of pedunculate oak (Quercus robur L.) to Corythucha arcuata (Say, 1832) attack[END_REF]. An unpublished study in Hungary resulted in a similar loss regarding the This article is protected by copyright. All rights reserved.

photosynthetic activity in late June, at above 50% of the degree of leaf discolouration (I. Mészáros' pers. comm.). Further targeted experiments should be established in order to clarify OLB's long-term impact on health, growth and fecundity of the infested oaks.

It is also still unknown how the mass presence of OLB will influence the extremely species-rich herbivorous insect communities thriving on European oaks. Only in Hungary, at least 650 herbivore insect species were recorded feeding on oaks and more than 40% of them are strictly specialists [START_REF] Csóka | A Magyarországon honos tölgyek herbivor rovaregyüttese[END_REF]2006;[START_REF] Csóka | Checklist of Herbivorous Insects of Native and Exotic Oaks in Hungary I (Lepidoptera)[END_REF]. Our survey in sentinel gardens and forest stands must be considered as an early, but evidently "snapshot" warning. By this, we mean that both the number of affected oak species and the level of infestation are likely to grow in the near future, particularly in most recently invaded areas. The host range, based on our results, could be considered as a "minimum" one. The datasets collected during our survey allows us to predict a further large-scale spread and even a wider host range within both Europe and Asia.

Insect outbreaks sometimes provoke otherwise unexpected host shifting together with range expansion [START_REF] Castagneyrol | Host range expansion is density dependent[END_REF]. As a consequence, we recorded 28 plant species within eight families as occasional hosts of OLB in eight recently invaded countries (Table 5). The family of Rosaceae was represented by 15 species, Betulaceae by three, Fagaceae, Ulmaceae, Sapindaceae and Malvaceae by two, the other two families (Cannabaceae and Cornaceae) by one each. Genera

Corylus and Rubus were infested in the highest number of countries, and regularly with highest infestation rates. New host records are underlined in Table 5. However, the infestation levels were much lower on a regular basis than those on oaks at the same locations. But still, host shifting may further facilitate the spread of OLB even where the landscape is strongly fragmented and the oak forests do not adjoin each other.

The recent explosive spread and outbreaks of OLB in several European countries show that the dispersal ability and the potential damage by the species can hardly be properly evaluated upon its arrival, as a non-native. Some species do not show immediate invasiveness, and start to spread

This article is protected by copyright. All rights reserved.

rapidly only after a latent period of different lengths [START_REF] Crooks | Lag times and exotic species: The ecology and management of biological invasions in slow-motion[END_REF]Jaric et al., 2018). The favourable weather conditions (likely mild winters allowing high overwintering survival) in several consecutive years may play a "triggering" role in the acceleration of the expansion and fast increase in abundance as it is assumed in the case of OLB.

Due to large-scale and potentially severe effects of OLB in the Eurasian oak forests, preferably international studies are further necessary. [START_REF] Osborn | Notes on American Tingidae with descriptions of new species[END_REF]; [START_REF] Connell | Life history and control of the oak lace bug[END_REF]; [START_REF] Drake | Lacebugs of the world: A catalog (Hemiptera: Tingidae)[END_REF]; [START_REF] Connor | Plant water deficits and insect responses: the preference of Corythucha arcuata (Heteroptera: Tingidae) for the foliage of white oak, Quercus alba[END_REF]; Torres [START_REF] Torres-Miller | Additions to the West Virginia tingid fauna (Hemiptera: Heteroptera: Tingidae)[END_REF]; Drew & Arnold [1997]; [START_REF] Trieff | Composition of the Coleoptera and Associated Insects Collected by Canopy Fogging of Northern Red Oak (Quercus rubra L.) Trees in the Great Smoky Mountains National Park and The University of Tennessee Arboretum[END_REF]; [START_REF] Kay | Fire effects on insect herbivores in an oak savanna: the role of light and nutrients[END_REF]; [START_REF] Barber | Light Environment and Leaf Characteristics Affect Distribution of Corythucha arcuata (Hemiptera: Tingidae)[END_REF]). Common names of the oaks follow [START_REF] Miller | Oaks of North America[END_REF]. Native ranges are taken from http://oaks.of.the.world.free.fr.

Name

  Figure 1.). Recognizing its potential importance, OLB was put on the EPPO Alert List in March 2001 and it remained until 2007, when it became clear that administrative efforts could not stop its further spread. Between April and July 2002, two specimens of OLB were caught in a

  was detected first are shown in Figure 1. The northernmost known record (N48.510889; E22.051056) in September 2019 is from eastern Slovakia (Zubrik's unpublished data). Population genetic studies may clarify the starting point and routes of the invasion (Estoup & Guillemaud 2010; Cristescu 2015).

  [START_REF] Mitchell | Collapsing foundations: The ecology of the British oak, implications of its decline and mitigation options[END_REF] reported 2,300 species associated with Q. petraea/robur in the UK, of which 326 were found to be obligate associates (only found on these two oak species). It has already been found in Hungary that larvae of oak specialist notodontids (Harpya milahuseri and Drymonia querna) starve and then die on leaves severely infested by OLB (authors' unpublished observations).

  e = eastern, ne = north-eastern, c = central, s = southern, se = south-eastern

Common name Native Range* Section Quercus -white oaks

	Q. alba L. 1753	white oak	e North America
	Q. bicolor Willd 1801	swamp white oak	ne USA; s Canada
	Q. macrocarpa Michx. 1801	bur oak	e North America
	Q. montana Willd. 1805	chestnut oak	s and e USA
	Q. muehlenbergii Engelm. 1887	chinkapin oak	e and cl USA; Canada; ne Mexico
	Q. prinoides Willd. 1801	dwarf chinkapin oak e USA
	Q. stellata Wangenh. 1787	post oak	c and se USA

Table 1 :

 1 North American host records of OLB based on literature sources:[START_REF] Morrill | Notes on the immature stages of some tingitids of the genus Corythucha[END_REF];Osborn &

This article is protected by copyright. All rights reserved.

-----------0 -

Acknowledgement

The work of the Hungarian participants was supported by the COST Action FP1401 -"Global Warning" and the OTKA 128008 research project sponsored by the National Research, Development and Innovation Office. Research in Croatia was by the two projects funded by Croatian forests LLC. The Ministry of Education, Science and Technological Development gave support to the work in Serbia, Grant number III43002. In Slovenia, the research was conducted through the project V4-1439 Development of new methods of detection, diagnostics and prognosis for non-native organisms harmful to forest 2014-2017 and programme groups P4-0059 Forest, forestry and renewable forest resources and P4-0107 Forest biology, ecology and technology. Special thanks for the Bulgarian data provided by Georgi Georgiev, Plamen Mirchev, Margarita Georgieva (Forest Research Institute), Snezhana Grozeva (Institute of Biodiversity and Ecosystem Research) and Nikolay Simov (National Museum of Natural History). The authors thank Dominique Fournier from Services Linguistiques DF (Canada) for linguistic and editorial improvements.

s and e Bulgaria, Asia

Minor, Caucasus

Europe, sw Asia, n Africa 3 3 3 -3 3 3 3 3 3 3 3 3 + 3 Minor


Marius Bozga
email: marius.bozga@imag.fr

Jean-Claude Fernandez
email: jean-claude.fernandez@imag.fr

Lucian Ghirvu

Susanne Graf

Jean-Pierre Krimm

Laurent Mounier

IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems

Keywords: asynchrony, timed systems, model-checking, static analysis, test generation

Formal Description Techniques (fdt), such as lotos or sdl are at the base of a technology for the speci cation and the validation of telecommunication systems. Due to the availability of commercial tools, these formalisms are now being widely used in the industrial community. Alternatively, a number of quite e cient veri cation tools have been developed by the research community. But, most of these tools are based on simple adhoc formalisms and the gap between them and real fdt restricts their use at industrial scale.

This context motivated the development of an intermediate representation called

if which is presented in the paper. if has a simple syntactic structure, but allows to express in a convenient way most useful concepts needed for the speci cation of timed asynchronous systems. The bene ts of using if are multiples. First, it is general enough to handle signi cant subsets of most fdt, and in particular a translation from sdl to if is already implemented. Being built upon a mathematically sound model (extended timed automata) it allows to properly evaluate di erent semantics for fdt, in particular with respect to time considerations. Finally, if can serve as a basis for interconnecting various tools into an uni ed validation framework. Several levels of if program representation are already available via well de ned api and allow to connect tools ranging from static analyzers to model-checkers.

Introduction

Formal Description Techniques, such as lotos ISO88] or sdl IT94c] and related formalisms such as msc and ttcn are at the base of a technology for the speci cation and the validation of telecommunication systems. Due to the availability of commercial tools, mainly for editing, code generation and testing, and the fact that these formalisms are promoted by itu and other international standardization bodies, these formalisms are now being widely used in the community of telecommunication systems. ? Work partially supported by R egion Rhône-Alpes, France ? ? ? Verimag is Research Laboratory of CNRS, Universit e Joseph Fourier and Institut National Polytechnique of Grenoble There are also increasing needs for description and validation tools covering as many aspects of system development as possible. This is the reason why the commercial editing tools contain also some veri cation facilities. Unfortunately, these veri cation facilities are often quite restricted and the tools are \closed" in the sense that there are only limited possibilities to interface them with others. On the other hand, a number of quite e cient veri cation tools have been developed by the research community, but they are in general based on adhoc input formalisms and the gap between them and real fdt restricts their use at an industrial scale. Even if these tools are in general less closed than commercial ones, they have rarely well-de ned interfaces. For example, a lot of developments were made around the Spin veri cation tool Hol91], but they are based on the availability of the source code and not on a priori de ned interfaces.

A di erent approach was followed within cadp FGK + 96], a toolbox for the verication of lotos speci cations. It was conceived right from the beginning as an open platform for interfacing di erent algorithms and provides several well-de ned and documented interfaces. The initial motivation for the work presented here was the fact that sdl becomes a more and more popular formalism in the telecommunication community, and that we wanted to adapt cadp to deal also with sdl speci cations. Since the intermediate program level formalisms used within cadp are not appropriated for sdl speci cations, we had to investigate alternative representations. For example cadp is based on a synchronous communication model (rendez-vous), whereas sdl communications are fully asynchronous (via queues).

Another motivation concerns time modeling. Finding a \reasonable" notion of time is a central problem which admits many possible solutions depending on choices of semantic models. This is certainly a non trivial question and this is re ected by the variety of the existing proposals for existing fdt. For instance, sdl syntax de nes a timer concept, but there is no consensus on its semantics for the moment and di erent sdl tools have adopted di erent choices. Similarly, in the original lotos de nition there was no particular notion of time, whereas di erent timed extensions are currently being proposed [START_REF] Lann | Distributed Systems { Towards a Formal Approach[END_REF]Que98]. Choosing an appropriate timed extension for an fdt should take into account not only technical considerations about the semantics of timed systems but also more pragmatic ones related to the appropriateness for use in a system engineering context. We believe that the di erent ideas about extensions of the language must be validated experimentally before being adopted to avoid phenomena of rejection by the users.

These problems motivated the development of if, a new intermediate representation for timed asynchronous systems. The requirements on this formalism were the following: it must be su ciently expressive to be used as an intermediate representation for the above mentioned speci cation formalisms, or at least for reasonably large subsets of them. it must have a formally de ned operational semantics, but exible enough to experiment di erent choices and extensions. it must be supported by a set of well de ned api, at di erent levels of program representation, allowing either to interface existing validation tools or to experiment new ones.

The paper is organized as follows. First, we de ne the if formalism, its main concepts and its operational semantics. We also discuss its expressiveness with respect to other models and speci cation formalisms, in particular regarding the timing aspects. Then, we present a set of tools interconnected within an open validation environment for if speci cations. We further detail two speci c components, based on static analysis and compositional generation, working at the program level and experimented within this environment. Finally, we illustrate the use of if on a small example, a distributed leader election algorithm on which di erent kinds of validation are performed.

Presentation of IF

In the following sections, we give a brief overview of the main features of if, its operational semantics in terms of labeled transition systems. A more complete description of if and of its semantics can be found in BFG + 98].

Syntax

An if system is a set of processes communicating either asynchronously through a set of bu ers or synchronously through a set of gates. The timed behavior of a system can be controlled through clocks (like in timed automata ACD93,HNSY94]).

IF system de nition: A system is a tuple Sys = (glob-def, procs, S) where glob-def = (type-def, sig-def, gate-def, var-def, buf-def) is a list of global de nitions, where type-def is a list of type de nitions (enumerated types, arrays, records and also abstract data types1 ) sig-def de nes a list of parameterized signals (as in sdl), gate-def de nes a list of parameterized gates (as in lotos), var-def is a list of global variables, and nally, buf-def is a list of bu ers through which the processes communicate by asynchronous signal exchange (as in Promela Hol91]). Notice that we allow various types of bu ers: fifo queues, stacks or bags, which can chosen to be unbounded or bounded and reliable or lossy. procs de nes a set of processes described in section 2.1. S is a synchronization expression, as in lotos or csp, telling how the processes de ned in procs synchronize. Such a synchronization expression is given by the following grammar where C is a (possible empty) set of gates: S ::= P2procs j S j C]j S Thus, a system S is either a process P or a parallel composition of two subsystems S 1 and S 2 with rendez-vous synchronization on the set of gates C. In a system of the form S 1 j C]j S 2 transitions concerning a gate in C are executed synchronously in the two subsystems whereas all other transitions are interleaved.

IF process de nition: Processes are de ned by a set of local variables, a set of control states and a set of control transitions. A process P2procs is a tuple P= (var-def, Q, cTrans), where: var-def is a set of local variable de nitions including also clocks 2 (as in timed automata)

Q is a set of control states on which the following attributes are de ned: { stable(q) and init(q) are boolean attributes, where the attribute stable can be used to control the level of atomicity: only stable states are visible on the semantic level.

{ the tpc(q) time progress condition attribute is a predicate depending on visible variable of the process (global variables and local ones) which de nes when time can progress. Notice that, anyway, time cannot progress in non stable states.

{ the attributes save(q), discard(q) are sets of filters of the form signal-list in buf if cond.

which lter the bu ers contents in this state. For example, discard(q) is used to eliminate silently unexpected signals: when consuming the next signal in the fifo queue buf, all signals of signal-list preceding it are discarded in the same atomic step, if the boolean expression cond evaluates to true. These primitives are useful in practice and taken from sdl.

cTrans is a set of control transitions, between control states q,q'2Q, which may be of the following types:

{ input transitions which are triggered by some signal read from one of the communication bu ers (as in sdl): q g 7 ! input ; body ???????????????! (urg) q 0

{ synchronization transitions which are executed simultaneously with compatible ones in other processes of the system (as in lotos): q g 7 ! sync ????????! (urg) q 0 { internal transitions depending not on communications: q g 7 ! body ????????! (urg) q 0

Where in all three cases: g is a boolean guard of the transition which may depend on visible variables in the process (including clocks) and prede ned tests on bu ers content (e.g., emptiness).

2 one can also de ne timers (as in sdl) which can be set to any positive value, which decrease with progress of time and expire if they reach the value zero; however to simplify the description we don't mention them in this document urg2feager, delayable, lazyg de nes the urgency type of the transition. eager transitions have absolute priority over progress of time, delayable transitions may let time progress, but only as long as they remain enabled, whereas lazy transitions cannot prevent progress of time. These urgency types have been introduced in BST98], which shows that the use of urgency predicates on transitions (instead of time progress conditions) facilitates the compositional speci cation of timed systems.

input is an input of the form \input sig(reference list) from buf if cond" where { sig is a signal, { reference list the list of variables3 (excluding clocks) in which the received parameters are stored, { buf is the name of the bu er from which the signal should be read { cond is a \post guard" de ning the condition under which the received signal is accepted and it usually depends on received parameters. Intuitively, an input transition is enabled if its guard is true, the rst signal to be consumed (according to the attributes save(q) and discard(q)) is of the form { cond is again a post guard usually depending on received values and which restricts the values that the process is willing to accept. The concept of synchronization is taken from lotos: the simultaneous execution of synchronization transitions concerning the same gate allows a instantaneous exchange of values between several processes. Notice that clock expressions cannot appear as communication o ers. body is a sequence of atomic actions of the following types: { asynchronous outputs of the form \output sig(par list) to buf" append a signal of the form \sig(par list)" to the bu er buf.

{ usual assignments between discrete variables. { resettings of clocks, which have the e ect to assign the value zero to the corresponding clock.

Semantics

The semantics of if is based on concepts taken respectively from lotos, sdl and timed automata. We de ne it by translating if sytems into Timed Automata with Urgency BST98]. First, we show how to associate a timed automaton with a process, and then, how these timed automata can be composed into a single one 4 . The timed automata can then be interpreted either using discrete or dense time depending on the veri cation tools and properties considered. Notice that the discrete/dense interpretation of time does not in uence the translation into a timed automaton.

Association of a Timed Automaton with a process: Let P= (var-def, Q, cTrans) be a process de nition in the system Sys and furthermore: Let buf be a set of bu er environments B, representing possible contents of the bu ers of the system, on which | depending on the declared bu er type | all necessary primitives are de ned: e.g. \get the rst signal of a given bu er, taking into account the save and the discard attributes of the control state", \append a signal at the end of a bu er",... Let env be a set of environments E de ning the set of valuations of all discrete variables de ned in the system Sys (the local and the global ones)

The semantics of the process P is the timed automaton P] = (Q env buf,Trans) where Q env buf is the set of states, for which we extend the attributes of control states in a natural manner, e.g. tpc((q,(E,B))) is the partial evaluation of tpc(q) in ((E,B)). Notice that the set of data environments env can be split into env loc env glob where env loc concerns only local variables of the process and env glob concerns the global variables of the system. Trans is the set of transitions of the timed automaton obtained from control transitions by the following two rules:

1. For any input transition (and for internal ones) q g 7 ! (sig(x 1 :::x n ); buf; cond) ; body ??????????????????????????????! (urg) q 0 2cTrans and for any (E,B),(E',B')2val, there exists a transition (q; (E; B)) `: g 0 7 ! body 0 ????????????! (urg) (q'; (E 0 ; B 0 )) 2Trans if { g' is the the partial evaluation of g in (E,B), which is an expression depending only on clocks.

{ let B 00 be the bu er environment obtained after consuming sig(v 1 :::v n ) in bu er buf (and after elimination of appropriate signals of the discard(q) attribute and saving of the signals of the save(q) attribute)

{ let E 00 =E v 1 :::v n /x 1 :::x n ] is obtained by assigning v i to x i , { the post guard cond evaluates to true in the environment (E 00 ; B 00 ) { (E 0 ; B 0 ) is obtained from (E 00 ; B 00 ) by executing all the assignments of the body, and by appending all signals required by outputs in the body.

{ body' is the sequence of resettings of clocks which remain as such in the timed automaton, 4 Notice that the semantics is compositional in the sense that, in order to associate a timed automaton with a system one can also rst compose the system into a unique process and then associate a timed automaton with this process { `is an appropriate label used for tracing.

2. For each synchronization transition of the form q g 7 ! c : !exp 1 ?y 2 ::: : cond ????????????????????????! (urg) q 0 2cTrans and for any (E,B),(E',B')2val, there exists a transition (q; (E; B)) `: g 0 7 ! skip ???????????! (urg) (q'; (E 0 ; B 0 )) 2Trans if { g' is the the partial evaluation of g in (E,B), { the expression exp i evaluates to the value v i in (E,B), { E 0 =E v 2 :::v j :::=y 2 :::y j :::] for some v j belonging to the domain of y j , { the post guard cond evaluates to true in the environment E', { the label `is equal to c !v 1 !v 2 ...

Composition of models:

The timed automaton associated with a system of the form Sys = (glob-def,procs,S) is obtained by composing the timed automata of processes according to the composition expression S. The composition rules correspond to the and-parallel composition described in BST98].

Let P i ] = (Q i val,Trans i ) i=1
;2 be the timed automata associated with processes or subsystems of Sys | where val concerns only all global variables and is of the form env glob buf and the valuations of local variables are integrated into the set of control states | and C a set of gates.

Then, P 1 j C]jP 2 ] = P 1 ] j C]j P 2 ] = (Q val,Trans) where Q= Q 1 Q 2 where init((q 1 ,q 2 )) = init(q 1 ) ^init(q 2 ) stable((q 1 ,q 2 )) = stable(q 1 ) ^stable(q 2 ) tpc((q 1 ,q 2 )) = tpc(q 1 ) ^tpc(q 2 ) Trans is the smallest set of transitions obtained by the following two rules: the rst one applies to all transitions of Trans 1 which are not synchronizations on gates in C and there is also a symmetrical rule for transitions of Trans 2 .

(q 1 ; V) `: g 7 ! act ??????????! (urg) (q 0 1 ; V 0 ) 2 Trans 1 and :stable(q 1 ) _ stable(q 2 ) ((q 1 ; q 2 ); V) `: g 7 ! body ???????????! (urg) ((q 0 1 ; q 2 ); V 0 ) 2 Trans

The requirement on stableness implies that there is no interleaving in non stable states; they are transient states, such that a nite sequence of transitions between to stable states can be considered as one atomic transition.

The second rule concerns the synchronizations on gates in c2C (q 1 ; V) `: g1 7 ! skip ???????????! (u1) (q 0

In this rule, the synchronization of two transitions with the same urgency attribute result in a transition with the same attribute, the composition of an eager transition with any other transition results in an eager one, an in order to compose a lazy with a delayable transition, one needs to decompose the delayable one into two transitions, an eager and a lazy one, which under a reasonable restriction is

always possible BST98].
The semantics of Timed Automata The semantics of A is de ned by the labeled transition system (Q time; !) where the transition relation ! consists of two types of transitions, discrete ones and time progress transitions:

For any transition q 1 `: g 7 ! body ???????????! (urg) q 2 of Trans and T 2time, there exists a discrete transition of the form (q 1 ; T ) ? ! (q 2 ; T 0 ) if { the guard g evaluates to true in T , { and T ' is obtained from T by executing all assignments to clocks (resettings) of body. in any state (q,T ), time can progress by the amount , that is (q; T ) time:

?????! (q; T ) if time can progress in the state (q,T ) and continuously until T 0 : whenever time has progressed by an amount 0 where 0 0 < , time can still progress in the reached state (q,T 0 ).

Time can progress in a state (q,T ) if and only if the following conditions hold:

{ stable(q), that means time can progress only in stable, never in transient states { the time progress attribute tpc(q) evaluates to true in T { no eager transition is enabled in (q,T ) { for each delayable transition tr enabled in (q,T ), there exists a positive amount of time , such that tr remains enabled when time progresses by . That means enabled delayable transitions allow time to progress, but only as long as they remain enabled.

IF and other formalisms

if is a formalism for the description of asynchronous systems at a programming language level. However, it has not been designed with the aim to replace speci cation languages such as lotos, sdl and Promela. if has been designed as an intermediate representation for sdl but it can also be used for other speci cation formalisms. Thus, the expressiveness of if and its adaptedness as an intermediate representation from sdl, lotos and Promela are discussed below.

SDL

The de nition of sdl (Speci cation and Description Language) started in 1974 and it has been standardized by CCITT in 1988 IT94c]. sdl is based on extended nite state machines communicating asynchronously via queues. There exists a formal semantics of the language de ned in IT94a,IT94b], various authors have criticized it and proposed alternative ones Bro91,BMU98,God91] to name only a few of them. Currently, sdl is widely accepted by the industrial community. This is due mainly to the fact that sdl development is supported by methodologies OFMP + 94] and tools Ver96,AB93] in all phases from requirement analysis, design and validation to implementation. However, the validation capabilities of the industrial tools are rather limited with respect to the ones existing in the academic community.

There is no standard semantics of time de ned for sdl. For example, Objectgeode uses a very \synchronous" time concept in which time can only progress when the system is blocked (that means all transitions are eager), whereas others consider that time can always progress (that means that all transitions are lazy). This shows that the currently used notions of time in sdl are extreme ones | which is often considered as problem by the users | and many intermediate solutions are possible using if as discussed in previous section.

We have identi ed a static subset of sdl which we are able to translate into if. That is, with the exception of dynamic creation of processes and some mobility aspects of communication, we can de ne a syntactic level translation between these two formalisms. A prototype translator has been implemented using the sdl/API Interface provided by ObjectGeode Ver96]. More detailed information about it can be found in BFG + 99].

3.2 LOTOS lotos (Language Of Temporal Ordering Speci cations) BB88] has been developed and standardized by ISO in 1989. It is a process-algebra based on ccs Mil80] and csp Hoa84]. In lotos, the communication is synchronous using rendez-vous. lotos has a well-de ned operational semantics and there exist tools supporting it.

The right approach to model and validate lotos speci cations is recognized to be the use of Petri nets, rather than communicating extended automata GS90] as intermediate representation. However, our experience with lotos has shown that often the speci cations have the form of a parallel composition of sequential components (processes). This observation motivated also the use of compositional generation methods, which gives good results for this kind of lotos speci cations KM97].

The timed extensions introduced in E-Lotos Que98], ET-Lotos LL97] and Lotos-NT Sig99] are similar to that of if, only that the urgency of an action is de ned implicitly by its type: \exceptions" and internal actions are urgent, whereas observable actions are not. This is due to the fact, that they want to achieve a much stronger form of compositionality, where with each process can be associated a directly labeled transition system (and not a timed automaton) which then can be composed into a system model.

We plan to investigate the translation of decomposable lotos speci cations into if, as parallel composition with synchronization between processes can be handled in if. Furthermore, a reasonably small Petri Net (corresponding to a non-decomposable lotos part) can be modeled by an if process.

PROMELA

Another language we have considered is Promela, the native language of the Spin model-checker Hol91]. It was designed as an intermediate representation language for protocols, mainly for validation purposes. It is based on extended nite-state machines communicating asynchronously or synchronously via queues.

Promela has not really been designed as a speci cation language but it has a relatively important visibility as well in the academic community as in the industrial one. Its success is due to the high availability of Spin, which provides powerful modelchecking algorithms based on partial-order reductions.

There exist timed extensions of Promela. The one proposed in CT96] is based on Timed Automata, whereas BD98] is very similar to the notion of time used in Objectgeode: all set timers decrease synchronously until one of them expires; then time is blocked until the corresponding timeouts are consumed, where these timeout consumptions take place when no other transition is possible in the system.

A translator from if to Promela is currently developed in the framework of the vires Esprit-ltr project at Eindhoven University. We plan to study also a backward translation from Promela to if. However, as for sdl, there are some limitations due to dynamic process creation feature of Promela.

A validation environment based on IF

One of the main motivation for developing the if intermediate representation is to provide an \open" validation environment, able to make heterogeneous tools cooperate within a single framework. Especially for sdl, solid industrial tools for editing and code generation have been built which are used by a large community of users. On the other hand, there exist many veri cation tools built upon diverse formalisms | such as the Spin tool Hol91] based on Promela, the cadp tool FGK + 96] based on lotos, the smv tool Mac93] based on extended automata, tools for the veri cation of Timed systems such as kronos Yov97] and Uppaal LPY97] based on di erent representations of Timed Automata, to name only a few of them.

Therefore, an integrated validation environment should ful ll the following requirements:

First of all, it is able to support several validation techniques, from symbolic interactive simulation to automatic property checking, together with test case generation and executable code generation. Indeed, all these functionalities cannot be embodied in a single tool and only tool integration facilities can provide all of them. Moreover, for a sake of e ciency, this environment also has to support several level of program representations. For instance it is well-known that model-checking veri cation of real life case studies usually needs to combine several optimization techniques to overcome the state explosion problem. In particular, some of these techniques rely on a program level representation, like static analysis and computations of abstractions (for which it may be necessary to cooperate with decision procedures or theorem-prover). Other techniques operate on a representation of the underlying model, such as on-the-y analysis, bisimulation based model reduction or model-checking. These representations can be either implicit, enumerative or symbolic and are explained below. Another important feature is to keep this environment open and evolutive. Therefore, tool connections are performed only by means of le sharing or program representation access. For this purpose several well-de ned interfaces are o ered.

In the remainder of the section we present the overall architecture of the existing environment and some of its related components. Then, we describe in a more detailed manner two speci c modules concerning static analysis (section 4.2) and compositional generation (section 4.3).

Overall architecture

The if validation environment is built upon two levels of program representation, each of them being accessed through well-de ned Api.

The syntactic level allows to consult and modify the abstract tree on an if program. Since all the variables, timers, bu ers and the communication structure are still explicit, high-level transformations based on static analysis (such as live variable computation, see below) or abstraction computations can be applied. Moreover, this Api is also well suited to implement translators from if to other speci cation formalisms (like Promela or invest).

The execution model level gives access to the underlying lts of the if program. In practice three distinct Api are o ered, depending on the representation used. [START_REF] Fernandez | Symbolic Equivalence Checking[END_REF] philosophy. It consists in a set of C functions and data structures allowing to compute on demand the successors of a given state. This piece of C code is generated by the if compiler, and it can be linked with a \generic" exploration program performing on the y analysis (deadlock detection, model-checking, test-case generation, ...).

The implicit enumerative representation is based on the open-caesar

In the symbolic representation (called smi Boz97]) set of states and transitions of the lts are expressed by their characteristic functions over a set of nite variables. These functions are implemented in terms of decision diagrams(bdds Bry86] andmdds). Existing applications based on this Api are symbolic model-checking and minimal model generation.

Finally, the explicit enumerative representation simply consists in an lts le format with the associated access library. Although this explicit representation is not suitable for handling a large system globally, it is still useful in practice to minimize some of its abstractions with respect to bisimulation based relations (like in compositional generation, see below). Figure 4.1 describes the existing connections in this environment (plain arrows) and the planned ones (dashed arrows). Most of the tools mentioned are presented below: cadp FGK + 96,BFKM97] is a tool set for the veri cation of lotos speci cations. It has been developed and by Verimag and the Vasy team of Inria Rhône-Alpes. We brie y present here two veri ers integrated in this tool set which have already been connected to the new if environment: { aldebaran compares and minimizes nite ltss with respect to various simulation or bisimulation relations. This allows the comparison of the observable behavior of a speci cation with its expected one, described at a more abstract level.

{ evaluator is a \on-the-y" model-checker for formulas of the alternating-free -calculus Koz83]. As for the if environment, an important feature of cadp is to o er several lts representations and in particular the open-caesar Api which is fully compatible with the if implicit enumerative representation. purposes characterize some abstract properties that the system should have and one wants to test, given trees of labels, decorated with verdicts \ok" and \fail". mmg FKM93] is a minimization tool based on a partition re nement algorithm combined with a reachable state space computation BFH90]. This tools works on the symbolic smi interface. Objectgeode is a tool set developed by Verilog supporting sdl, msc and omt. It includes graphical editors and compilers for each of these formalisms. It also provides a C code generator and a simulator to help the user to interactively debug an sdl speci cation.

Objectgeode also provides an Api o ering a set of functions and data structures to access the abstract tree generated from an sdl speci cation. A translation tool (sdl2if) uses this abstract tree to generate an operationally equivalent if specication. Kronos Yov97] is a Tctl model-checker for communicating timed automata. The current connection with the if environment is as follows: control states and discrete variables are expressed using the if implicit enumerative representation whereas clocks are expressed using an appropriate symbolic representation (particular polyhedra).

invest BLO98] is a tool computing abstractions and invariants on a set of guarded command processes communicating through shared variables. We are actually implementing the translation between this formalism and if, which will allow to compute abstract systems.

Static analysis and abstraction

Considering the expressiveness of if, static analysis and abstraction techniques can be applied in order to improve the veri cation and the test generation process. The expected bene ts of such techniques are mainly the reduction of the state space and the reduction of the complexity of the if program.

We have already experimented very simple analysis, used classically in the context of data-ow analysis which can be divided into two classes: property independent analysis: without regarding any particular property or test purpose (such as live variable analysis or constant propagation), property dependent analysis: takes into account some information of the property and propagate them over the static control structure of the program (such as irrelevant variables abstraction) We brie y describe two techniques currently implemented for if.

\Live variables" analysis: A variable is live in a control state if there is a path from this state along which its value can be used before it is rede ned. An important reduction of the state space of the model can be obtained by taking into account in each state only the values of the live variables.

The reduction considered is based on the relation live de ned on the state space of the model: two states are related if and only if all live variables have the same value. It can easily be proved that live is a bisimulation on the model. This result can be exploited in several ways. Due to the local nature of live it is possible to directly generate the quotient model w.r.t. live instead of the whole model without any extra computation. Exactly the same reduction is obtained by \resetting"(that is assigning some prede ned value) in the initial program systematically all non-live variables. The second approach is implemented for if. \Irrelevant variables" abstraction: Given a subset X of irrelevant variables (which in general depend on the considered property), an upper approximation for this program can be computed syntactically and iteratively as follows: the assignments of variables belonging to X are removed the expressions containing variables from X are replaced by a special any value (denoting any element of its domain) the guards which evaluate to any are removed (i.e., replaced by the true value) Clearly the resulting program contains all executions of the initial one and does not depend anymore on variables in X. Any safety property valid on the resulting abstract program is also valid on the initial one, but the converse does not necessarily hold.

In practice, the set of irrelevant variables can be chosen in di erent manners. Either, the user can directly supply it based on his knowledge about the speci cation and the given veri cation context. Another possibility is to derive this set automatically from the considered property (or the test purpose). Finally, irrelevant variables can also be taken among the variables provided by the environment and the ones depending on them: such variables are uncontrolled since their values are nondeterministically chosen by the environment. This latter choice has been considered in CGJ98].

We are also investigating more general abstraction techniques. For instance, through the connection with invest we will be able to compute abstract if programs using more general and powerful abstraction techniques.

Compositional generation

As shown in the previous section, e cient reductions are obtained by replacing a model M by its quotient w.r.t an equivalence relation like live . Much weaker equivalences (that is smaller quotients) can be obtained by taking into account the properties under veri cation. In particular, it is interesting to consider a weaker equivalence R | which should be a congruence for parallel composition |, able to abstract away non observable actions. The main di culty is to obtain (an approximation of) the quotient M=R without generating M as a whole.

A possible approach is based on the \divide and conquer" paradigm: splitting the program description into several pieces (i.e., processes or process sets), generate the model M i associated with each of them, and then compose the quotients M i =R. The hope is that the generated intermediate models can be kept small. This compositional generation method has already been applied for speci cation formalisms based on rendez-vous communication between processes, and has been shown e cient in practice GLS96,Val96,KM97]. To our knowledge it has not been investigated for systems based on communication via bu ers, may be, because bu ers raise several di culties or due to the lack of suitable representations and tools.

The potential bene t of this compositional approach will be illustrated on an example in the next section.

An illustrating example

We present a simple example to illustrate the if formalism and related veri cation tools. We consider a token ring, that is a system of n stations (processes) S 1 , : : : S n , connected in a circular network, in which a station is allowed to access some shared resource R only when it \owns" a particular message, the token. If the network is unreliable it is necessary to recover from token loss. This can be done using a leader election algorithm Lan77,CR79] to designate a station responsible for generating a new token.

Table 1 shows the global de nitions of the if speci cation corresponding to the particular protocol considered [START_REF] Graf | Compositional Minimisation of Finite State Systems using Interface Speci cations[END_REF]. The signals open and close denote the access and the release of the shared resource (here a part of the environment). The signals token and claim are the messages circulating on the ring.

All stations S i are identical up to their identity and described by an if process as the one of Figure 2. The timer worried is set when the station waits for the token and reset when it receives it. On expiration of the timer worried token loss is assumed and an election phaes is started. The \alternating bit" round is used to distinguish between valid claims (emitted during the current election phase) and old ones ( The most spectacular reduction is obtained by the live reduction: the reduced model is about 100 times smaller than the one obtained by simultaneous generation, while preserving all properties (models 1 and 2 are strongly bisimilar). This is explained by the fact that only a few variables are live in each state: in the idle state the live variables are round and worried, in the critical state only round is live, while variables adr and rnd are never live.

More reduction is achieved by the following compositional generation strategy:

1. We split the if description into two parts, the rst one contains processes S 1 and S 2 and the second one processes S 3 and S 4 . For each one of these descriptions, the internal bu er between the two processes is a priori bounded to two places. Note that, when a bounded bu er over ows during simulation, a special over ow transition occurs in the corresponding execution sequence. 2. The lts associated with each of these two descriptions are generated considering the \most general" environment providing any potential input. As claim and token can be transmitted at any time, over ow transitions appear in the corresponding ltss.

3. In each lts the input and output transitions relative to the internal bu ers (Q 2 and Q 4 ) are hidden (i.e., renamed to the special action); then they are reduced w.r.t an equivalence relation preserving the properties under veri cation. For the sake of e ciency we have chosen the branching bisimulation vGW89] preserving all the safety properties (e.g. mutual exclusion). 4. Each reduced lts is translated back into an if process (without variables), and the resulting processes are combined into a single if description, including the two remaining bu ers (Q 1 and Q 3 ). It turns out that the lts generated from this new description contains no over ow transitions (they have been cut o during the second composition, which con rms the hypothesis on the maximal size of the internal bu ers). The nal lts is branching bisimilar to the one obtained from the initial if description.

Veri cation: We are interested in checking that the shared resource is accessed in mutual exclusion. For this, we consider as visible only the open and close actions.

Mutual exclusion property can be rephrased as follows: every open i (station i access the resource) can only be followed by close i (station i releases the resource) possibly after some internal moves . This property can be expressed in the -calculus (see below) and veri ed with evaluator, on any of the generated models. î =1

X: ( open i ] : Y: (hfclose i ; giT _ h iY ) ^ ]X) Another approach to verify mutual exclusion is to compare the model of the speci cation with an abstract one expressing the desired behavior. For instance, all three models are branching bisimilar to the one shown in Figure 3. The reductions and comparisons are carried out using aldebaran. Test Generation: We illustrate the use of the tgv to extract test cases for the token ring protocol. We want to test the property stating that a station lters a received claim with a smaller address than its own and transmits it unchanged otherwise. We chose a test purpose expressing that after S 4 has sent its claim, it will be transmitted unchanged by station S 1 , then by S 2 and nally by S 3 . The generated test case is shown in gure 4.

Conclusion and perspectives

We have presented the formalism if which has been designed as an intermediate representation for sdl, but it can be used as a target language for other fdt as it contains most of the concepts used in these formalisms. The use of if o ers several advantages:

if has a formal semantics based on the framework of communicating timed automata. It has powerful concepts interesting for speci cation purposes, such as di erent urgency types of transitions, synchronous communication, asynchronous communication through various bu er types (bounded, unbounded, lossy, : : : ).

Fig. 4. ttcn test case

if programs can be accessed at di erent levels through a set of well de ned apis. These include not only several low-level model representations (symbolic, enumerative, ...) but also higher level program representation, where data and communication structures are still explicit. Using these api several tools have been already

interconnected within an open environment able to cover a wide spectrum of validation methods.

The if package is available at http://www-verimag.imag.fr/DIST SYS/IF. In particular, a translation tool from sdl to if has been implemented and allows both to experiment di erent semantics of time for sdl and to analyze real-life sdl speci cations with cadp.

A concept which is not provided in if is dynamic creation of new process instances of processes and parameterization of processes; this is due to the fact that in the framework of algorithmic veri cation, we consider only static (or dynamic bounded) con gurations. However, it is foreseen in the future to handle some kinds of parameterized speci cations.

The results obtained using the currently implemented static analysis and abstractions methods are very encouraging. For each type of analysis, it was possible to build a module which takes an if speci cation as input and which generates an reduced one. This architecture allows to chain several modules to bene t from multiple reductions applied to the same initial speci cation. We envisage to experiment more sophisticated analysis, such as constraints propagation, and more general abstraction techniques. This will be achieved either by developing dedicated components or through the connections with tools like invest.

Fig. 1 .

 1 Fig. 1. An open validation environment for if

Fig. 3 .

 3 Fig. 3. The reduced behavior of the token ring.

  The model of time of if is that of Communicating Timed Automata with urgency introduced[START_REF] Bryant | Graph based algorithms for boolean function manipulation[END_REF]. Each process has a number of clocks which increase with progress of time (either in a discrete or continuous way). Clocks can be \tested" in the guards and \reset" in the bodies of the transitions. In this model, time is considered global, that is, it progresses synchronously in all processes of the system. The main problem is \when can time progress?". In timed automata ACD93], time progress is de ned by means of \invariants" associated with each state, such that time is allowed to progress as long the invariant expression evaluates to true. The problem with this model is that the composition of timed automata leads to time deadlocks. A time model avoiding this problem is obtained by associating with every transition a deadline (a predicate implying the guard), meaning that, whenever the deadline predicate evaluates to true, the transition has priority over progress of time.

[START_REF] Bryant | Graph based algorithms for boolean function manipulation[END_REF]

, it has been shown that a much simpler model using three possible urgency attributes instead of deadlines is su cient: eager transitions have always priority over time, delayable transitions may let time progress, but only as long as they remain enabled, and lazy transitions cannot prevent time from progressing. In if the time progress condition in each state is de ned depending on the urgency of enabled transitions and, in order to include the model of timed automata, one can associate an explicit tpc attribute with control states, with the potential risk of introducing time deadlocks by composition.

The semantics of Timed Automata with Urgency is de ned in BST98]. Let A = (Q; Trans) be a Timed Automaton. Let time be a set of environments for clocks, where T 2time de nes for every clock a value in a time domain T (positive integers or reals). Resetting a clock a ects T by changing the value of the reset clock to zero. Progress of time by an amount transforms the valuation T into the valuation T in which the values of all clocks are increased by .

Table 1 .

 1 if global de nitions token reception). In the idle state, a station may either receive the token from its neighbour (then it reaches the critical state and can access the resource) or receive the timer expiration signal (then it emits a claim stamped with its address and the current value of round) or receive a claim. A received claim is \ ltered" if its associated address is smaller than its own address and transmitted unchanged if it is greater. If its own valid claim is received, this station becomes elected and generates a new token. We summarize in Table2the size of the models obtained from the token-ring protocol using three generation methods: directly from the initial if program (global generation), using the live variable reduction (global + live) and using a compositional generation strategy (compositional + live).

	cancelled by a

Table 2 .

 2 Models obtained for the token ring example

where we suppose that the user provides also implementations of the introduced functions, otherwise expressions containing them are handled syntactically

or \assignable" expressions such as elements of records or arrays

; V 0 )

Trans 1 and (q 2 ; V) `: g 2 7 ! skip ???????????! (u2) (q 0 2 ; V 0 ) 2 Trans 2 ((q 1 ; q 2 ); V) `: g 1 ^g2 7 ! skip ???????????????! (urg) ((q 0 1 ; q 0 2 ); V 0 ) 2 Trans

 ------+-----------------------------------+---------+------------+--- ------+-----------------------------------+---------+------------+--- ---+-------+-----------------------------------+---------+------------+---+