PhD Karen Ritchie
email: karen.ritchie@inserm.fr

PhD Joanna Norton

MD Anthony Mann

PhD Isabelle Carrière

PhD Marie-Laure Ancelin

Late-onset agoraphobia: general population incidence and evidence

Keywords: agoraphobia, anxiety, depression, suicidal ideation, elderly, longitudinal study

teaching and research institutions in France or abroad, or from public or private research centers.

INTRODUCTION

Increasing interest is now being shown in phobias in the elderly as they have been associated with higher mortality, increased proinflammatory cytokines [START_REF] Covelli | Stress, neuropsychiatric disorders and immunological effects exerted by benzodiazepines[END_REF][START_REF] Luchins | Late-life onset of panic disorder with agoraphobia in three patients[END_REF] and stress reactivity [START_REF] Chaudieu | Abnormal reactions to environmental stress in elderly persons with anxiety disorders: Evidence from a population study of diurnal cortisol changes[END_REF] , lower heart rate variability, [START_REF] Kawachi | Decreased heart rate variability in men with phobic anxiety (data from the Normative Aging Study)[END_REF] fatal coronary artery disease, and sudden cardiac death [START_REF] Albert | Phobic anxiety and risk of coronary heart disease and sudden cardiac death among women[END_REF] . Recent studies of anxiety disorders in the elderly suggest that rates of all phobias may not only be much higher than previous epidemiological studies have suggested, but perhaps even constitute the most common form of anxiety disorder in this population [START_REF] Bryant | The prevalence of anxiety in older adults: methodological issues and a review of the literature[END_REF] . Agoraphobia is a specific form of phobia which has been differentiated from other phobias within the international classifications of psychiatric disorder, principally due to its assumed association with panic attacks. It is defined as a fear and avoidance of being in places or situations from which escape might be difficult in the event of sudden incapacitation. As a result of such fears, the agoraphobic person avoids travel or requires a companion when away from home. Moderate cases may cause some constriction in lifestyle, while severe cases of agoraphobia may result in the person being completely housebound or unable to leave home unaccompanied. Within DSM-IV [START_REF] American | Diagnostic and Statistical Manual of Mental Disorders[END_REF] agoraphobia is a sub-section of panic disorder.

Agoraphobia without a history of panic disorder may be classified as such, but is considered atypical.

Agoraphobia in the elderly has received little attention, being considered to be principally a disorder of young adulthood [START_REF] Luchins | Late-life onset of panic disorder with agoraphobia in three patients[END_REF] ; the Epidemiological Catchment Area study in the U.S. for example reported a one month prevalence of agoraphobia in persons over 65 of under 1.4% [START_REF] Regier | One-month prevalence of mental disorders in the United States. Based on five Epidemiologic Catchment Area sites[END_REF] . Clinical reports have suggested, however, that this form of phobia is commonly overlooked in the elderly; unwillingness to go outside the home being easily attributed to poor health and loss of social networks 9 . Undetected agoraphobia in the elderly is highly unlikely to improve spontaneously [START_REF]Wittchen H Natural course and spontaneous remissions of untreated anxiety disorders[END_REF] and given its association with anxiety and depressive symptoms, is likely to lead to a downward spiral of loneliness and deteriorating mental health. On the other hand, treatment of agoraphobia with cognitivebehavioural therapies and psychotropics has been proven to be highly successful at all ages 9,[START_REF] Hendriks | Predictors of outcome of pharmacological and psychological treatment of late-life panic disorder with agoraphobia[END_REF][START_REF] Hendriks | A randomized controlled study of paroxetine and cognitive-behavioural therapy for late-life panic disorder[END_REF] .

The aim of the present study is to provide estimates of the rates, clinical characteristics and risk factors for late-onset agoraphobia from a large prospective population study; previous studies being compromised by small samples, hierarchical case-finding procedures excluding cases with comorbidity, and failure to take into account potential confounding factors. The current study is part of a longitudinal project (the ESPRIT study) examining psychiatric disorder in the elderly using a standardized clinical interview based on international diagnostic algorithms for agoraphobia with clinical case validation. The study also has extensive information relating to clinical and life-style variables, permitting the identification of risk factors, and adjustment for multiple potential confounding factors.

METHOD

Sample

Community dwelling persons 65 years and over, were recruited by random selection from the fifteen electoral rolls of the Montpellier district between March 1999 and February 2001 as part of the ESPRIT study of late-life psychiatric disorder [START_REF] Ritchie | Prevalence of DSM-IV psychiatric disorder in the French elderly population[END_REF] . Of the persons contacted 72.7% accepted. Refusers were replaced by another subject drawn at random from the same electoral division such that each division is equally represented. Subjects refusing were slightly older and more likely to live alone than non-refusers. Participants were given a base-line examination and re-examined with a detailed psychiatric interview on two further occasions at intervals of two and four years. Seventy persons diagnosed with dementia at base-line were excluded from the present study. Dementia was diagnosed by a neurologist as part of a standardized examination (see below) and validated by a panel of independent neurologists. Of the 2189 dementia-free participants included in the ESPRIT study, 221 were excluded because of missing data on agoraphobia or on one of the main sociodemographic variables at baseline. The cross-sectional analyses were thus conducted on a maximum of 1968 persons. Participants did not differ from those excluded from the analysis for baseline sociodemographic and health variables. The longitudinal analysis was carried out on participants with either 2-year or 4-year follow-up examinations. Of the baseline sample, 98 participants (5%) were missing both follow-up examinations, (38 died, 26 were lost to follow-up and 34 refused to participate). Compared to the follow-up participants, those lost to follow-up were older (p=0.0004), with a lower educational level (p=0.02), with more frequent baseline respiratory problems (p<0.0001), cardio and cerebro-vascular pathologies (p=0.02), and disability (p<0.0001). There were no significant differences for baseline depressive symptomatology, anxiety or agoraphobia. Incident cases of dementia (n=48) were retained in the study as they were still community-dwelling and able to undertake the examinations. In cases of doubt family proxies and general practitioners were consulted. The study protocol was approved by the Ethics Committee of the University-Hospital of Kremlin-Bicêtre and written informed consent was obtained from each participant.

Measures

Participants were required to attend a half-day examination by a neurologist and a centre interviewer (nurse or psychologist) at the Gui de Chauliac Neurology Hospital (Montpellier, France).

Persons unable to come to the study centre (7% of participants) were examined in their homes. The following procedures were carried out:

A standardized health interview covering present and past health and medication use (subjects were asked to bring medications to the centre). The examination covered past and current vascular disease (angina pectoris, arrhythmia, lower limb arteritis, heart failure, myocardial infarction, cardiovascular surgery, stroke) and other chronic illnesses (cancer, osteoporosis, asthma, diabetes defi ed as fasti g glu ose≥ ol/l or treat e t, h per holesterole ia defi ed as total holesterol ≥ .

ol/l or treat e t, h perte sio defi ed as resti g lood pressure ≥ /9 Hg or treatment, and thyroid disorders).

Confinement (to bed, home or neighbourhood) for health reasons was noted and disability measured using the Rosow and Breslow mobility scale (ability to do heavy housework, walk over 500 metres and go up and down two flights of stairs) [START_REF] Rosow | A Guttman health scale for the aged[END_REF] and the Lawton Instrumental Activities of Daily Living scale [START_REF] Lawton | Scales to measure competence in everyday activities[END_REF] . Recent exposure to adverse life events in the past year was assessed at base-line using the Gospel Oak Questionnaire [START_REF] Harwood | The prevalence of diagnoses, impairments, disabilities and handicaps in a population of elderly people living in a defined geographical area: the Gospel Oak project[END_REF] .

A standardized clinical examination based on ICD-10 criteria 17 to detect neurological and cardiovascular disorder, including measures of sitting and standing blood pressure, was carried out at base-line and at each follow-up examination by a research neurologist. Childhood environment A retrospective self report questionnaire [START_REF] Ritchie | Association of adverse childhood environment and 5-HTTLPR Genotype with late-life depression[END_REF] examining traumatic experiences during childhood and adolescence and covering 25 adverse and 8 protective factors, was given to subjects for completion at the second follow-up.

Statistical Analysis

A sensitivity analysis was conducted to compare participants with those excluded using the Chi² test.

The Chi² test and Fisher exact test were used to compare crude rates for psychiatric co-morbidities at baseline and follow-up. The clinical characteristics of the sample of 1968 subjects is described according to presence or not of agoraphobia at baseline, giving p-values from a logistic regression analysis adjusted for age, sex and education. The incident rate over the follow-up was calculated on 1175 subjects with no baseline history of agoraphobia and data available at both follow-ups. For new cases the exact date of onset during the follow-up period was not available, onset was therefore considered to have occurred midway between the two examinations. Population incidence was estimated by dividing the number of new cases occurring during follow-up by the total number of agoraphobia-free years lived by the cohort from base-line, expressed as number of new cases per 1000 person-years. Longitudinal associations between baseline socio-demographic, health and lifestyle variables and incident agoraphobia were examined using a mixed logistic model [START_REF] Carriere | Choosing marginal or random-effects models for longitudinal binary responses: application to self-reported disability among older persons[END_REF]

RESULTS

In our population of community-dwelling adults 65 years and over, the base-line one-month prevalence of agoraphobia is observed to be 10.4%, with a life-time prevalence of 17.7%. Of these, 10.9% of cases were reported as having their onset over age 65. The sample, overall and according to baseline agoraphobia, is described in Table 1. Agoraphobia is more frequent in women ( p<0.0001) and in lower educational levels (p=0.01). The mean (SD) age of cases is 72.3 (5.2) and for non-cases 72.8 (4.9) (non significant). Regarding other psychiatric conditions, agoraphobia is significantly associated with trait anxiety (p=0.0005), severe depressive symptomatology (p<0.0001) and a history of major depression (p=0.02). Only one new case of agoraphobia (0.8%) had panic disorder within the follow-up period and one reported previous panic disorder at baseline (0.8%). These rates were not significantly different to those found among non-cases.

In order to determine potential risk factors for agoraphobia onset in the elderly, a mixed regression model adjusted for age and time to diagnosis examined the association between socio-demographic and clinical characteristics at base-line and incident cases of agoraphobia at 2 and 4 year follow-up (

DISCUSSION

Prevalence, incidence and co-morbidity

Our prospective study of agoraphobia in a large general population cohort using a standardized clinical interview based on DSM-IV criteria with clinical validation of cases, suggests the disorder to have a much higher prevalence in the elderly than was suggested by the 1988 ECA study (10.4% versus 1.4%). A subsequent study carried out in the U.K. using DSM III criteria [START_REF] Lindesay | Phobic disorders in the elderly: a comparison of three diagnostic systems[END_REF] on a small sample of 168 elderly persons from a community care service found similarly high rates of agoraphobia (14.9%), which was lowered to 6.5% when hierarchical exclusion rules were applied. The exclusion rule includes co-morbid major depression, which if applied to our cohort would have more than halved the base-line prevalence estimate.

Over the four-year follow-up period we detected and validated 132 new cases of agoraphobia (11.2%

of the base-line population) without application of hierarchical decision rules, giving an estimated general population incidence of 32 per 1000 person-years. During follow-up these new cases were also seen to be associated with incidence of other anxiety disorders (principally generalized anxiety disorder) and suicidal ideation. Although agoraphobia was seen to be commonly preceded by depression, new cases of agoraphobia were not accompanied by incident depression, suggesting that depression is a risk factor, and not a consequence of agoraphobia.

The overall rates observed for panic disorder (less than 1%) are similar to those found by the National Co-morbidity Survey Replication [START_REF] Byers | High occurrence of mood and anxiety disorders among older adults: The National Comorbidity Survey Replication[END_REF] . The importance of panic attacks as a risk factor for agoraphobia in younger populations [START_REF] Eaton | Panic and panic disorder in the United States[END_REF][START_REF] Weiller | Social phobia in general health care: an unrecognised undertreated disabling disorder[END_REF] has led to an assumption that they are part of the same syndrome, largely based on the behavioral hypothesis that agoraphobia is a conditioned avoidance response to the aversive stimulus of spontaneous panic attacks. According to this model panic attacks are the primary diagnosis, although other investigators including the behavioral scientist Marks [START_REF]Marks IM Phobias and Rituals[END_REF] , have questioned the temporal precedence and causal role of panic attacks in the development of agoraphobia. Clinical studies have suggested that late onset cases of agoraphobia in particular may be characterized by high rates of past major depression rather than panic attacks 9 although this has never been investigated in a prospective epidemiological study. Our findings support this observation, with only two of the 132 incident cases having a previous or recent episode of panic attacks, but having more than doubled the rates of depression found in non-agoraphobic persons at base-line. Overall, results fro the urre t stud largel support Fli t's 9 observation that depression is the primary co-pathology and that antidepressants and/or behavioral therapies, rather than benzodiazepines, should be the treatment of choice in elderly cases of agoraphobia. At baseline we found that only 6% of persons with agoraphobia were treated with an anti-depressant and 13% with an anxiolytic (results not shown). These rates were not significantly higher than for the non-agoraphobic group.

Risk factors

The principal documented risk factors for all phobias are younger age, female gender, living alone, physical illness, other anxiety disorders and depression, not having been raised by both parents, and cognitive disorder [START_REF] Schaub | Anxiety and anxiety disorders in the old and very old--results from the Berlin Aging Study (BASE)[END_REF][32][START_REF] Schulz | Phobic anxiety in late-life in relationship to cognition and 5HTTLPR polymorphism[END_REF][START_REF] Cohen | The prevalence of phobia and its associated factors in a multiracial aging urban population[END_REF] . All of these risk factors were examined in the present study. The odds of incident agoraphobia during follow-up were seen to decrease with age at baseline, whereas poorer visuospatial memory, high trait anxiety and severe depression at baseline were associated with increased odds. On the other hand we found no significant association with living alone, physical illness, or child-rearing conditions (data not shown). Interestingly, although a higher prevalence rate of agoraphobia was observed in women at base-line, the slightly greater number of women in new cases aged 65 and above did not quite reach significance, and disappeared in the multivariate risk model, probably due to confounding by depression and anxiety.

Boldrini et al. [START_REF] Boldrini | Selective cognitive deficits in obsessive-compulsive disorder compared to panic disorder with agoraphobia[END_REF] found agoraphobia to be specifically associated with spatial learning impairment and our findings further support this observation, with agoraphobia onset being accompanied by poor performance on a visuospatial memory task but not a verbal fluency test. Poor visuospatial performance has been associated with falls and sensory impairment, which might have confounded the association, however, no association was found with either sensory impairment or falls.

It has previously been suggested [START_REF] Sareen | Anxiety disorders and risk for suicidal ideation and suicide attempts: a population-based longitudinal study of adults[END_REF] that a past history of any anxiety disorder doubles the probability of both suicidal ideation and suicide attempts. We observed higher rates of suicidal ideation in persons with agoraphobia at baseline (16.6% vs. 9.1% for non-cases). This observation was further confirmed prospectively, with new cases of agoraphobia being paralleled by an increase in the incidence of suicidal ideation. On the other hand, no association was found between onset of agoraphobia and base-line cardiac pathology. Nor were new cases accompanied by an increase in incidence of cardiac disorder in contrast to previous observations relating to phobic anxiety in general [START_REF] Albert | Phobic anxiety and risk of coronary heart disease and sudden cardiac death among women[END_REF][START_REF] Kawachi | Decreased heart rate variability in men with phobic anxiety (data from the Normative Aging Study)[END_REF] . Persons with reduced mobility were also found to be at greater risk, however, its significance disappears within a multivariate analysis taking into account competing risk factors.

A weakness of the study has been reliance on retrospective recall by participants of life events and previous episodes of agoraphobia. While the refusal rate is low for an epidemiological study we cannot exclude bias due to loss at both base-line and follow-up of a more disabled group, which along with our non-inclusion of institutionalized persons at base-line may have led to an underestimation of the actual number of cases. Depression and poor physical health are strongly associated in the elderly, and while we have eliminated confounding due to all the main causes of chronic and acute illness in this cohort we have not examined self-perceived health which may have had an independent effect. Furthermore, while we have demonstrated the significance of depression as a risk factor, the study design does not permit us to clarify the causal association between the two. Further research is required to clarify whether there may be a direct relationship based on underlying neurophysiological changes driven by chronic depressive symptomatology or whether the association is further moderated by complex interactions implicating genetic and biochemical vulnerability, social learning and cognitive processes. On the other hand the study has a number of strengths; incident case identification procedures have been rigorous and this well phenotyped study has been able to examine a large number of potential confounding factors within a prospective design. Overall our findings suggest that agoraphobia may be relatively common in the elderly, occurring in over 10% of community-dwelling persons. Late-onset cases show some clear distinctions from clinical reports of early onset cases. Firstly there seems to be no clear sex difference. While early onset cases have been more frequently associated with panic disorder, this appears not to be the case in late-onset cases, in which severe depression is predominant as a risk factor rather than a consequence of the disorder. The principal risk factors for late-onset agoraphobia are younger age, severe depression, trait anxiety and poor performance on a test of visuospatial memory. Unlike other phobias, there does not appear to be increased risk for cardiac pathology, although our four-year follow-up period may be too short to definitively conclude on this point. Agoraphobia in this cohort is clearly under-treated, with preference still being for anxiolytics rather than anti-depressants despite the presence of severe depressive symptoms. Screening for agoraphobia in the elderly is clearly worthwhile as it is a highly treatable condition which may be masked by depression, and overlooked due to lack of history of panic attacks. Its association in the elderly with suicidal ideation is of clinical concern, as persons with agoraphobia may be less likely to seek assistance. Our finding that agoraphobia in the elderly has a clinically atypical presentation in comparison with younger cases is also of relevance to the on-going process of revision of diagnostic criteria for psychiatric disorder, suggesting the need to consider the possibility of a syndrome sub-type in older populations.

Clinical Vignette

A 76 year-old married woman reported experiencing a depressive episode 10 years prior to interview following a traumatic event. At this time she received only symptomatic treatment for sleeping difficulties. She has subsequently experienced chronic depressive symptoms, notably periods of tearfulness and sleep disturbance but did not have major depressive disorder at the time of examination. She currently reports being unable to go out alone for fear of something happening to her, and is particularly fearful of empty streets, crowds and public transport. She is able to drive but will only do so if accompanied. She has no past history of panic disorder and no chronic or acute illnesses or disability. Her self-rated health is very good. At two year follow-up her fears had worsened and she rarely leaves the house as her husband is now disabled.

Funding/ Support: The Esprit Study has been funded by an unconditional grant from Novartis and from the National Research Agency (ANR Project 07 LVIE004).

Declaration of Conflict of Interest:

The authors have none to declare

A

  standardized psychiatric interview, the Mini International Neuropsychiatric Interview (MINI) (French version 5.00) previously validated within the general population setting[START_REF]American Psychiatric Association Diagnostic and Statistical Manual of Mental Disorders (DSM-IV[END_REF] recorded life-time and current DSM-IV[START_REF] American | Diagnostic and Statistical Manual of Mental Disorders[END_REF] Axis I psychiatric disorders and suicidal ideation. Interviewers were trained for three months within the Department of Adult Psychiatry of the La Colombière Psychiatric Hospital, and positive cases were reviewed by a panel of psychiatrists, notably to distinguish agoraphobia from specific and social phobias. The psychiatrists reviewed cases independently in accordance with DSM-IV criteria by reference to all information provided by the MINI examination, participant responses as recorded by the interviewers, all other biological and clinical data available for the subject and if necessary after consultation with the general practitioner. Consensus agreement was subsequently reached on all cases. Only one case was reclassified as a non-case of agoraphobia (specific phobia).The MINI uses a non-hierarchical case-identification procedure thus permitting the diagnosis of psychiatric co-pathologies. The Center for Epidemiologic Studies-Depression Scale (CES-D)[START_REF] Radloff | The CES-D scale: a self-report depression scale for research in the general population[END_REF] was used to detect levels of current depressive symptomatology. Depression was classified as 'Severe' (current Major Depressive Episode by the MINI or a CES-D score>23), 'Mild' (CES-D score between16 and 22) or 'None' (CES-D score lower than 16)[START_REF] Ryan | Late-life depression and mortality: influence of gender and antidepressant use[END_REF] . Trait anxiety was assessed with the Spielberger scale[START_REF]Spielberger C Manual for the State-Trait Anxiety Inventory[END_REF] . Scores in the highest tertile were compared to the lower two. Cognitive functioning. Visuospatial memory and semantic access (verbal fluency) were assessed respectively by the Benton Visual Retention Test 22 and the Isaa s' Set Test 23 . Scores were grouped into tertiles and the lowest compared to the highest two.

  The analysis of new onset cases (excluding recurrent cases) was thus conducted on a maximum of 1461 subjects (1376 with 2-year follow-up data and 1260 with 4-year follow-up data) with neither past nor current agoraphobia at baseline, and at least one follow-up examination with complete data on agoraphobia and its principal covariates. Variables with a p-value <0.15 in the univariate model were entered into a final multivariate model. A Co 's proportio al hazards model was used to examine the association between base-line agoraphobia and incident cardio-vascular events.

(SAS version 9.2 NLMIXED procedure), taking into account the correlation between within-subject responses (repeated evaluations). This model allows the inclusion of subjects with incomplete responses across time.

Table 1 here

 1 Over the four-year follow-up 11.2% (132/1175) of the sample had a first episode of agoraphobia. The incidence rate is estimated at 32 per 1000 person-years. During the follow-up period these subjects also had more frequent first episodes of other anxiety disorders (11.5% in cases vs. 5.0% in non-

	cases; Chi²=7.96; p=0.005), specifically general anxiety disorder (8.5% in cases vs. 4.5% in non-cases;
	Chi²=3.43; p=0.06), and marginally more frequent suicidal ideation (13.3% in cases vs. 8.3% in non-

cases; Chi²=3.06; p=0.08). There was no increase compared to non-agoraphobic subjects in the incidence of severe depression (6.5% in cases vs.4.3% in non-cases; Fisher exact test F=0.11; p=0.29).

Table 2 )

 2 . The model showed a significant effect of age, with the odds of incident agoraphobia decreasing with age (OR=0.95; 95% CI 0.91-0.98; p=0.02). There was no significant effect of time and no interaction between time and age. A significant sex difference was not found in these late-onset cases. Incident agoraphobia was associated with severe baseline depression (OR=3.81; 95% CI 2.08-6.97; p<0.0001), a history of major depression (OR=1.70 95% CI 1.05-2.74; p=0.03), lower scores on

	Table 2 here

the Benton visual recall test (OR=1.53; 95% CI 0.98-2.39, p=0.058), and a higher score on the Spielberger trait anxiety scale (OR=2.48; 95% CI 1.58-3.90, p<0.0001). New cases of agoraphobia had higher rates of mobility restriction (heavy housework; ability to climb stairs; walking more than 500 metres) (OR=2.33; 95%CI 1.43-3.81; p<0.001) but not increased rates of confinement due to poor health or difficulty with instrumental activities of daily living (IADLs). Incident agoraphobia was not associated with base-line cardiovascular disease. A Cox model was also used to examine the relationship between base-line agoraphobia and incident cardiovascular disease adjusted for age, sex and education. This was also found to be non-significant (HR= 1.07 ; 95%CI 0.53-2.14 , p=0.85). (OR=1.73; 95% CI 1.03-2.90, p=0.04) as significant predictors of incident agoraphobia. While base-line severe depression greatly increased odds of subsequent agoraphobia, incident cases were not accompanied by the onset of new episodes of severe depression.

Table 1 .

 1 Baseline association between health and lifestyle variables and agoraphobia (adjusted for age, sex and education)

	Agoraphobia


Faqing Yang

Jean-Pierre Jacquot

Jeanine Souquières

JeB: Safe Simulation of Event-B Models in JavaScript

Keywords: Formal methods, Event-B, Validation, Simulation, JavaScript, Proof-Obligations

The validation of formal models is a challenge for formal methods. We propose JeB, a framework which generates and executes simulations of Event-B models, even highly nondeterministic ones. JeB allows users to safely insert pieces of code to supply deterministic computations where the automatic translation fails. We present how JeB translates Event-B model into JavaScript. We define Fidelity as the formal notion which captures the idea of the correctness of a simulation. We define it through proof-obligations.

I. INTRODUCTION

Formal methods promise the production of software which are correct, i.e., proven to meet their specification. Hence, getting the right formal specification is crucial.

The validation of formal models through execution is an old issue [START_REF] Balzer | Operational Specification as the Basis for Rapid Prototyping[END_REF], [START_REF] Fuchs | Specifications are (preferably) executable[END_REF], [START_REF] Hayes | Specifications are not (necessarily) executable[END_REF]. Actually, the main difficulty revolves around the level of determinism: good practice advocates the slow refinement of highly abstract and non-deterministic specifications [START_REF]Formal methods in industry: achievements, problems, future[END_REF] while execution tools require deterministic or quasi-deterministic models.

Event-B [START_REF]Modeling in Event-B: System and Software Engineering[END_REF] is a modeling language of the B family [START_REF]The B Book[END_REF] based on refinement; it is supported by the Rodin environment [START_REF] Rodin | Rigorous Open Development Environment for Complex Systems[END_REF]. Event-B has a dynamic semantics which is implemented by the available compilers [START_REF] Wright | Automatic Generation of C from Event-B[END_REF], [START_REF] Méry | Automatic Code Generation from Event-B Models[END_REF] and animators [START_REF] Leuschel | Automated property verification for large scale B models with ProB[END_REF], [START_REF] Servat | BRAMA: A New Graphic Animation Tool for B Models[END_REF]. However, while the semantics accounts well for nondeterminism, the current tools often fail on early models in developments. Hence, those cannot be validated.

JeB, a JavaScript framework for executing Event-B specifications, answers this issue. JeB consists of a translator which compiles the Event-B model into JavaScript code and generates enough "hooks" for developers to provide their own hand-coded resolution of non-determinism. Obviously, hand-coded functions could be "incorrect." Fidelity formally expresses this notion of correctness. It is defined so we can derive proof obligations.

JavaScript looks an unlikely choice in a formal context, yet it has technical features which fit well with our purpose. Furthermore, the browsers running JavaScript allow to set up easily graphical displays.

We first present Event-B. Then, we discuss JeB's design and the translator's implementation. Last, we show the formal definition of fidelity and the associated proof obligations.

II. EVENT-B

A. Notations

A specification in Event-B consists of a state and events. The state maps names to values; it is constrained by an invariant. For practical purposes, models are split into Contexts and Machines. The values are built inductively from integers, booleans and symbols by using power sets and cartesian products. Special cases such as binary relations, partial functions, or injections enjoy specific notations. The typing system is equivalent to set membership and inclusion. The invariant is a first-order formula on the state. It is a conjunction of smaller formulas called axioms in contexts and invariants in machines.

Events model the evolution of the state. Formally, they are guarded substitutions. Guards are first-order formulas on the state; they may contain free variables called event parameters. Substitutions change some values, all at the same time. An event is enabled when its guard is true, it can then be fired.

The formal semantics of an Event-B model is based on the feasibility (fis) property expressing two ideas:

• a legal state with actual values must exist, and • firing enabled events leads from legal states to legal states. The specification language is designed so that fis can be cast as a set of small logical formulas, called proof-obligations. A model is correct when all its POs have been discharged.

Figure 1 shows the first model of a platooning system. Vehicles are required to maintain a minimum distance dmin between themselves. At this level, the distance function dist, the representation of the geometric surface Plane and the movement of the platoon move are abstractions.

B. Refinement

Event-B embodies two ideas about programs: they are elaborated by stepwise refinements, and they can be correct by construction. In this context, correct means "mathematically proven to meet their specification."

A model M r is a refinement of a model M a , if:

• M r is consistent (i.e., it defines one actual state, invariants are preserved through the actions), • there is an abstraction function from the M r state and events to the M a state and events, • M r legal states are abstracted as M a legal states, and • all events fired in M r preserve the invariant of M a . Refinement is embedded in the framework at two levels. The language contains a syntax to express the refinement relationship (refines or extends) and the abstraction function (with clause). The support tools generates the POs.

CONTEXT space SETS Plane Vehicles

CONSTANTS dist dmin AXIOMS axm1: dmin ∈ N 1 axm2: dist ∈ Plane × Plane → N 1 axm3: ∀x, y.dist(x → y) = dist(y → x) axm4: ∀x.dist(x → x) = 0 END MACHINE platoon SEES space VARIABLES pos INVARIANTS inv1: pos ∈ Vehicles → Plane inv2: ∀v1, v2•v1 = v2 ⇒ dist(pos(v1) → pos(v2)) > dmin EVENTS INITIALISATION = BEGIN act1: pos :| ∀v1, v2•v1 = v2⇒ dist(pos (v1) → pos (v2)) > dmin END move = STATUS ordinary ANY np WHERE grd1: np ∈ Vehicles → Plane grd2: ∀v1, v2•v1 = v2 ⇒ dist(np(v1) → np(v2)) > dmin
In Event-B, refinements add information into a model. Users can see a refinement as one of four kinds:

• adding new invariants; this reinforces the properties of interest and the constraint on the domain, • adding new variables and constants unconnected to previous ones; this introduces new concepts and properties, • adding new variables and constants to implement previous ones; this is the usual data-refinement, or • adding new events; this splits an abstract "large" event into several concrete "smaller" events.

C. Event-B Operational Semantics

The operational semantics of Event-B is a three-step cycle: 1) compute the set of enabled events, 2) pick one enabled event and values for its parameters, 3) apply the substitution on the state. The INITIALISATION event starts the cycle which ends when no event is enabled. Depending on the modeled system, stopping can be a desired feature (termination) or not (deadlock).

Non-determinism is present at three levels: free variables can take any value which makes the guards true, substituted values can be described non-constructively by a property ("any value such that"), and any enabled event can be fired. As a practical consequence, execution tools must deal with nondeterminism and the associated combinatorial explosion.

III. JEB DESIGN

A. Motivations

The claim that a proven Event-B model is therefore correct in the broad sense is too strong as the three cases below show.

A first case is the introduction of new axioms during a refinement. The new model may then become logically inconsistent, which is a non-decidable property. We must resort to test-like procedures like proving formulas such as true = f alse.

A second case concerns the limitation on provable properties. In Event-B, temporal properties are notoriously difficult to state and to prove. Therefore, some may be left unchecked.

A third case concerns the introduction of new events, that is, new behaviors. Even when requirement documents guide the specifiers, emergent behaviors may slip in then and stay unnoticed until the model is actually executed.

So, the equivalence between "proven" and "correct" can only be claimed if all properties have been expressed in the initial models. Stated another way: we must have complete requirements before developing. Unfortunately, we know that we do not for most actual projects [START_REF] Nakatani | Requirements Maturation Analysis by Accessibility and Stability[END_REF].

B. Target Language

We use JavaScript/HTML as the target language because:

• JavaScript [START_REF]ECMAScript Language Specification[END_REF] is embedded and interpreted in most Web browsers. Those environments provide efficient and lightweight tools to build generic and ad-hoc GUI. • JavaScript supports sophisticated OOP techniques which helped solve two issues: the name conflicts and the traceability between the JavaScript and the Event-B codes. The generated code is clean and easy to read. • JavaScript uses dynamic interpretation that allows users to switch between different implementations even at runtime. We use this feature to separate user hand-coded functions from the main simulator code. • JavaScript has first-class functions, which eased the translation of nested expressions and quantifications. The architecture of JeB reflects our philosophy that a simulation is the result of a cooperation between tools and humans. The former provides the efficiency and safety of automation, the latter provide the insights to overcome nondeterminism. Humans are involved at three levels:

• specifiers provide hand-coded functions for some uninterpreted functions, • experts provide values for constants and event parameters in different scenarios; they set up graphic visualizations, • users run simulations, observe and analyze behaviors to check that an Event-B model meets their expectations.

IV. JEB REALIZATION

Technically, a simulation consists in three parts: the generated code, a runtime library, and the hand-coded functions provided by the users.

A. Generated code 1) Namespace: Generated names must not conflict between themselves or existing names in the target environment, and should be traceable back to Event-B. With prefixes on global object properties, we can achieve the same effect as with namespaces; Table I shows some examples.

2) Translation of Contexts: Each context is translated into a file which contains the translation of the axioms as JavaScript objects. The overall structure of the file is derived from the structure of the Event-B code, as shown on Table II where id is a unique reference; label is axiom's name as written in the context; domNode links this instance to the HTML page to display its evaluation; predicate is a method to evaluate the axiom.

3) Translation of Machines: The translation of a machine generates three files: an executable version of the model, a configuration file (both JavaScript), and a simulation GUI (HTML). The configuration file contains stubs and default implementation of non-deterministic features.

a) Variables: Each variable is translated as an instance of jeb.lang.Variable, prefixed by $var: where id is a unique reference; value is the current value; _value is the primed value; domNode binds to an element in the HTML page which displays its value; updateView is the method used for updating the user interface. The variable value can be any Event-B mathematical object. It is checked by computing the invariant after each simulation cycle.

b) Invariants: They are translated like axioms, using jeb.lang.Invariant instead of jeb.lang.Axiom. c) Events: JeB generates an independent simulation for each refinement, so the refinement links (refines and with) are ignored. The guards and actions are translated as two different functions. Events' parameters require a special treatment described thereafter. Each event is translated as an instance of jeb.lang.Event: Each true parameter par is associated with an argument generator function get_par which is bound to the input field in the HTML page. The JeB translator generates it into a configuration file as a function stub or, when possible, as a default implementation. Users should provide their own implementation for a realistic simulation in the auto-run mode of execution. Before each simulation cycle, the bindArguments method binds each parameters to a get_par function, which can then be changed "on the fly."

The order in which the parameters are declared is irrelevant in Event-B, but not in JavaScript. When necessary, the JeB translator adjusts the order of parameters in the GUI and in the bindArguments function so they get a value before being used.

Each identifier declared in an ANY clause is translated as an instance of jeb.lang.Parameter: jeb.lang.Parameter = function( id, type, eventId ) { this.id = id; this.type = type; this.domNode = jeb.ui.$( id ); this.domNodeInput = jeb.ui.$( id + '.input' ); this.eventId = eventId; ... };

where id is a unique reference; type indicates its nature (local variable or true parameter); domNode (resp. domNodeInput) binds to an element in the HTML page for display (resp. input), eventId references the event;

e) Event Guards: An event guard is a predicate formula. The enabled status of an event is the result of computing all its guards. Guards are translated like axioms with an added reference to the event.

f) Event Actions: Actions are assignments with two features: they occur simultaneously and they can involve nondeterministic values ("becomes such that" for instance).

The left-hand side of Figure 2 is a classical trap. The idea is to use only :| assignments and "primed values" as shown on the right-hand side. The order of execution becomes then irrelevant. Technically, the assignments are realized on the variables' property _value and copied to the value property after all assignments have been made.

The non-deterministic assignments generate stubs in the configuration file which call default implementation in the runtime library. Users may override them to provide their own, deterministic, implementation.

Each action is coded as an instance of where assignment is the method to realize the assignment.

4) Translation of Formulas: Each operator is coded as a call to the runtime library. The API of the library is a oneto-one mapping of the Event-B mathematical notation. So, the translation algorithm is based on Event-B syntax and independent of the target language. Proving the correctness of the translation resolves into proving the library functions. Table III shows some translation rules.

B. Runtime Library

1) Simulation Scheduler: The operational semantics is implemented as follows:

(1) setup contexts, prompt user if needed (2) trigger the INITIALISATION event (3) do

(1) save the state of variables (2) update the variable view (3) compute the invariants, stop if one is false (4) build the set of enabled events, stop if empty ( 5) pick an enabled event to trigger [START_REF] Rodin | Rigorous Open Development Environment for Complex Systems[END_REF] save the state of arguments [START_REF] Wright | Automatic Generation of C from Event-B[END_REF] execute the actions of the selected event

The step (3.3) is useless when executing a fully proven model, but it is a useful feature for the preliminary exploration of complex refinements. Step (3.4) is a computation of all the guards of the events based on the state values and the values chosen for the parameters, either through user's input in the GUI or computation of the get_par functions.

2) JavaScript Library for Event-B: The computation core of the expressions is delegated to a library which implements set theory and first order logic. Its realization aims at two goals: a clear interface and efficient computations.

Technically, the APIs are modeled on the mathematical language of Event-B. The translation from Event-B to JavaScript is mostly syntactic. The APIs contain about 90 profiles.

The representation of numbers is an important issue. In Event-B, integers are unbounded; contrary to JavaScript primitive numbers. Discretization of computations, tiny units or large multiplicative constants are standard modeling tricks to model R or functions such as sin. They induce very large numbers. The library implements arbitrary large integers.

3) Graphical User Interface: The simulation interface is implemented as an HTML page [START_REF] Yang | The case for Using Simulation to Validate Event-B Specifications[END_REF]. JeB provides a generic page with the code needed to control it.

C. Hand-Coded Add-Ons

An important feature of JeB is to allow users to provide safely pieces of code to improve the simulation.

Implication P ⇒ Q $B.implication(P T R , Q T R ) Universal ∀x 1 , . . . , x n •P (n ≥ 1) $B. f orAll(P T R * , [x T R * 1 , . . . , x T R * n ]) Set membership E ∈ S $B.belong(E T R , S T R ) identifiers / Atomic values / Expressions Free identifier χ 1) $cst.χ if χ is a constant 2) $var.χ.value if χ is a variable 3) $arg.χ.value if χ is a parameter Boolean TRUE TRUE $B.TRUE Bool expression bool(P) $B.bool(P T R ) Integer literal α $B( α ) Bool expression bool(P) $B.bool(P T R ) Subtraction m -n $B.minus(m T R , n T R ) Sets / Relations Empty set ∅ $B.EmptySet Interval m .. n $B.UpTo(m T R , n T R ) Natural numbers N $B.NATURAL Set extension {E 1 , . . . , E n } (n ≥ 1) $B.SetExtension(E T R 1 , . . . , E T R n ) Ordered pair E → F $B.Pair(E T R , F T R ) Relations S ↔ T $B.Relations(S T R , T T R ) Partial functions S → T $B.PartialFunctions(S T R , T T R ) Function image f (E) $B. f unctionImage( f T R , E T R ) Assignments Becomes such that x 1 , . . . , x n :| Q(x 1 , . . . , x n ) (n ≥ 1) $B.becomesSuchThat([x T R 1 , . . . , x T R n ], Q T R * , [x 1 T R * , . . . , x n T R * ])
1) Graphical Display: The generic GUI contains two stubs:

• jeb.animator.init to initialize the display area,

• jeb.animator.draw to draw the system's state. The second function is called at each cycle, the first one is called only once during initialization.

2) Parameters of Events: They are the main controls when running a simulation. The value of each "true parameter" is obtained by getting the content of the input fields in the GUI. Those fields can contain either a literal value or a function call. In the latter case, the execution mechanism looks for an implementation in the configuration files. Users can switch between values and functions at any time during a simulation.

V. CORRECTNESS OF SIMULATION

The notion of correctness is captured by the idea of fidelity.

A. Definition of Fidelity

The execution of an Event-B model M is formalized as a trace [START_REF] Bert | Genesyst: a tool to reason about behavioral aspects of B event specifications. application to security properties[END_REF]. Intuitively, a trace is a succession of instances of firings of events 1 , starting with the E 0 (INITIALISATION), which goes through a succession of legal states. Formally, E 0 e 1 e 2 . . . e n is a trace iff ∀ j. j ∈ 1..n ⇒ e j ∈ Evts(M) and fis(E 0 ; e 1 ; e 2 ; . . . e n ) ⇔ true where fis is the feasibility predicate defined as the point-wise application of the feasibility PO of the machine M [START_REF]The B Book[END_REF]:

Axm(s, c) ⇒ ∃v • BAP E 0 (s, c, v )
1 lowercase e i denotes instances, uppercase E i denotes events

m i=1 Axm(s, c) ∧ Inv(s, c, v) ∧ Grd E i (x E i , s, c, v) ⇒ ∃v • BAP E i (x E i , s, c, v, v )
where s, c, v are the Sets, Constants and Variables of the state, Inv and Axm the invariants and axioms, BAP the Before-After predicate of a substitution, and v is the After-value.

Traces(M) is the set of all traces of the machine M.

Intuitively, fidelity is seen as the inclusion of the set of traces of the executable model into Traces(M). However, one set belongs to the JavaScript world, while the other belongs to the Event-B world. So, we introduce three abstraction-functions:

• f ∈ V J → V B which maps values in JavaScript to their equivalent in Event-B, • eval which evaluates the JavaScript translation f Ψ () of the Event-B predicate Ψ. eval is assumed such that:

eval(x t = x 0 ); eval( f Ψ ()) == true (resp. f alse) ⇔ bool([x := f (x 0 )]Ψ) = TRUE (resp. FALSE)
where [a := b]Ψ is the substitution of a by b in Ψ. • f Trace ∈ f Evts(M) → Evts(M) which maps the JavaScript translation of each event to each Event-B event. Assuming f and eval and noting x f e j the event's parameters, the set of "interesting" traces in a simulation is defined as where Ψ contains several application of g, and type(v k ) is a typing predicate for v k . Ψ is translated into a program, Prog, using JeB rules for predicates and calls to the user's implementation, g user , for each appearance of g. Let f Ψ be the translation in JavaScript of Ψ using the definition of g, then the PO is wp(Prog, f Ψ ) ⇒ n k=1 f type (v k ) where wp is the usual weakest-precondition transformer. POs 1, 2 and 5 can be discharged within the Event-B system; POs 4 and 6 must be discharged within JavaScript semantics.

f E 0 (); f e 1 (x f e 1 ); f e 2 (x
{ f (v J ) | v J = f act ()} ⊆ {v | BAP act (x E i , s, c, v, v )} 6

C. Assumptions

The discussion of fidelity focused on our main contribution: the safe inclusion of hand-coded pieces of code. Discharging the POs proves the fidelity under four assumptions: A1 Event-B values can be represented in JavaScript, A2 Event-B expressions can be translated into an observational equivalent JavaScript expression, A3 Event-B AST can be syntactically mapped to library calls, A4 Event-B operational semantic cycle can be implemented into a scheduler in JavaScript. SETL [START_REF] Schwartz | Programming with sets; an introduction to SETL[END_REF] shows that A1 is reasonable. Existing translators such as B2C [START_REF] Wright | Automatic Generation of C from Event-B[END_REF] and EB2ALL [START_REF] Méry | Automatic Code Generation from Event-B Models[END_REF] show that A2 makes sense. The design of our run library, whose API covers all Event-B notations, establishes the validity of A3. A4 grounds tools such as ProB [START_REF] Leuschel | Automated property verification for large scale B models with ProB[END_REF] and Brama [START_REF] Servat | BRAMA: A New Graphic Animation Tool for B Models[END_REF]. We are confident that the assumptions can be proven. Such proofs would use the wellestablished techniques of proving compilers.

VI. CONCLUSION

In [START_REF] Mashkoor | Stepwise Validation of Formal Specifications[END_REF] we showed how a formally correct model can be safely transformed into an "incorrect" animatable model which keeps the same behaviors. Here, we showed how to produce simulations which are guaranteed to preserve a subset of the behaviors. So, we have the theoretical framework necessary to validate most refinements in a development.

The design and implementations of support tools for proving fidelity is the next challenge: the mix of different formal frameworks raises interesting questions. Another challenge lies in the invention of techniques to create, manage and replay validation scenarios using simulations and animations.

Figure 1 .

 1 Figure 1. Initial model of a platooning system

  jeb.lang.Event = function( id, label ) { this.id = id; this.label = label; this.domNode = jeb.ui.$( id ); this.enabled = true; this.parameter = {}; this.guard = {}; this.action = {}; this.bindArguments = function(){}; ... }; jeb.Event.prototype.evaluateGuards = function(){...}; jeb.Event.prototype.testGuards = function(){...}; jeb.Event.prototype.updateParametersView = function(){ ...}; jeb.Event.prototype.doActions = function(){...};where id, label, and domNode have the same role as for axioms. The property enabled contains the result of the evaluation of the guards. The properties parameter, guard, and action are namespaces for the event's parameters, guards and actions, respectively. The four functions are helpers for implementing the simulation cycle: evaluateGuards and testGuards are used for determining parameter values, updateParametersView and doActions do what their names imply. d) Event Parameters: The so-called "event parameters" in Event-B are the variables introduced in the ANY clause act1: a := b act2: b := a act3: c :∈ S act4: x, y :| x > y ∧ y < x + z act1: a :| a = b act2: b :| b = a act3: c :| c ∈ S act4: x, y :| x > y ∧ y < x + z

Figure 2 .

 2 Figure 2. Assignments

  f e 2 ); . . . ; f e n (x f en ) belongs to TraceSimulation(M) if n j=1 eval( f e j . f Grd (x f e j )) == true The definition of fidelity is simply that all traces in TraceSimulation(M) can be abstracted to a trace of M ∀t •t ∈ TraceSimulation(M) ⇒ map(t, f Trace ) ∈ Traces(M)B. Proof ObligationsThe general definition can be broken down into local properties, which allow to associate a specific PO to each hand-coded element[START_REF] Yang | A Simulation Framework for the Validation of Event-B Specifications[END_REF]. Six cases have been identified 1) Valuation of constants. The PO checks the axioms hold. bool([s, c := f (s J ), f (c J )]Axm(s, c)) = TRUE 2) Valuation of parameters. The PO checks the guards hold. n j=1 bool([x e j := f (x f e j )]Grd e j (x e j , s, c, v)) = TRUE 3) Parameter generator. The produced value is checked against the event's guards, no proof is needed. 4) Predicate in an invariant or a guard. Let f Ψ be the user implementation of the predicate Ψ, the PO is eval( f Ψ ()) == true ⇔ bool(Ψ) = TRUE 5) Value for an action. Let f act the user implementation. The PO ensures that computed values are admissible values.

  ) Function defined by non-constructive properties. Technically, this is the most difficult case. An axiom defining a function g has the form∀v 1 , ..., v n •type(v 1 ) ∧ ... ∧ type(v n ) ⇒ Ψ(g, v 1 , ..., v n )

Table I NAMESPACES

 I USED IN THE SIMULATOR CODE (EXCERPT)

	Namespace	Prefix	Description
	jeb	jeb	the top namespace
	jeb.axiom	$axm	axioms
	jeb.event	$evt	machine events
	$evt.<eventId>.arg	$arg	event parameters
	$B	$B	JavaScript library for Event-B
		Table II
	STRUCTURAL MAPPING OF A CONTEXT
	Event-B	JavaScript/HTML
	CONTEXT name	(1) name.js (context model)
		(2) name.html (user interface)
	EXTENDS context_names	list of context_name in the HTML page
		for navigation
	SETS identifiers	list of $cst.identifier
	CONSTANTS identifiers	list of $cst.identifier
	AXIOMS predicates	list of jeb.lang.Axiom instances
	END

  . a) Sets and Constants: They are translated as standard identifiers prefixed by $cst. They are given values in the configuration files. Enumerated sets are instantiated by collecting elements already defined in the CONSTANTS clause. The JeB library supports the instantiation of a carrier set either as a collection of symbolic strings or as a class in the OOP sense.b) Axioms: JeB translates each axiom as an instance of jeb.lang.Axiom, prefixed by $axm:

	jeb.lang.Axiom = function( id, label ) {
	this.id = id;
	this.label = label;
	this.domNode = jeb.ui.$( id );
	this.predicate = function(){};
	...
	};

Table III FORMULA

 III TRANSLATION RULES (EXCERPTS) ( T R AND T R * DENOTES RECURSIVE CHILD TREE TRAVERSAL)

	Event-B Notation	Event-B Syntax	Translation
		Predicates
	True predicate		$B.bTrue()


Faqing Yang

Jean-Pierre Jacquot

Jeanine Souquières

Proving the Fidelity of Simulations of Event-B Models

Keywords: Formal methods, Event-B, Validation, Simulation, JavaScript, Proof obligation

A major hindrance to the use of formal methods is the difficulty to validate the models, particularly at the early stages of the development. We propose to build simulations: programs automatically generated from the specifications but with user-provided implementations of the non-executable traits of the models. We present such a simulation. Of course, the question of the fidelity of the simulation to the model is raised in such a setting. We provide a formal definition of fidelity and the proof obligations that can be attached to each hand-coded element so that fidelity can be proven.

I. INTRODUCTION

Among the techniques required to develop high assurance systems, refinement-based formal methods have a strong appeal. Their foundational idea is that it is possible to develop pieces of software which are correct by construction. So, when the code is delivered, there should be no need to test it for discovering anomalies or to check its conformity to the specification. This is made possible by languages such as B [START_REF] Souquières | The B Book[END_REF] and Event-B [START_REF]Modeling in Event-B: System and Software Engineering[END_REF] with their environments which make this paradigm an effective choice for developers.

For those "development methods," building a software is constructing a sequence of formal models with the following properties:

1) the first model is an abstraction of the specification of the software, 2) the last model is a concrete model, i.e. a model fully deterministic and implementable on current machines, 3) each model is formally consistent and "correct," and 4) each model, except for the first, is formally tied to the previous one by a "refinement" relation and all ties can be proven "correct."

"Correct" is perfectly defined above. In case 3, it is the preservation of an invariant; in case 4, it is the existence of some abstraction function between the models with the property to preserve the abstract invariant when the concrete invariant is preserved. The language used for expressing the formal models is designed in such a way that the correctness properties can be cast into sets of small theorems. It is also designed so the proofs of the theorems can be conducted with current software provers.

The weak point of refinement-based methods is actually the first case above. There are two reasons for this weakness.

A minor one is the difficult to go from informal requirements toward formal models. Works on requirements elicitation with formal goal models [START_REF] Dardenne | Goal-directed requirements acquisition[END_REF], on transforming goal models into specifications [START_REF] Matoussi | A First Attempt to Express KAOS Refinement Patterns with Event B[END_REF], or on formal domain modeling in [START_REF] Mashkoor | Guidelines for Formal Domain Modeling in Event-B[END_REF] for instance, show that the formalization question can be answered. The major reason lies in the fact that requirements evolve during many projects [START_REF] Nakatani | Requirements Maturation Analysis by Accessibility and Stability[END_REF]. Therefore, it is unlikely that the very first formal model will contain the complete and final specification.

The obvious solution is to cycle developments, including new requirements as they are discovered. However, in practice, such cycle can work only if the new requirements are discovered early and if they can be included smoothly into the chain of refinements. The worst case scenario is when the discovery happens on the coding phase and requires to restart all the development from the initial model.

In this paper, we defend the point of view that all models, or at least, most of them, should be validated as well as verified. Validation ensures that the model is a description of the software we really want. To achieve this, we need specific tools and theories.

A usual technique is to run the model. Tools such as animators, ProB [START_REF] Leuschel | Automated property verification for large scale B models with ProB[END_REF] for instance, or translators, EB2ALL [START_REF] Méry | Automatic Code Generation from Event-B Models[END_REF] for instance, allow to execute some Event-B models, but they fail on most because of their high level of non-determinism. We propose a tool JeB, a JavaScript simulation framework for Event-B. This tool generates automatically JavaScript programs, combining ideas from animators and translators, but it allows users to add hand-coded elements to supply deterministic solutions when needed. Our case-studies show that the manual part amounts to only 1% of the size of the simulation [START_REF] Yang | The case for Using Simulation to Validate Event-B Specifications[END_REF]. On the one hand, this strategy allows us to execute a lot of models, for a small cost. On the other hand, it raises some questions about the correctness of the observations made during the executions.

Our answer is to propose a formal notion, called fidelity, which defines precisely the form of correctness we desire. From this definition, we can derive what must be proven in order to ensure that what is observed on a simulation is what is specified in the model.

The paper is organized as follows. We first present Event-B and the refinement-based process it supports. We present then a case-study to motivate the necessity and the difficulty of validating early steps in a development. The simulation of the models is discussed after. Last, we present the notion of fidelity and the proof obligations that can be generated to assess that a particular simulation is correct.

II. EVENT-B

A. Language

A specification in Event-B consists in two parts: a state and events. The state maps names to values; it is constrained by an invariant. For practical purposes, models are split into Contexts and Machines which describe respectively the constant and the variable parts of the state. The values are build inductively from integers, boolean and symbols by using power sets and cartesian products. Special cases such as binary relations, partial/total functions, or injections enjoy specific notations. The typing system is equated with the "belongs to" relation between a value and a set.

The invariant is a first-order formula on the state. It is constructed as the conjunction of smaller formulas called axioms and invariants in contexts and machines.

Events model the evolution of the state. Formally, they are guarded generalized substitutions. Guards are first-order formulas on the state; they may contain free variables called event parameters. Substitutions change some values, all at the same time. An event is enabled when its guard is true, it can then be fired. The substitution uses the parameters' values which made the guard true.

The formal semantics of an Event-B model is based on the feasibility (fis) property expressed as two ideas:

• a legal state with actual values must exist, and

• the firing of any enabled event from a legal state leads to a legal state.

The specification language is designed so fis can be cast as a set of small logical formulas, called proof obligations. A model is correct when all its POs have been discharged. POs can be automatically generated; current provers can discharge automatically most of them.

B. Refinement

Event-B embodies a development method based on the association of two ideas: programs are constructed through stepwise refinements, and programs can be correct by construction. In this context, correct means "mathematically proven to meet its specification."

Mathematically, the refinement is a relation between models. A model M r is a refinement of a model M a , if:

• M r is consistent (i.e., it defines one actual state, invariants are preserved through the actions),

• there is an abstraction function from the M r state and events to the M a state and events,

• M r legal states are abstracted as M a legal states,

• all events fired in M r preserve the invariant of M a .

These properties generate POs. Discharging all POs of all refinements in a chain guarantees that the most concrete model preserves the invariant of the most abstract model.

These definitions are embedded in the framework at two levels. The language provides users with a syntax to express the refinement relationship (refines or extends) and the abstraction function (with clause). The support environment generates the POs.

In Event-B, refining is an activity which adds information into a model. Users can see a refinement as one of four kinds:

• adding new invariants; this reinforces the properties of interest and the constraint on the domain,

• adding new variables and constants unconnected to previous ones; this introduces new concepts and properties,

• adding new variables and constants to implement previous ones; this is the usual data refinement which reifies abstract data structures,

• adding new events; this splits an abstract "large" event into several concrete "smaller" events.

Of course, it is possible to build a refinement belonging to several kinds, but this is bad practice [START_REF]Formal methods in industry: achievements, problems, future[END_REF].

C. Operational Semantics

Event-B has an intuitively simple operational semantics. It is a cycle of three steps : 1) compute the set of enabled events, 2) pick one event and one value for each of its parameters, 3) apply the substitution on the state.

The cycle starts with the INITIALISATION event and ends when no event is enabled. Depending on the system modeled, stopping can be a desired feature (termination) or not (deadlock).

The operational interpretation of an Event-B model relies on non-determinism at three levels: free variables can take any value which makes the guards true, substituted values can be described non-constructively by a property ("any value such that"), and any enabled event can be fired. So, the execution of Event-B specifications requires tools that can deal with non-determinism. In practice, this means that combinatorial explosion must be tamed.

III. CASE-STUDY

A. Platooning

New urban transportation systems could be build with small automatic electric public cars. For several reasons, such cars should be able to move in platoons. This moving mode involves several vehicles which aggregate and move like a train but which are connected by virtual rather than material links. The software which controls the cars, except for the platoon's leader, is typical of the kind for which formal methods where created. Modeling and developing control algorithms for platooning are an excellent case-study.

We have studied a local version of the Daviet-Parent algorithm [START_REF] Daviet | Longitudinal and Lateral Servoing of Vehicles in a Platoon[END_REF]. It relies on vehicles being able to observe the position and speed of their front neighbor in the platoon and make decision on those values; no communication between vehicles are required. While not the most efficient control algorithm, it is very robust and could then be used as a fall-back solution when sophisticated communication-based systems fail. In [START_REF] Lanoix | Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles[END_REF], a simplistic "linear" (or 1D) version of the Davier-Parent algorithm id modeled to assess the feasibility of using Event-B to develop a proven version; In [START_REF] Yang | Scaling Up with Event-B: A Case Study[END_REF], a more realistic 2D version is presented. Both versions end in a deterministic model which guarantees that no vehicles belonging to the same platoon may collide. The version presented thereafter has been slightly modified from [START_REF] Yang | Scaling Up with Event-B: A Case Study[END_REF].

B. First Two Models

Figure 1 shows the very first model of 2D platooning 1 . The safety property is expressed as an invariant: vehicles are required to maintain a minimum distance dmin between themselves. When the platoon moves, the invariant is preserved.

It should be noted that this model is totally abstract. In a sense, we don't define much more than a vocabulary. The distance function dist , the representation of the geometric surface Plane, the set of vehicles Vehicles and even the movement of the platoon move are abstractions. We assume only that they exist, they can be observed, and they have some basic obvious properties. For instance, the axiom labeled axm9 states that there is enough space to contain one platoon.

Figure 2 is the first refinement. The movement of the platoon is decomposed into the movements of its members. From the perspective of validation, it is important to note the following additions to the initial model which are brought up by the first refinement:

1) two new events, 2) three new variables in the state, with their respective invariants, which represent an abstraction of "temporary" movements, 3) the reduction of the non-determinism of the event move by an abstraction function which lifts the concrete variable tpos as the abstract parameter np, 4) an implicit constraint, introduced by the guard labeled forw, which states that the vehicles move forward.

Those additions actually introduce several behaviors and properties into the model. Some behaviors may be explicit in the requirements; for instance, the "order" in which the individual vehicles move is modeled by the non-determinism in the events fst_move and nth_move. Some behaviors may be implicit or inferred; for instance, the invariant labeled tpos_safety requires that the temporary positions and the "observed" positions are all spaced apart by dmin at least. This is a stronger property than the invariant. Some behaviors may sneak in as emergent behaviors. For instance, the model may have deadlocks, or platoons may be unable to stop. A validation of the model is then strongly advised, both to check the correct formulation of the explicitly and implicitly required behaviors, and to exhibit and assess the other behaviors.

IV. SIMULATION OF THE MODEL

A. Executing the model

Any kid playing with dinky toys would be able to execute platoon1 without any difficulty. Yet, no current execution tool 1 The specification presented here is a simplified version of the actual specification. could animate it or translate it into an executable program. On the one hand, the tools need to consider all the options opened by the non-deterministic features: all the possible realizations of the Plane space, all the possible realizations of the distance computation, all the possibilities to put the vehicles in their initial positions, etc. Even when the space of possible values can be automatically explored, it is often impractical because of combinatorial explosion. On the other hand, the kid has an approximate, but good enough, implementation of the elements of the model: a tabletop for Plane, a ruler for dist , some natural constraints on the movement (no jump, limited turning radius), etc. An interesting observation is that, even if the dinky toys cover only a tiny fraction of all the theoretically possible implementations of platoon1, they are in practice the most interesting to observe: the final system will have analogous constraints.

CONTEXT space SETS Plane Vehicles

CONSTANTS dist dmin AXIOMS axm1: f inite(Vehicles) axm2: f inite(Plane) axm3: dmin ∈ N 1 axm4: dist ∈ Plane × Plane → N 1 axm5: ∀x, y•x ∈ Plane ∧ y ∈ Plane ⇒ dist(x → y) = dist(y → x) axm6: ∀x•x ∈ Plane ⇒ dist(x → x) = 0 axm7: card(Vehicles) ≥ 2 axm8: card(Plane) > card(Vehicles) axm9: ∃start •start ∈ Vehicles Plane ∧ (∀v1, v2•v1 ∈ Vehicles∧ v2 ∈ Vehicles ∧ v1 = v2 ⇒ dist(start(v1) → start(v2)) > dmin) END MACHINE platoon SEES space VARIABLES pos INVARIANTS type_pos: pos ∈ Vehicles → Plane pos_safety: ∀v1, v2•v1 = v2 ⇒ dist(pos(v1) → pos(v2)) > dmin EVENTS INITIALISATION = BEGIN act1: pos :| pos ′ ∈ Vehicles → Plane∧ ∀v1, v2•v1 = v2 ⇒ dist(pos ′ (v1) → pos ′ (v2)) > dmin END move = STATUS ordinary ANY np WHERE type_np: np ∈ Vehicle → Plane inv_np: ∀v1, v2•v1 = v2 ⇒ dist(np(v1) → np(v2)) > dmin
JeB, a JavaScript framework to simulate Event-B models, is based on the last observations. Automated tools and human can cooperate to build and run simulations of formal models. Most of the simulation programs can be automatically generated from the Event-B text. Specifiers have only to provide a few quasi deterministic resolutions of non-deterministic features which will be good approximations of the solutions to come. We don't present the details of JeB in this paper and refer the interested readers to [START_REF] Yang | The case for Using Simulation to Validate Event-B Specifications[END_REF], [START_REF] Yang | A Simulation Framework for the Validation of Event-B Specifications[END_REF]. Simulating a specification with JeB is a process with four steps:

END nth_move = ANY v npv WHERE type_v: v ∈ 2..card(Vehicles) v_move: v ∈ unmoved to : npv ∈ Plane forw: dist(npv → pos(iveh(v -1))) < dist(pos(iveh(v)) → pos(iveh(v -1))) safe: ∀i.i ∈ 1..card(Vehicles) ∧ i = v⇒ dist(t pos(iveh(i)) → npv) > dmin
1) the JeB translator generates a JavaScript program from the axioms, invariants and events of the system, and an HTML page; 2) users complete the program by providing JavaScript functions for generating values for non-deterministic event's arguments and assignments, for implementing carrier sets and functions defined by properties; 3) optionally, users realize a graphical display to adapt the visualization of the state to their purpose; 4) simulations are run, using the scheduler and the set library provided by JeB as a part of the simulator runtime.

Experiments with different specifications at all their refinement stages indicate that the above step (2) accounts for around 1% of the size of the simulation programs.

B. Moving Platoons

When JeB is activated on the specification, it generates the bulk of the code for two independent simulations2 : one for platoon and one for platoon1. Those simulations cannot be run directly as the models contain several traits either non executable or executable with unpractical inefficiency. Four points require us to provide our own code.

1) Carrier sets: Neither Plane nor Vehicles are specified in enough details that an implementation can be derived automatically. Vehicles can be simply enumerated:

$cst.Vehicles = $B.SetExtension( 'Vehicle01', 'Vehicle02', ' Vehicle03' );
Plane cannot be enumerated in a useful way. However, we can be fairly confident that a standard cartesian representation is adequate. In JavaScript, this is done with the definition of an object:

2) Function dist:

The function dist is definite descriptively rather than constructively by the axioms. Again, a standard euclidean definition is a reasonable approximation of the function that will be implemented in future refinements. A possible implementation is: 3) Initialization: The starting position of the platoon can be set by a probabilistic computation. However, this has two disadvantages: we may have to wait long before an admissible value is found, and, more to the point, many random legal position are without any interest (vehicles spaced too far apart). The value of iveh is not very important, so, setting it to facilitate the reading of the state is a good idea. So, the nondeterministic assignments labeled ini_pos, ini_tpos and init_iveh are realized as assignments to predefined values:

$cst.dist = $B.

4) Generation of arguments:

The generation of the arguments for the events leads to the same reflection as the one above. We can still get a probabilistic choice but on a restricted range for the parameters in platoon1: The scheduler will call the two functions repetitively until a value makes the guards true or the number of calls exceeds a specified limit.

The total amount of code provide by us for the simulations of the two machines is around 150 lines, including a graphical display of the platoons (not shown here). The total amount of code of the simulation is around 5,000 lines, either generated or from the runtime.

C. Observations on the simulations

With our provided code, the simulators can run in "automatic" mode. Using this feature, we can execute the models without any further preparation. We ran the simulations many times. In most runs, the platoon behaved as expected, however, a few runs exhibited two unexpected behaviors. Figure 3 is a screen-shot of the GUI view which displays the state for platoon1. It was taken after the system deadlocked. In this case, we can not find a value for the parameter npv of the event nth_move to satisfy the guard forw and the guard safe at the same time, therefore no event can be fired.

Figure 4 shows another interesting behavior. It is a screenshot of the graphical display of the state which shows the vehicles on the plane. We can see that the vehicles do not look like a platoon anymore. There is no requirement on the maximum distance between two vehicles in the models.

Whether those two behaviors should be considered wrong or not is left to the hypothetical stakeholder who ordered the platooning system. The point is that JeB should allow her to make decision on the model: for instance, to add a requirement about the longest distance, and to consider the temporal properties such as the deadlock-freeness at the early stages of the development.

The issue is of course: can we trust our simulations to make such decisions?

V. FIDELITY OF SIMULATIONS JeB allows one to easily build simulators. Once a simulation is set up, the issue becomes whether it is "safe" to use it as an observation tool of the model. This, of course, depends on the kind of usage we want to put simulation in.

Table I.

SYMBOLS AND NOTATIONS

Elements

Event-B JavaScript

machine M P sets s s t constants c c t axioms Axm(s, c) variables v v t invariants Inv(s, c, v) f Inv () events Evts = {E 1 , E 2 , ..., E m } f Evts = { f E 1 , f E 2 , ... f E m } initialization event E 0 , E 0 / ∈ Evts f E 0 , f E 0 / ∈ f Evts actions Act E 0 (s, c, v) f E 0 . f Act () before-after predicate BAP E 0 (s, c, v ′ ) a particular event E i , E i ∈ Evts f E i , f E i ∈ f Evts parameters x E i x t E i guards Grd E i (x E i , s, c, v) f E i . f Grd (x t E i ) actions Act E i (x E i , s, c, v) f E i . f Act (x t E i ) before-after predicate BAP E i (x E i , s, c, v, v ′ ) interpretation function bool eval boolean values T RUE FALSE true f alse equal operator = == substitution x := y x t = y t event occurrences e j , e j ∈ {E 0 } ∪ Evts f e j , f e j ∈ { f E 0 } ∪ f Evts
To be used for the validation of models, simulations must guarantee that any behavior of the simulation is a behavior specified in the model. We call this property fidelity of the simulation to the model. Casting this intuition into a formal frame requires us to define behaviors, observations and the relation between the Event-B code and the JavaScript code.

Let M be an Event-B machine, P be a translated JavaScript simulator of M, Table I summarizes the symbols and notations that we use. The prime ( ′ ) notation denotes the state after the substitution. The value of a predicate Ψ after the application of a substitution σ is noted as [σ]Ψ. The superscript ( t ) notation denotes the translated expressions. The dot (.) notation is used to access JavaScript object properties, the semicolon (;) notation represents sequential execution of JavaScript statements.

We make the assumption that the translation of data types, values and expressions from Event-B to JavaScript is correct. Formally, this can be stated as the existence of a total function mapping JavaScript values to Event-B values ( f ∈ V J → V B ) and that the evaluation of the translated predicates produces the same result as the evaluation of the original predicates. Let x be the collection of all free identifiers for predicate Ψ, x t and f Ψ are the translated identifiers and predicate function respectively, x 0 be the given values of x t , then there exists an interpretation function eval, where

eval(x t = x 0 ); eval( f Ψ ()) == true ⇔ bool([x := f (x 0 )]Ψ) = T RUE eval(x t = x 0 ); eval( f Ψ ()) == f alse ⇔ bool([x := f (x 0 )]Ψ) = FALSE
Actually, Event-B syntax and semantics for expressions and predicates have been designed to be close to their programming equivalent. So, the assumption is reasonable.

A. Behaviors

A behavior of a machine M is a finite sequence of events E 0 ; e 1 ; e 2 ; . . . e n such that ∀ j. j ∈ 1..n ⇒ e j ∈ Evts and fis(E 0 ; e 1 ; e 2 ; . . . e n ) ⇔ true where fis is the feasibility predicate of the sequence which is point-wise extension of the feasibility proof obligation for M:

Axm(s, c) ⇒ ∃v ′ • BAP E 0 (s, c, v ′ ) m i=1 Axm(s, c) ∧ Inv(s, c, v) ∧ Grd E i (x E i , s, c, v) ⇒ ∃v ′ • BAP E i (x E i , s, c, v, v ′ )
Traces(M) denotes the set of all behaviors of the machine M.

B. Simulation Traces

A simulation trace is a finite sequence f E 0 (); f e 1 (x f e 1 ); f e 2 (x f e 2 ); . . . ; f e n (x f en )

of event firings such that: n j=1 eval( f e j . f Grd (x f e j )) == true TraceExecutions(P) denotes the set of all simulation traces of the simulator P.

C. Fidelity of a simulation

Let f Trace ∈ f Evts → Evts be the function which relates the JavaScript events with their Event-B counterpart and map be the function which applies its functional arguments to all events in a sequence. The fidelity of the simulator P to the model M is defined as

∀t •t ∈ TraceExecutions(P) ⇒ map(t, f Trace ) ∈ Traces(M)
In practice, we need to relate this definition to actual observations and properties on the code introduced by users.

• Condition 1 (Correct Context Setup): eval(s t = s v ); eval(c t = c v ); eval( f Axm ()) == true ⇒ bool([s, c := f (s v ), f (c v )]Axm(s, c)) = T RUE
where s v and c v are the actual values given to carrier sets and constants.

• Condition 2 (Correct Initialization):

eval(v 0 = f E 0 . f Act ()); eval( f Inv ()) == true ⇒ bool([s, c, v ′ := f (s v ), f (c v ), f (v 0 )]BAP E 0 (s, c, v ′ )) = T RUE∧ bool([s, c, v := f (s v ), f (c v ), f (v 0 )]Inv(s, c, v)) = T RUE
where v 0 is the value of variables v t after initialization.

• Condition 3 (Events' Enabledness): For all events E i j in a simulation trace

eval( f E i . f Grd (x E i j )) == true ⇒ bool([s, c, v, x E i := f (s v ), f (c v ), f (v j ), f (x E i j )]Grd E i (x E i , s, c, v)) = T RUE
where v j is the current value of v t and x E i j the current value of x t E i .

• Condition 4 (Reachable States):

eval(v j+1 = f E i . f Act (x E i j )); eval( f Inv ()) == true ⇒ bool([s, c, v, v ′ , x E i := f (s v ), f (c v ), f (v j ), f (v j+1 ), f (x E i j )] BAP E i (x E i , s, c, v, v ′ )) = T RUE∧ bool([s, c, v := f (s v ), f (c v ), f (v j+1 )]Inv(s, c, v)) = T RUE where v j+1 is the next value of v t , x E i j the current value of x t E i
and f E i a randomly chosen event which satisfies Condition 3.

We can then define the observation theorem: Theorem 1: If the execution of a simulator P satisfies the condition 1, 2, 3 and 4, then the fidelity of the simulation is guaranteed.

The proof is straightforward.

D. Proof Obligations

Assessing the fidelity of a given simulator amounts to discharging a series of proof obligations generated from the user-provided values and code. Some of those POs can be expressed and discharged in Event-B, but others cannot and need to be discharged by classical semantic reasoning on JavaScript programs.

1) Constants

: PO 1 (Valuation of Constants -Event-B): bool([s, c := f (s v ), f (c v )]Axm(s, c)) = T RUE 2) Parameters: PO 2 (Valuation of Events Parameters -Event-B): n j=1 bool([s, c, v, x e j := f (s v ), f (c v ), f (v j ), f (x f e j )]
Grd e j (x e j , s, c, v)) = T RUE 3) Hand-coded Functions: The proof obligations associated with the hand-coded functions provided by the users depend on their role and place. There are four cases. a) Parameter value generators: this kind of functions is just a facility to run the simulation. The values it produces are actually fed to the guard-function of the event; so, since we assume the translation is correct, only legal parameter values will make the guard true. So, the only requirement on parameter generators is that they produce fairly consistent and reasonable values efficiently. b) Predicate in invariant and guard: let f Ψ be a user implementation of a particular predicate Ψ. The basis of the PO is to show that f Ψ is equivalent to a naive translation of Ψ. Discharging such PO requires us to reason at the level of JavaScript programs:

{ f (v 0 ) | v 0 = f act ()} ⊆ {v ′ | BAP act (x E i , s, c, v, v ′ )}
1 , ..., v n •type(v 1 ) ∧ ... ∧ type(v n ) ⇒ Ψ(g, v 1 , ..., v n )
where Ψ contains several application of g. Let g user be the user implementation of g, m ∈ N 1 be the number of occurrences of g in Ψ, l ∈ N 1 be the number of parameters of g, the transformation is sketched in the following algorithm:

Program Prog = for each call to g (i th call, 1 ≤ i ≤ m) for each argument of the call ( j th parameter, 1 ≤ j ≤ l) generate a fresh variable a i j generate instruction a i j = translation of j th argument expression generate a fresh variable for result r i generate r i = g user (a i1 , ..., a il ) translate the typing expressions to f type (v k ) translate the predicate Ψ to f Ψ , replacing each call of g by their corresponding immediate evaluation result r i

The following PO ensures the correcttness of g user :

PO 5 (Uninterpreted Function -JavaScript):

wp(Prog, f Ψ ) ⇒ n k=1 f type (v k )

E. Assumptions

The formal definition of fidelity presented above focused on the original part of our contribution: the safe inclusion of hand-coded elements into a simulation. In designing the POs, we made four assumptions: A1 Event-B values can be represented in JavaScript, A2 Event-B expressions can be translated into an observationally equivalent JavaScript expression, A3 Event-B Abstract Syntax Tree (AST) can be syntactically mapped to library calls, A4 Event-B operational semantic cycle can be implemented into a scheduler in JavaScript.

SETL [START_REF] Schwartz | Programming with sets; an introduction to SETL[END_REF] shows that A1 is reasonable. Existing translators such as B2C [START_REF] Wright | Automatic Generation of C from Event-B[END_REF] and EB2ALL [START_REF] Méry | Automatic Code Generation from Event-B Models[END_REF] show that A2 makes sense.

We have designed and implemented a set library whose APIs cover all Event-B notations, thus establishing the validity of A3. A4 grounds tools such as ProB [START_REF] Leuschel | Automated property verification for large scale B models with ProB[END_REF] and Brama [START_REF] Servat | BRAMA: A New Graphic Animation Tool for B Models[END_REF]. We are confident that the assumptions can be proven. The proof of correctness of the set library and of the translator can be achieved by using standard verification techniques.

VI. CONCLUSION

In this paper, we have shown how to integrate safely userwritten pieces of code into simulations of abstract models in Event-B. Thus, we can validate all refinements in a development. We strongly believe that the inclusion of validation activities into formal refinement-based methods is necessary as it allows developers and stakeholders to assess the progress of the development toward its goal.

Of course, this work is only a first step. It provides us with the foundations for research in several directions. A first direction is technical. It concerns the integration of JeB into the Rodin environment and the improvement of the efficiency of simulations. A second direction is theoretical. It concerns the generation of the POs and their proof which must be automated in some way to become practical. A third direction is methodological. Current formal methods focus mostly on the issue of verification. Refinement is only defined in this respect. How to integrate validation into the refinement process is an open question.

THEN act1 :Figure 1 .

 act11 Figure 1. Initial model of a platooning system

MACHINE

  platoon1 REFINES platoon SEES space VARIABLES pos tpos iveh unmoved INVARIANTS type_tpos: t pos ∈ Vehicles → Plane tpos_safety: ∀v1, v2•v1 = v2 ⇒ dist(t pos(v1) → t pos(v2)) > dmin type_iveh: iveh ∈ 1..card(Vehicles) ։Vehicles type_unmoved: unmoved ∈ P(1..card(Vehicles)) EVENTS INITIALISATION = BEGIN ini_pos: pos :| pos ′ ∈ Vehicles → Plane∧ ∀v1, v2•v1 = v2 ⇒ dist(pos ′ (v1) → pos ′ (v2)) > dmin ini_tpos : t pos :| t pos ′ ∈ Vehicles → Plane∧ ∀v1, v2•v1 = v2 ⇒ dist(t pos ′ (v1) → t pos ′ (v2)) > dmin ini_iveh : iveh :∈ 1..card(Vehicles) ։Vehicles ini_unmoved: unmoved := 1..card(Vehicles) END move = REFINES move WHERE grd1: unmoved = ∅ WITH np: np = t pos THEN act1: pos := t pos act2: unmoved := 1..card(Vehicles) END fst_move = ANY np1 WHERE 1_move: 1 ∈ unmoved to : np1 ∈ Plane forw: dist(np1 → pos(iveh(2))) > dist(pos(iveh(1)) → pos(iveh(2))) safe: ∀i.i ∈ 1..card(Vehicles) ∧ i = 1⇒ dist(t pos(iveh(i)) → np1) > dmin THEN act1: t pos(iveh(1)) := np1 act2: unmoved := unmoved\{1}

THEN act1 :Figure 2 .

 act12 Figure 2. First refinement of the platoon model

$

  cst.Plane = function(x, y) { var obj = {}; obj.x = x; obj.y = y; obj.__proto__ = $cst.Plane.prototype; return obj; }; $cst.Plane.finite = true; $cst.Plane.card = function() { return $B('90000'); }; $cst.Plane.anyMember = function() { return $cst.Plane( $B.UpTo($B('0'), $B('299')).anyMember(), $B.UpTo($B('0'), $B('299')).anyMember() ); }; ...

$

  evt.init.action.a1.assignment = function( $arg ) { $var.pos._value = $B.SetExtension( $B.Pair('Vehicle01',$cst.Plane($B('30'),$B('30'))), $B.Pair('Vehicle02',$cst.Plane($B('20'),$B('20'))), $B.Pair('Vehicle03',$cst.Plane($B('10'),$B('10'))) ); }; $evt.init.action.a2.assignment = function( $arg ) { $var.tpos._value = $var.pos._value; }; $evt.init.action.a3.assignment = function( $arg ) { $var.iveh._value = $B.SetExtension( $B.Pair($B('1'),'Vehicle01'), $B.Pair($B('2'),'Vehicle02'), $B.Pair($B('3'),'Vehicle03') ); };

  var get_np1 = function (eventId) { return $cst.Plane( $B.plus($var.tpos.value.getImage('Vehicle01').x, $B.UpTo($B('-2'), $B('5')).anyMember() ), $B.plus($var.tpos.value.getImage('Vehicle01').y, $B.UpTo($B('-2'), $B('5')).anyMember()) ); }; var get_npv = function (eventId) { var v = $B.functionImage($var.iveh.value, $evt.e3.parameter.v.value); return $cst.Plane( $B.plus($var.tpos.value.getImage(v).x, $B.UpTo($B('-2'), $B('5')).anyMember()), $B.plus($var.tpos.value.getImage(v).y, $B.UpTo($B('-2'), $B('5')).anyMember()) ); };

Figure 3 .Figure 4 .

 34 Figure 3. Deadlocked state (screen-shot)

PO 3 (

 3 Invariant and Guard -JavaScript): eval( f Ψ ()) == true ⇔ bool(Ψ) = T RUE c) Value returned by an action: let f act be an user implementation of a particular action act. The PO ensures that the set of computed values are admissible values: PO 4 (Action -Event-B):

  d) Function defined by properties in a context: this situation requires us to transform each property axiom into a program whose correctness must be established. A property axiom defining the functional constant g has the form ∀v

The simulators can be found at http://dedale.loria.fr/misc/jeb/platoon-hase