Enrique Wulff Barreiro

Enrique Wulff-Barreiro

How to evaluate university performance

The capacity of Library Science to produce knowledge in such an information system as the decision-taking process in scientific policy, is highlighted by the assessment of University teachers research activity, as recently performed in Spain. The social environment of written communication has been stated, noticing the controversy on scholarly productivity concentration and some key concerns in the analysis of citations as quality indicators. Different meanings of the term "quality" are studied and analysis of the relationships within bibliometric indicators and non-bibliometric data has been undertaken. From the investigation of an important information source in research areas, it is advanced the adequacy of dialogue in complex situations where problem solving oriented librarianship work shows defined features of a post-hoc rationalization of events.

Introduction

The American Library Association (ALA) stated in a biannual report, last year, intitled "Less Access to Less Information By and About the U.S. Government" : Since 1982, from the sixteen thousand official publications one out offour has been removed", foreseeing "an acceleration ofthe current tendency to commercialize and private the government information" [START_REF]Less access to less information by and about the U.S. government[END_REF]. The automation of USA University Libraries has provoked that, as the search for information has been increasing its costs, what was public and freely accessible to all sorts ofpeople has became commercialized, and private. On the pages of Science, the journal ofthe American Association for the Advanceraent of Science (AAAS ), one can read: "commercial pressures and heightened competition are testing the notion that scientific data and materials should be widely shared" (25 May 1990) [START_REF] Marshall | Data sharing: a declining ethic?[END_REF]. These is the present-day framework used for the estimation, from bibliographic criteria, ofthe evaluation standards used to measure, in Spain, the research activity ofUniversity teachers as stated in the Governmental Order, 5 february 1990 [START_REF]Orden Ministerial del 5 de febrero de 1990. Resolución 3021[END_REF].

Il.

Data Theodora Hodges, Ph.D. (Library School, South Hall, USA) supplies a certain number of answers from editors of scientific journals to questions on citation practices [4]. The physicist R. Powell (Annual Reviews) says that references are important because they appear in the index ofthe journal; the biologist J.Pettigrew finds that references are a good clue to worthwhile papers, and " especially to whether it's suited to the particular journal in question" . The geneticist M . Lerner (Evolution) pointed out that paper' s references are useful as a quick subject guide; al1d tremendouslv helpful in " picking suitable referees". This last suggestion was rejected by the librarian ofthe California University (Berkeley) R. Dougherty whose opinion is that "references don ' t help in deciding to whorn to send a paper for refereering". M . Protter"s (Bulletin ofthe American Mathematical Societv) opinion is that, occasionally, there ' s a celiain editorial correspondence on references as when is asked if an author knows about a certain paper. Ironically in regard to written communication, physicist Emilio Segré (Annual Review ofNuclear Science) emphasizes that in Italy clarity, the main concern of an annual scientific journal editor, is more extensively implanted because all student examinations are oral! Bensman [START_REF] Sj | Bibliometric laws and library usage as social phenomena[END_REF] mentions the case of Sharon Johnson, a biochemist who was denied tenure at the University of Pittsburgh and charged sex discrimination. R.E. Davies, Benjamin Franklin Professor of Molecular Biology at the University ofPennsylvania, J.S . de Cani, chairman ofthe Department of Statistics at the same University, and N .L. Geller, an assistant professor in the latter Department, relying on the suppoli ofDerek J. de Solla Price, used Science Citation Index [6] data to construct a mathematical model, and with it they demonstrated that Johnsonls citation rates were significantly higher than those oftwo men in her Department who had been promoted and given tenure. Nevertheless, the usage of citation frequency as a scientific quality indicator is liable to controversy. Sornetirnes, scientific establishment has openly showed its hostile objections against citation analysis believing it to be a certain evaluation of the work they do, undertaken by people outside the specific discipline and whose biasided results are suspected to produce a radical redistribution of scientific resources. In this regard, data from Hagstrom are wOlihwhile when he comments that in a survey of scientists (mostly biologists and med ical) 72 per cent of more than three hundred answered "always" to the question "In scientific or other professional papers about work to which you have made some contribution, is proper credit given to your own contribution by means of authorship or acknowJedgement?" [START_REF] Hagstrom | The scientific community[END_REF]. In the case Johnson v. University ofPittsburgh, the results aboye mentioned drew such descriptions as "premature", "a product of methods whose reliability in individual cases has not been shown", or "frightening". Much of this criticism has focused on the nature of citations; CoJe & Cole who deveJoped a techl1ique of weighting citations -note that avaiJable data suggest the use of citation counts as reasonably reliable indicators of the qualíty or the ímpact of a scientific research, and they don 't consider citations as a measure of the absolute quality of work, emphasizing current citations as an adequate measure of the quality ofwork socially defined.

III. Quantity and quality of scientific production

It must be noted that the measures of association between productivity -the total of each scientistls count ofpapers produced in the preceding three years -and other variables, according to Hagstrom (who considered publications as the most important component when determining the prestige of an University Department), have to be cautiously [START_REF] Hagstrom | The scientific community[END_REF]. Defining the impact factor, with Narin & Moll, as the average nllmber of citations received by an atticle during a specified period [START_REF] Narin | [END_REF]; the usage of the instruments of science, objectives and qllantitatives as they are, with regard to itself, has provoked strong criticisms that talk about 'num berology' -, nevetthe less, it isn't a case of m isticism but of numeric sciences showing LIS tl1at there would be a significant correlation between qualitative solidity and quantitative solid ity [START_REF] Solla | Little science, big science[END_REF]. The misunderstand ing takes the form of supposing an empirical finding that the el ite in a research context (books, papers, reports statements, studies) -or anywhere else -, as measured by reasonable standards of quality or utílity, represents some fixed proportion ofthe total population [START_REF] Solla | Some remarks on elitism in information and the invisible college phenomenon in science[END_REF]. It would be necessary, to have a through knowledge of the context in which a citation is done, to take advantage ofwritten communication condition as a process of social communication of information, what leads to the use of inductive impact models [START_REF] Le Coadic | Modelling the communication, distribution, transmission or transfer of scientific information[END_REF] , thus suggesting the call in question of the 'transmission' notion.

Moravcsik and Murugesan, with a content analysis of citation requiring the reading of the primary source text, settled a citation tipology ofthe contexts in which references are made [14], that Chubin & Moitra used to compared the results thus obtained with respect to the counts made by scr, searching "to clarify the status of citation counts as a measure of quality or impact in science" [START_REF] Chubin | Content analysis of references: adjunct or alternative to citation counting?[END_REF], with confirmatory outcomes.

IV. Communication in science and quality assessment

Quality assessment is an action-oriented option, it consists of information suppLied to be helpful in solving evaluation problems in communication processes. In value-added terms, a great quantity of value would be added to the considered information units [START_REF] Neill | The information analyst as a quality filter in the scientific communication process[END_REF]. The term quality would be considered with two meanings: internar quality of a work or estimation of its scientific value, and new ideas or "new knowledge" or innovation the work implies 116]. For example, to consider a patent as a kind of "new idea" would give, in I&D, an indication ofthe relationship between quality and quantity by correlation of the growth rate the amount of patents presents and the scientific and technicalliteratura growth [START_REF] Neill | The information analyst as a quality filter in the scientific communication process[END_REF].

When the evaluative work on research quality in academic milieu draws from expert panels, the elite scientific peers, it has been demonstrated that two different components are invoJved, the number of publications and the "influence per paper" (according to the influence methodology developed by Computer Horizons Inc. (CHI), that puts quality in terms ofweighted citation counts, with weights based on the prestige of the citing journals (determined by interactions [START_REF] Anderson | Publication ratings versus peer ratings of universities[END_REF]). The objectivity of this quality filtering is dubious because, it has been presumed, the global prestige of a University influences the ratings of its own Departments. Otherwise, the use of citation analysis as an instrument for the evaluation of research quality has been criticized as a simple visibility indicator (a conseqllence of personality, reputation, author's position in the social academic structure; the Coles places the awards visibility as a function ofthe nllmber ofrecipients, scope, money, quality ofwork ofrecipients, being these factors of diverse degrees of relevance [START_REF] Cole | Social stratification in science[END_REF]), a function of the pllblication with minimal possibilitíes as a measure ofthe research prodllction.

The comparison between expert jlldgements and bibliometr indicators in order to evaluate the research performance provides, in the case ofthe pharniacelltical industry -where marketed drllgs suppose a simple and objective ofthe approval pharmaceutical innovation -, enlightened suggestions [START_REF] Koening | Bibliometric indicators versus expert opinion in assessing research performance[END_REF]. By compiling the citation data from Science Citation Index, by scoring the specific productivity rates ofthe pbarmaceutical companies, and by sending questionnaires to a panel of experts (in regard to the criteria of creativity, contribution, commercialization and basic research), the conclllsións points to support the fact that bibliometric indicators are as good, if not probably better, as expert judgements when predicting research performance.

Anyone who undertakes the evaluation of the validity of a specific work and who is not used to decide what should be published or who should be promoted is in the correct place, at least in what concerns industrial and scientific research, to carry it out with precision. The information analyst, who is present in the emergent market for information specialists [START_REF] Moore | The employment market for librarians and information specialists in the United Kingdom[END_REF], going beyond the labour of provision of state-of-the-ali summaries relevant to the work of the research team to which he belongs, could identify publications as being methodologically valid and also as containing new knowledge. This way another quality filter would be added to the information system.

V. University Research: Statistical evaluation

The display ofthe relationships between short-term impact (operationalized in citation counts) and the visibility of the research groups at the research front, when it's based on a definition of scientific quality incluiding the degree to which researchers successfully perform "public relations" activities (such as awards, internacional contacts, invitations to take part in important conferences) as well as the basic quality in its triple meaning cognitive quality (importance of the specific content of scientific ideas), methodologically quality (accuracy ofmethods and techniques current in a particular scientific field) and aesthetic qual ity (the controversias question of the attractiveness of mathematical formulation models) sllpposes, at least, two d ifferent kind of results [START_REF] Moed | The use ofbibliometric data for the measurement ofUniversity research performance[END_REF].

An approximation to the real influence ofthe research activity on its specific surroundings, meaning by this that the research peers do have the opportunity of consider the basic quality of that research, starts by choosing the adequate unit of research activity, a question that determines the relevance of prodllctivity and impact analysis in what concerns university research policy.

The use of Journal Citation Report (JCR) by ISI (Philadelphia) in order to construct average counts of citations received by all the papers published in the jOllrnals where a research group publishes, for a comparative interpretation with the "actual" number of citations per publication a research group receives, complemented byan indication of the impact levels that present the journals in which the group has pllblished, is a procedure that, by judging optimal tITe research group as an unity, was intended to nelltralize the disturbing factors (such as, a mechanical interpretation -in impact terms -ofthe differences between citation counts for groups working in different fields, a change in citation practices into the own fields, ISI diverse editorial actitudes) that would reduce, otherwise, the validity of bibliometric indicators in that for which they were devised [START_REF] Moed | The use ofbibliometric data for the measurement ofUniversity research performance[END_REF]. Now, the actual utility as a guide in what concerns the relative quality of scientific journais supposed to the impact factor (according to 1SI) has became so dubiollS that it has been considered an uninformative derivation measure ofthe uncorrected citation rate (when searching to determina the qllalitative effect ofthe journal on formal communication in science), as in the case of visibility index [START_REF] Ch | A statistica1 assessment oftwo measures ofcitation: the impact factor and the ímmediacy index[END_REF] .

It's derived from these viewpoints that both the circumstances and the conditions in which the publication of the journals and the intellectual reception of its contents are realised, are constituent palts of the citation rates the journals receive. The combination of bibliometric data and non-bibliometric data (i.e., for example institutional data), the valuation ofthe visibility's influence underlying impact factor and thus the estimation of impact factor as a relevant aspect from which investigate the intensity employed by researchers in order to make their results known to colleages, provide a meaningful basis for a dialogue between research policymakers and the researchers ofvarious University groups in order to interpret the bibliometric results as relevant factors to policy.

VI.Qualitative study: impact factor and quality. The journal 'Science'.

To pose that the alTIount of citations received by a pllblication cOllld be a val id representation of its utility for readers (scientific colleagues), as well as half a century ago, based on the idea that it's a common thing to rely on previously published papers when writing an article [22]. Let's consider 'Science', a major information source, specific to research fields, from which scientists elaborate its reference lists, and let's study thisjournal, between 1980 and 1988, in order to reveal the possible relationship between quantitative indicators and the quality of the scientific contents. The research results available to the internacional scientific commllnity via scientific jOllrnals compete with each other this way, using utility as their pretext. In this 'intersubjective' order the position attained by a published scientific work outlines the strength with which an infonnation unit shifts usable knowledge in the research milieu. Studies concerning 'Science', starting from tbe evaluation of27.892 cítations between 1978-83 received by the 1.639 pllblications issued in 1978, show that, the initial utility of a specific publication decreases by "absorption" of (parts of) this initial usefulness as a result ofthe mechanisms of competition [START_REF] Van Raan | Impact ofresearch performance as measured by citations: a new model[END_REF]. This judgement ofusefulness, collectively established by the scientific community, seems to be well representad by the amount of received citations, a process similar, in this respect, with political elections (in the European political system, for example).

From data in the Table below, it could be considered that the annual citation rate (number of bibliographic citations obtained per citable paper and year) drops because the annual relative increase (positive) ofthe amount of bibliographic citations the journal receives -i.e. BC, Bibliographic Citations is less than the rise ofthe total sum ofthe papers published in the period under consideration (citable papers, ART); in its turn, the impact factor (ISI) rises, reaching more than its double [24]. Consequently, as the two numeric computes don't present convergence, and when the reasons for this fact are pursued, the visibility effects which inf1uence the impact factor point out to the non-bibliometric data. !t's possible that the number of subscribers -160.000 -, the amount of databases collecting the papers the jOllrnal publishes -39 -, and the figure of SDI services disseminating them, are all relevant aspects to this proved inflllence [START_REF] Egghe | Introduction to informetrics[END_REF] . The amount of annually pllblished papers during 1980-88 shows a decreasing tendency, of course dlle to the conception of the editorial product. It may be that, in the case ofthe journal under analysis, this decision seekes to avoid a situation of saturated demando

VII. Starting from iII-defilled problems

It's possible that the introduction of a change in a management information system like the decision taking process in scientific policy as a result ofthe evaluation ofthe research activity may have to be accompanied by the need of making use of a process of negotiation, consultation, and confrontation with which a change agent is faced in an organizational setting. The problem-solving management perspectiva becomes necessary in order to understand the more political concerns in an organization, itls an specially relevant approach when problems are ill defined [START_REF] Lj | Designing from ill-defined problems[END_REF].

The political model of an information system in its organizational aspects is not adapted to make from it simplist inferences, otherwise it emphasizes that the organizational contexts are complex situations. one question thar makes the work enormously complicated consists in that those who design the information system are entangled, during the process, in the informal system (as opposed to the functional model of the organization, the formal system). To pay attention to the bibliometric data as an impol1ant base for dialogue, in a problem solving negotiation process, includes to pay attention to non bibliometric data issued from the organizational context ofthe research. It's not a strange activity to those tbat have introduced tbe idea of service studies, of empirical studies aimed to make a service better, thus proposing a positive and empiricval model of science in Librarianship [START_REF] Brooks | The model of science and scientific models in Librarianship[END_REF].

Tbe defence of value statements in written communication studies have an already prolonged tradition, possibly of little usefulness in order to produce knowledge. Arguments of this sort confronted on tlle question of running modern academic libraries, tbose tbat would recommend the professional library work to scholars/librarians and those who would let it to a business manager/chief librarian [START_REF] Brooks | The model of science and scientific models in Librarianship[END_REF]. The presumed refutation, on the basis ofthe status quo defence, (incluiding an elaborated model), ofthe empirical data on circulation of library materials in academic libraries presentes by a study ofthe University of Pittsburgh, points out an invalidating action with no relationship to knowledge production but rather with simple personal opinions [START_REF] Brooks | The model of science and scientific models in Librarianship[END_REF].

VIII. Final Report

Norbert Wiener, father of the Cybernetics, cautionsagainst the danger of wasting the notions derived from information due to a mercantile attitude in its concern [START_REF] Wiener | The human use of human beings: Cybernetics and society[END_REF]. Perhaps this kind of factors could be checked on the excluding choice of certain pinpointed international criteria for evaluation of the publications quality. It must not be forgotten that, recently, a prestigious research business, like Unión Musical Española, has not only didn't follow an information technical dissemination process through a musical documentation centre (at the INAEM, Spanish national institute for dramatic and musical arts), but also has it succumbed to an uncontrolled selling dynamics, with tones being destroyer as old paper [START_REF] Gallego | [END_REF].

x


Andrea Cozza
email: andrea.cozza@centralesupelec.fr

Florian Monsef

Wavefront Synthesis in a Reverberation Chamber: Experimental Results

The TREC recipe in a nutshell: a) a weakly lossy diffusive environment (e.g., a reverberation chamber), b) a single source, with no special features and c) a scanning system for sampling Green's functions over a surface.

Observations: a) stable wavefronts against translation and rotation, b) good level of contrast (> 20 dB), c) good polarization control.

Applications : a promising application currently developed is imaging coupling paths in metallic shields. An example is shown below.

Fig. 1 :Fig. 2 :Fig. 3 :

 123 Fig. 1 : The robot optimized to weakly perturbate a reverberation chamber in the GHz range. On the right, a detail showing the electro-optic probe.

Fig. 4 :

 4 Fig. 4 : A transmission image of a slotted metal box, showing the position of a slot and its sensitivity to polarization. Moving focal spots were used in order to generate it.


Philippe Ayrault
email: philippe.ayrault@etersafe.com

Thérèse Hardin

François Pessaux

Franc ¸ois Pessaux

Development of a Generic Voter under FoCal

Keywords: formal methods, development cycle, voter, FoCaL

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

Introduction

Development of safety related systems has to be strictly compliant with applicable standards. This is required by any safety authority before commissioning of a system. Safety demonstration is greatly helped by using a formally based framework to express requirements, design, code and to ensure that this code meets specification requirements. Unfortunately, this is not sufficient. Safety authorities also require an independent verification process which must follow the different stages of a strict development cycle. Thus, any tool claiming to be dedicated to formal developments should not only provide a formal paradigm to model and prove the system but must also strongly support a well defined development cycle and must produce adequate documentation at each stage of the development. Moreover, such a tool should help to identify impacts of modifications during the whole life of the system (frequently more than 20 years). The purpose of the FoCaL tool is to bring some answers to this problem area. FoCaL provides a unified language to express requirements (declaration and properties) as well as source code and proofs while only using concepts largely accessible to engineers.

In [START_REF] Ayrault | Development life cycle of critical software under FoCaL[END_REF], we introduced a safety development cycle customised for FoCaL. Our problem now is to study its feasibility and to understand how practically FoCaL can help to answer safety and good practise requirements. We have chosen to fully treat the example of a voter. Indeed a voter is a central equipment of all redundant architectures, widely used for safety related systems. A voter is a process or a device whereby a number of similar signals are monitored for discrepancies and are voted upon to obtain the selected output which is most probably correct. It is highly safety critical because in many cases, the voter is the last barrier able to eliminate failure effects and answers a part of the safety principles underlining the whole system. As these ones strongly depend of the aim and domain of the system, for the re-usability sake, a voter should be conceived as a very generic equipment. Thus choosing a voter seems a good balance between the exemplary nature of the development and the length of the paper.

The rest of the paper is organised as follows. We present the main features of the FoCaL tool in Section 2. Section 3 exposes the rules of a voter and its textual specification. The Section 4 comments the development of the voter using the FoCaL tool. We conclude and comment possible further works in Section 5.

The FoCaL environment

We give here an informal presentation of near all FoCaL features, to help further reading of this paper. For more details and the new release 3 .

The Basic Brick

The primitive entity of a FoCaL development is the species. Like in most modular systems (i.e. objected oriented, algebraic abstract types), it can be viewed as a record grouping a data structure with its related operations. Since FoCaL does not only address data type and operations, species may contain the declarations (specifications) of these operations, some properties (which may represent requirements) and their proofs. All these components of a species are called methods and we briefly describe them.

-The method introduced by the keyword representation gives the data representation of entities manipulated by the species. It is defined by a type expression, which is roughly a ML-like pure type (with restricted polymorphism). The representation may be not-yet-defined in a species, meaning that the real structure of the data-type the species embeds does not need to be known at this point. However, to obtain an implementation, the representation has to be defined later either explicitly or by inheritance. -Declarations (keyword signature followed by a name and a type) introduce methods to be defined later: they only specify types without implementation yet. Declarations serve to express specifications, properties. Thanks to late-binding, as soon as a name is declared, it can be used in definitions. -Definitions (keyword let, followed by a name, a type and an expression) introduce constants or functions, i.e. computational operations. The expressions are roughly pure ML-like expressions with an auxiliary construction (S!m) to call the method m from a given species S. -Statements (keyword property followed by a name and a first-order formula) may serve to express requirements (i.e. facts that the system must hold to conform to the Statement of Work) and then can be viewed as a specification purpose method, like signatures were for let-methods. They entail a proof obligation later in the development. Like signatures, even if no proof is yet given, the name of the property can be used to prove other theorems or lemmas.

-Theorems (theorem) made of a name, a statement and a proof are properties together with the formal proof that their statement holds in the context of the species. This proof will be processed by FoCaL and ultimately checked with the theorem prover Coq.

In addition, FoCaL provides a powerful mechanism for documentation by allowing special kind of commentaries (called annotations) kept along the compiler process.

Type of Species, Interfaces and Collections

The type of a species is obtained by removing definitions and proofs. Thus, it is a kind of record type, made of all the method types of the species. If the representation is still a type variable say α, then the species type is prefixed with an existential binder ∃α. This binder will be eliminated as soon as the representation will be instantiated (defined) and must be eliminated to obtain executable code. Species types remain totally implicit to users and serve only to introduce interfaces.

The interface of a species is obtained by abstracting the representation type in the species type and this abstraction, which hides the representation, is permanent. Interfaces play an important role. They are simply denoted by the species name. Interfaces can be ordered by inclusion, a point providing a very simple notion of sub-typing.

A species is said to be complete if all declarations have received definitions and all properties have received proofs. When complete, a species can be submitted to an abstraction process of its representation to create a collection. Thus the interface of the collection is just the interface of the complete species underlying it. A collection can hence be seen as an abstract data-type, only usable through the methods of its interface, but with the guarantee that all methods/theorems are defined/proved.

Combining Bricks

A FoCaL development is organised as a hierarchy which may have several roots. Usually the upper levels of the hierarchy are built during the specification stage while the lower ones correspond to implementation. Each node of the hierarchy, i.e. each species (or collection as terminal ends), is a progress to a complete implementation. There are two ways to build new species from previously built species: inheritance and parametrisation.

In FoCaL inheritance serves two kinds of evolutions, which can be freely mixed. One may create a new species by extending the inherited ones with new operations and properties while keeping those of the inherited ones (or redefining some of them). One may create a new species by giving explicit definitions to signatures and proofs to properties of the inherited species, to be closer to a "executable" implementation.

Multiple inheritance is available in FoCaL. In case of inheriting a method from several parents, the order of parents in the inherits clause serves to determine the chosen method.

The type of a species built using inheritance is defined like for other species, the methods types retained inside it being those of the methods present in the species after inheritance is resolved.

A strong constraint in inheritance is that the type of inherited, and/or redefined methods must not change. This is required to ensure logical consistency of the FoCaL model.

FoCaL allows two flavors of parametrisation: parametrisation by collection parameters and parametrisation by entity parameters. For instance a pair is a structure which is built upon its two components and is described by a species parametrised by its two components. Entity parameters are not introduced as we do not use them within this paper.

The parametrised species can use collection parameters' methods to define its own ones. A collection parameter is given a name C and an interface I. The name C serves to call the methods of C which figure in I. C can be instantiated by an effective parameter CE of interface IE. CE is a collection and its interface IE must contain I. Note that species (without abstraction) are not allowed as parameters. Indeed, if an incomplete species were used as an effective parameter run-time error due to linkage of libraries can occur and properties stated in I can not be safely used as an hypothesis. In contrast, the collection and late-binding mechanisms ensure that all methods appearing in I are indeed implemented in CE.

The Final Brick

As briefly introduced, a species needs to be complete to lead to executable code for its functions and checkable proofs for its theorems and then, can be turned into a collection. Hence, a collection represents the final stage of the inheritance tree of a species and leads to an effective data representation with executable functions processing it. As said before, to ensure modularity and abstraction, the representation of a collection turns hidden. This means that any software component dealing with a collection will only be able to manipulate it through the operations (methods) its interface provides. This point is especially important since it prevents other software components from possibly breaking invariants required by the internals of the collection.

Properties, Theorems and Proofs

FoCaL intends to encompass both the executable model (i.e. program) and properties this model must satisfy. For this reason, theorems, properties and proofs are methods dealing with logical instead of purely behavioural aspects of the system. Stating a property entails that a proof of it will be finally built. For theorems, the proof is directly embedded in the theorem. The compilation process submits proofs to the formal proof assistant Coq which automatically checks that they are consistent.

No syntax is offered to express high-order properties as they are rather difficult to manage by engineers not experts in logic theory. But special instances for induction and termination proofs are to be provided.

Proofs are done by the developer as follows. It can be written in "FoCaLProof Language", a hierarchical proof language that allows to give hints and directions for a proof. This script is submitted to an external theorem prover, Zenon4 developed by D. Doligez. Zenon is a first order theorem prover based on the Tableaux method incorporating implementation novelties such as sharing [START_REF] Bonichon | An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF]. From these hints Zenon attempts to automatically generate a proof and if it succeeds, expresses its proof as a Coq term verified by Coq during the compilation process. Basic hints given by the developer to Zenon are: "prove by definition of a method" (i.e. looking inside its body) and "prove by property" (i.e. using the logical statement of a theorem or property". Surrounding this hints mechanism, the language allows to build the proof by stating assumptions (that must obviously be demonstrated next) which can be used to prove lemmas or parts for the whole property. We show below an example of such a demonstration.

theorem order_inf_is_infimum: all x y i in Self, !order_inf(i, x) -> !order_inf(i, y) -> !order_inf(i, !inf(x, y)) proof:
<1>1 assume x in Self, assume y in Self, assume i in Self, assume H1: !order_inf(i, x), assume H2: !order_inf(i, y), Like any automatic theorem prover, Zenon may fail finding a demonstration. In this case, FoCaL allows to write verbatim Coq proofs. The compiler provides a Coq script "with a hole" which can be filled with the proof done by hand, then imported back to the FoCaL source code as verbatim Coq code.

prove !order_inf(i, !inf(x, y)) <2>1 prove !equal(i, !inf(!inf(i, x),
Finally, the assumed keyword is the ultimate proof backdoor, telling that no proof is given thus the property is considered as an axiom. Obviously, a really safe development should not make usage of such "proofs" since they bypass the formal verification of software's model and can break the global consistency. However, a development may use external (trusted or not) code no property of which can be proved. Moreover, whatever the reason, the user may choose to admit some properties. But any "assumed" lemma should always be at least receive a textual justification inside an annotation. A good practise is to submit such lemma to the FoCaL test tool to increase confidence.

Around the Language

All along the development cycle of a FoCaL program, the compiler keeps track of dependencies between species, their methods, the proofs, . . . to ensure any modification of component will be detected and its impact will be reported on those depending of it.

FoCaL considers two types of dependencies: -The decl-dependency: a method A decl-depends on a method B if the declaration of B is required to express A. -The def-dependency: a method (and more especially a theorem) A def-depends on a method B if the definition of B is required to state A (and more especially, to prove the property stated by the theorem A).

The redefinition of a function may invalidate the proofs that use properties of the body of the redefined function. All the proofs which truly depend on the definition are then erased by the compiler and must be done again in the context updated with the new definition. Hence an important point is the choice of the most interesting level in the hierarchy where to write a proof.

FoCaL currently supports two target languages: OCaml [START_REF] Leroy | The Objective Caml system, documentation and user manual[END_REF] and Coq [START_REF] Bertot | Coq'Art: The Calculus of Inductive Constructions[END_REF]. Code generation towards OCaml allows to build an executable: all the logical aspects are discarded since they can't be expressed in this language and don't lead to executable code. Code generation towards Coq provides a formal model of the program, including computational and logical aspects: all computational methods and logical methods with their proofs are compiled. Thus the consistence of the whole FoCaL development can be checked by Coq.

However the compilation model (i.e. the structure of a collection, of a species, of a method) remains very simple. It is the same in both target languages and uses a few set of basic constructs: records (i.e. structures), functions and simple modules (not even functors).

Note that references are not currently allowed as it is not so easy to handle memory management at the proof level. However functional views of memory are used in several developments. We currently consider to add data-flow programming features and their logical counterparts to ease reactive systems development.

The tool called FOCDOC [START_REF] Maarek | FoCDoC: the documentation system of FoC[END_REF] automatically generates documentation, ensuring that the documentation of a component is always consistent with respect to its implementation. This tool uses its own XML format that contains information coming not only from structured comments (that are parsed and kept in the program's abstract syntax tree) and FoCaL concrete syntax but also from type inference and dependence analysis. From this XML representation and thanks to some XSLT style-sheets, it is possible to generate HTML or L A T E X files. In the same way, it is possible to produce UML models [START_REF] Delahaye | Producing UML Models from Focal Specifications: An Application to Airport Security Regulations[END_REF] as means to provide a graphical documentation (class diagrams) for FoCaL specifications. The use of graphical notations appears quite useful when interacting with end-users, as these tend to be more intuitive and easier to grasp than their formal (or textual) counterparts. This transformation is based on a formal scheme and captures every aspect of the FoCaL language, so that it has been possible to prove the soundness of this transformation (semantic preservation).

Although this documentation is not the complete safety case, it can helpfully contribute to its elaboration.

As a conclusion of this presentation, FoCaL is not at all a "All-in-One" language, it helps to define strict boundaries between phases of a development. Consistency between phases is ensured by a powerful dependency calculus and a proof system. FoCaL user is guided to maintain the global consistency of a complete development, even during the maintenance phase.

There exist several systems and languages having the same purposes like B [START_REF]The B-Book -Assigning Programs to meanings[END_REF], CASL [START_REF] Astesiano | CASL: the Common Algebraic Specification Language[END_REF], RAISE [START_REF] The | The RAISE Development Method[END_REF]. . . True comparison with these systems is out of the scope of this paper (but is considered in a forthcoming paper). It seems to us that the originality of FoCaL is its unified language along the different phases which allows to provide the assessor a complete package built in conformity with the related standards.

Differently from CASL [START_REF] Astesiano | CASL: the Common Algebraic Specification Language[END_REF] that is strongly oriented towards ADT, hence without effective representation of data and computation, FoCaL lets the user go until speci-fying them (and adds an abstraction layer to prevent users from having access to internal effective implementation). FoCaL produces executable code and related proofs whereas CASL emphasises on the specification phase despite the fact that institutions are provided to link specifications to some SML or Java code [START_REF] Aspinall | From specification to code in CASL[END_REF]. RAISE [START_REF] The | The RAISE Development Method[END_REF] provides a large range of specification and programming concepts. In contrast, FoCaL offers a limited set of concepts but they can be altogether translated to Coq to ensure a global consistency of the whole development.

FoCaL development cycle

As recalled in the introduction, the development of a critical system must follow a strict development cycle, compliant with standards. In [START_REF] Ayrault | Development life cycle of critical software under FoCaL[END_REF] we proposed a development life cycle taking advantages of all features of FoCaL and compliant with the main Standards in the field of critical software development ( [START_REF]Railway Applications -Communications, Signalling and Processing Systems -Software for Railway Control and Protection Systems[END_REF], [START_REF]Functional safety of electrical/electronic/programmable electronic safety-related systems[END_REF],...). It is based on a V-cycle, decomposed into five (mandatory) phases: requirements/specification, architecture/design, implementation and low level testing, integration/validation testing and the longest one, the maintenance phase. It also covers some transverse processes like generation of the documentation or formal traceability between phases. Transverse processes are processes that should be applied once during all phases. The main characteristics of this life cycle are :

a strong boundary between phases, especially between the specification phase and the architecture/design one. Specification phase ends when all safety requirements can be proved using the functional requirements and the glue assumptions (see below). Architecture/design phase ends with the implementation of the functional requirements into executable code. the implementation phase consists in assembling collections and proving the glue assumptions made on the parametrised species. the use of the FoCaL dependencies calculus and documentation generation to generate formal traceability and to help maintenance.

In this paper, we mainly focus on requirements specification, architecture/design and implementation phases as we build the voter. Integration/validation testing phase is considered in the work of M. Carlier [START_REF] Carlier | Functional Testing in the Focal environment[END_REF].

The development cycle is strongly based on the establishment of the specification through requirements expression. We distinguish four kinds of requirements:

-Functional requirements describe the relations between inputs and outputs of the system and what is expected on the behaviour of the system without referring to any specific solution. -Non-functional requirements describe all constraints that the system must meet, like time and space bounds, safety integrity levels to achieve, portability needs. . . These requirements are pretty difficult to express by a first-order formula. They are put inside annotations, so are kept along the compilation process and figure in the compiled documentation. -Safety requirements coming from the results of the safety studies. They ensure that the functional requirements will never trigger a Feared Event. They are considered as requirements on functional requirements.

-As a species can be parametrised, proofs of functional and/or safety requirements sometimes need assumptions on the functions and properties of the collection parameters. These assumptions are called glue assumptions. They are proved at the coding level just before final building of the whole system.

All the requirements but some non-functional ones are expressed as FoCaL properties.

Overview of the voter

Generic definition

Sensors may exhibit various kinds of errors like bias offset, scale factor or transient faults due to sensitivity to spurious or environmental factors (temperature, pressure,. . . ). Redundancy is one of the major techniques used to guard safety critical systems against such transient faults. There exists many kinds of redundancy, depending on which characteristics (safety, reliability or both) should be privileged for the system. Roughly speaking, each redundant component performs the same work and, when one of them fails, the voter has to detect it and to select an output value among the other, then has to go on providing the service.

Usually, a voter is used to elaborate the output from the input values given by the redundant components. Voters are used, for example, for temperature acquisition by multiple sensors in a boiler, or elaboration of the emergency brake signal of a train from several computer replicas. . . The basic principle of a voter is to compare its input values according to a given consistency relation, and then to output one value depending on a voting policy. The point is that, in redundant systems, the voter is the component that must be perfect (as far as possible obviously). A failure of the voter is considered as a major weakness of the system.

A voter system must fulfil three main requirements:

reliable and correct choice of one non faulty input among its n inputs5 detection of errors on inputs localisation of the source of the error and report of a diagnosis related to it 6The elaboration of the output value follows a two-stages process:

1. the inputs comparison, which takes 2 or more inputs and compares them according to a "consistency law". There are many kinds of such consistency laws: strict equality, equality within a certain tolerance, most recent input, max or min values . . . 2. the arbitration, by a voting policy algorithm which produces the output value. This algorithm is the heart of a voter and determines its classification and its main properties (majority vote, selection of the most restrictive vote, selection of the most recent value . . . ).

A pre-processing of the inputs can also be performed by a filtering process. It analyses input values by in-line "acceptance tests" and eliminates values recognised wrong, a way to eliminate some transient faults. The inputs that succeed the filtering process are then sent to the voter 7 .

In the following, we focus on voters with 3 inputs. Our choice is motivated by the fact that 3 inputs is the minimal number for a voter to deal both with safety and reliability characteristics. Taking the case where agreement between 2 sensors is sufficient to ensure the required safety level of a system. Using a voter with 2 inputs meets the safety requirements. But, in case of one failure on a sensor, you need to stop or run your application in a degraded mode. Adding a third sensor permits to continue the service in case of one fault. Most of the time, the cost of the third sensor is far less than the unavailability of the whole system. This kind of voter is a widespread voter architecture in safety critical systems (i.e. Triple Modular Redundancy).

Our choice could be even more generic. It is indeed possible to specify an "n out of m" voter and then to instantiate n and m with the needed value. But this solution needs to highly complicate the voter specification and implementation for a small added value. Indeed only some n and m values are generally used; 1oo2 for reliability, 2oo2 for safety, 2oo3 or 2oo4 for safety and reliability and the concerns are so different that this "sharing by genericity" is just useless.

The 2oo3 voter specification

The 2oo3 voter, used for our example, selects one value from three independent inputs if at least two of them are consistent. Moreover, we also want to detect the faulty value. So, a second output is added to the voter in order to qualify the first result. Table 1 summarises all cases, described as follows:

-perfect match: the three inputs are consistent, the value and index of one of them are returned. -partial match: two of the three inputs are consistent together, but the third one is not. One of the consistent values and the index of the inconsistent one are returned. This enables identifying a failure on this input. -range match: One input is consistent with the two others which are mutually inconsistent. The consistent value and the associated index are returned. This can arise when the consistency law is not transitive (i.e. equality within a tolerance). In this case, the system can go on working with the most plausible value. -no match: all the inputs are inconsistent two per two. The voter cannot take a decision since the majority rule is not applicable.

The specification of the no match case seems, at first sight, satisfactory: no value is output as there is no good candidate. At the specification level, this behaviour is acceptable, but a choice has to be made during the design phase: the component connected to the voter is waiting for two values (the index of the component and the flag). It will be its own concern to decide what to do with the first output, according to the second.

Another safety requirement allocated to a voter is that the output value is always one of the inputs. The voter specification closely follows the description given in Section 3. Indeed separation of the voting policy and the inputs management eases reuse and independent evolution of parts of the voter. The whole specification of the voter is thus split into two major parts. The part concerning the voting policy is introduced by the species Voter (see fig. 1) which specifies the voting policy algorithm and the glue assumptions made on the inputs of the voter, represented by parameters. The second part, which concerns values, is itself split into two parts, the first one describing what is supposed/needed on the "basic" types (like naturals, integers, booleans) and functions on them, the second one (the species Values) specifying inputs as "complex values" (like integers with tolerance, integers modulo n) built upon basic types and ensuring that glue assumptions could be satisfied. Consistency between the two parts is guaranteed by the FoCaL dependency and proof mechanisms.

The voting policy

Specification phase The aim is to specify the data-flow interfaces and the requirements for the system without referring to any specific solution. In FoCaL, data-flow interfaces are encoded by functions declarations and requirements by properties on these functions.

Specification of the voting policy is performed with a two levels approach. The first level corresponds to the specification of a most general voter. It gives the signatures and the generic properties of all 2oo3 voters, making no assumption on the voting policy.

The second level, derived from the first one, specifies the voting policy and gives the proof of the generic properties.

The specification of the generic 2oo3 voter is represented by a species "Voter 2oo3" with two parameters: a collection V for the values submitted to the vote, a collection Diag for diagnosis prescriptions. The species provides a single signature vote. It also gives the safety requirements allocated to the voter. In order to ease reading, we add a shortcut to extract the value from of output value. A species can be derived from this generic species for any choice of a voting policy. These derived species define the "voting policy", the glue properties required on the input values (through the collection parameter of interface Value) and give a proof of the generic properties. As an example, see the specification of a majority voter with identification of the faulty inputs as defined in section 3.

species Gen_2oo3_voter( V is Value, Diag is Basics_object) = signature vote in V -> V -> V -> (V *
( * Specification of the diagnostics output * ) species My_diag(C is Sensor, Q is Qualifier) inherits Basics_object = ... end;; To create the specification of the "majority voter", we use two main features of the FoCaL language. First, we use the FoCaL inheritance mechanism to create a species having all declarations, definitions and properties defined in the species Gen 2oo3 voter. Then, we instantiate parameters of Gen 2oo3 voter with a more specific species (i.e. My diag). Note that, the dependency calculus ensures consistence between the different occurrences of formal and effective parameters.

( * Specification of the majority voter * ) species Majority_voter(V is Value, C is Sensor, Q is Qualifier, Diag is My_diag(C, Q)) inherits Gen_2oo3_voter(V,
The new species contains the functional specification of the 2oo3 majority voter, the glue assumptions on parameters and the proof of safety properties under those assumptions (done with Zenon). We can compile the FoCaL model to an OCaml file and a Coq file. The first one contains only typed functions declarations that can be used as an external interface for a development. The second one contains a proof term of the safety properties that can already be checked by the Coq prover.

Architecture/design phase This phase introduces the architectural choices to answer the specification requirements. It provides definition of the functions and the representation of the species. From the majority voter specification, we have sufficient information to propose an implementation of the functional requirements and to provide a proof that this code fulfils them. Transition between specification and design is also made using inheritance. Here parameters are kept while a definition is provided to the declaration, using the FoCaL functional language. Proofs of the functional properties are made using Zenon. Giving a FoCaL interface (and thus at least a specification species) for the input values, the sensor and the qualifier, this species can be compiled: type-checking can be done and a translation of the whole species contents (including Zenon proofs) into a Coq term can be obtained to be immediately assessed. Thus we have a species that implements a 2oo3 majority voter, which can be used with any kind of input values respecting the required glue properties.

species Imp_Majority_voter(V is Value, C is Sensor, Q is Qualifier, Diag is My_diag(C, Q)) inherits Majority_voteur(V, C, Q, Diag) = ( * Implementation of the vote function * ) let vote( v1 in V, v2 in V, v3 in V) in V * Diag = let c1 = V!consistency_law( v1, v2) in let c2 = V!consistency_law( v1, v3) in let c3 = V!consistency_law( v2, v3) in if c1 then if c2 then if c3 then (v1, Diag!constr(C!sensor_1, Q!perfect_match)) ... ( *
Multiple inheritance can be used at design level to provide an existing representation to a specification species. For instance the implementation species Imp vote status is a "merge" of two species: the specification species Sp vote status which provides the functional requirements and the species Integers which provides the representation and its basic properties. The dependency calculus ensures compatibility between these inherited species. Definitions can also be changed at any level to fit new needs. In this case, the FoCaL compiler computes all definitions and properties impacted by the redefinitions and asks to provide a new proof of the impacted properties.

Building a voter

At this stage, we have several species representing all components of the voter. In order to obtain runnable code a species should be transformed into a collection. Thus a voter collection has to be created from the voter species and collections representing the values and the diagnosis. Firstly, we choose the nature of input values (here the collection Coll int with tol), finalise the diagnosis (here the collection Coll my diag). Secondly, we create a species which inherits from the implementation of the voter applied to effective parameters and we provide a proof for the glue assumptions. This step ensures "compatibility" between species. Then, as the new species is now complete, we can create a collection. When a component is a COTS (Commercial Off The Shelf) or a very low level component as I/O drivers, one cannot produce a proof of its functional properties. In the same way, we do not want to prove well known or highly used components. In order to consolidate our confidence level of such components, works are currently performed by M. Carlier [START_REF] Carlier | Functional Testing in the Focal environment[END_REF] to generate test cases from FoCaL functional requirements. These test cases can be ran on the external component to validate it. Verification of the voter using M. Carlier tool has been achieved. It shows that the FoCaL life cycle we propose is fully compliant with the validation of external components.

Re-usability

Many other implementations can fit the generic voter. For example, S. Dajani-Brown proposes a 2oo3 voter for avionics purpose [START_REF] Dajani-Brown | Formal verification of an avionics sensor voter using SCADE[END_REF]. This voter is based on a classical 2oo3 architecture with an high availability (voter provides an output even when only one input is available). Following our development cycle, we implemented this voter within FoCaL by changing the voting policy and the value representation. Then we carried out successfully all the proof of the generic voter properties (voter always returns one of the input values, voter is insensitive to inputs order).

Conclusion and further works

This paper illustrates a safety life cycle can be developed using FoCaL features like inheritance, parametrisation by collections, properties and proofs. This development process respects boundaries between development phases, produces a certified and efficient code, is compliant with standards and thus, eases the assessment process required before commissioning. Several other examples have been developed following the same methodology like hierarchical automata's, physical input acquisition. . . These developments give similar results on the development process.

In this paper, due to a lack of space, we only gave a short glimpse on FoCaL testing. However we used the testing tool (still in development), not only to do classical tests on outputs of the voter but also when encountering some difficulties in proofs, to validate expression of some requirements. We appreciated a lot to have at our disposal, at any stage of the development cycle, a proof tool and a test tool working on the same expressions. This is indeed a FoCaL feature which is of great help when expressing some requirements, when wondering about the validity of some lemmas, when some proofs are out of reach. In this last case, some of the corresponding statements are considered as axioms during proof process, a point which weaknesses the logical approach but is unavoidable in practice, thus increasing confidence by testing the statement is welcomed.

More generally, we emphasise the great facilities given by the coordination of Fo-CaL programming features (typing, inheritance, late binding, etc.) and FoCaL logical features (statements, proofs) through syntactical means controlled by dependency calculus. Indeed, having the possibility to introduce a statement using names not yet associated to a definition and to prove it under hypothesis submitted to a delayed proof obligation, allows to detect anomalies sooner in the life cycle and the diagnostic provided by the compiler helps to repair them. Yet it is possible to criticise the choice of a functional language for source code. Having no notion of internal state for species can be considered as a weakness. But first, there is no difficulty to translate, if needed, FoCaL definitions into some imperative language: the compiler uses only very basic features of programming languages (simple records and modules). Second, a lot of static analysers rebuild a functional version of imperative code to perform their analyses. In FoCaL this functional version is directly at hand, a point which will be exploited to integrate static analysers in FoCaL, in the near future as the new compiler was conceived to easily include such extensions.

Using the theorem prover Coq as an assessor while having near all proofs quite automatically done with Zenon and having the choice of either doing the remaining ones directly in the Coq environment build by the FoCaL compiler or assuming their statement as a good compromise between the confidence level and the cost of the development. Yet the choice of Coq can be questioned. As the compiler does not use truly specific features of Coq, other theorem provers based on type theories and a flavor of Curry-Howard isomorphism can be chosen.

  ∀v1, v2, v3 in value, vote(v1, v2, v3) = v1 ∨ vote(v1, v2, v3) = v2 ∨ vote(v1, v2, v3) = v3

Fig. 1 .

 1 Fig. 1. Voter decomposition

  Diag); ( * Shortcut to extract the value * ) let output_value(p in V * Diag) in V = basics#fst(p); ( * Safety requirements of a voter * ) property voter_returns_an_input_value: all v1 v2 v3 in V, output_value(vote(v1, v2, v3)) = v1 \/ output_value(vote(v1, v2, v3)) = v2 \/ output_value(vote(v1, v2, v3)) = v3 end;;

  Diag) = ( * Functional requirements of the majority vote * ) ( * Vote with 3 consistent values returns a perfect_match and * ) ( * the value of the first sensor. * ) property perfect_vote : all v1 v2 v3 in V, (V!consistency_law(v1, v2) /\ V!consistency_law(v2, v3) /\ V!consistency_law(v1, v3)) -> (output_value(vote( v1, v2, v3)) = v1) /\ (output_diag(vote( v1, v2, v3)) = Diag!constr(C!sensor_1, Q!perfect_match))) ... ( * Glue assumptions on parametrized species * ) property consistency_law_is_symmetric : all v1 v2 in V, V!consistency_law(v1, v2) -> V!consistency_law(v2, v1); ... ( * Proof of the safety requirements * ) proof of voter_returns_an_input_value = ... end;;

(

  * Specification species for a set of vote status * ) species Sp_vote_status inherits Setoid = ( ** The 3 values are inconsistent * ) signature no_match : Self; ( ** 1 value is consistent with the two other which are mutually inconsistent * ) signature range_match : Self; ... end;; ( * Design of the vote status * ) species Imp_vote_status inherits Sp_vote_status, Integers = ( * Definition of the set elements * ) let no_match = 0;; ... end;;

species

  Majority_voter_on_int_with_tol inherits Imp_Majority_voter(Coll_value, Coll_sensor, Coll_int_with_tol, Coll_my_diag) = proof of consistency_law_is_symmetric = by property Coll_int_with_tol!consistency_law_symmetric; ... end ;; collection Coll_int_imp_vote_tol implements Sp_int_imp_vote_tol ;; The collection Coll int imp vote tol is ready to use. let s = Coll_int_imp_vote_tol!output_value(voter( 1, 3, 5);; ( * Results of several calls * ) Voter for integer with a tolerance of 2 v1 : 1, v2 : 3, v3 : 5 --> val : sensor_2 , res : partial_match v1 : 1, v2 : 2, v3 : 5 --> val : sensor_3 , res : range_match v1 : 4, v2 : 5, v3 : 5 --> val : sensor_1 , res : perfect_match v1 : 1, v2 : 4, v3 : 7 --> val : sensor_1 , res : no_match

see : http://focalize.inria.fr

see : http://focal.inria.fr/zenon/

We wilfully limit the voter specification to a function that returns one of its inputs. Other more complex voters can be found in[START_REF] Paul | Theoretical Investigation of Generalized Voters for Redundant Systems[END_REF].

The third requirement is sometimes optional depending on which dependability characteristic is emphasised.

Filtering is different from the input comparison as it works on one single input in opposition to the consistency law which compare at least two inputs.

Note that the voter does not need transitivity for the consistency law. Use of a transitive consistency law will remove the partial match qualifier.

This work is supported in part by the Agence Nationale de la Recherche under grant ANR-06-SETI-016 for the SSURF Project (Safety and Security UndeR FoCaL).

The 2oo3 properties

Functional requirements should describe the voting policy. Each line of the table 1 is transposed in a functional requirement. For example, for a perfect match, the requirement is:

Table 1 makes also assumptions on symmetry and reflexivity of the consistency law 8 . This leads to define the following glue assumptions: ∀v1, v2 in value, consistency(v1, v2) ⇒ consistency(v2, v1) and ∀v in value, consistency(v, v)

A voter should also meet some safety requirements. Whatever is the order of the input values, the voter has to return a compatible output value. Thus a notion of "compatible output value" is introduced by properties P1 and P2. P1 says that if input values can be compared and output values are consistent and qualifiers are the same then the output values are compatible. P2 says that by default all output values are compatible for inconsistent input values (i.e. there is no choice made for inconsistent input values).


V Prinet
email: prinet@nlpr.ia.ac.cncassisa@liama.ia.ac.cn

C Cassisa

F F Tang

MRF MODELING FOR OPTICAL FLOW COMPUTATION FROM MULTI-STRUCTURE OBJECTS

Keywords:

We propose in this paper a new formulation of the equation of the optical flow enabling to compute global and local motions of multi-structure objects (flowers and petals, trees and leaves, ...). The displacement fields are computed using a Markovian Random Field (MRF) model. Local and global components of the vector flow are both explicitly retrieved. The minimization of the Gibbs energy is achieved with a down-scaling approach, in which we first analyze the motion of the compact object, the sub-structures' movement being retrieved in a second stage. We validate and demonstrate the efficiency of our approach on synthetic and real images for various applications.

INTRODUCTION

The objective of this paper is to propose an efficient formulation and computational framework to estimate local and global motions of non-compact non-rigid objects. Modeling rigid and non-rigid objects movement using optical flow (OF) has been widely studied for various applications including tracking, surveillance [START_REF] Ranchin | Moving objects segmentation using optical flow estimation[END_REF][START_REF] Ye | Two stages robust optical flow estimation[END_REF]. Analysis of deformation of non-compact material such as water or smoke has also recently raised much attention [START_REF] Menin | Hierarchical estimation and segmentation of dense motion field[END_REF]. However, objects which are composed of substructures (leaves of trees, feathers of birds, petals of flowers, etc) do not fit into these categories. Existing approaches are unable to tackle efficiently the problem because the deformation of this type of object is both global (at the level of the entire object) and local (at the level of the sub-structure, usually of a few pixels size). Most recent works aim at tackling the problem of discontinuities [4], of noise [START_REF] Roy | Mrf solution for probabilistic optical flow formulation[END_REF], to develop hierarchical or multi-resolution computational approaches [START_REF] Adachi | Multi-resolution optical flow estimation with local approximation[END_REF][START_REF] Provost | Hierarchical markovian segmentation of multispectral images for the reconstruction of water depth maps[END_REF].

We propose to generalize the constant intensity constraint of the optical flow, and to retrieve the optimal solution via a Markov Random Field (MRF) framework. The problem we address focuses on the multi-motion analysis of objects composed of sub-structures, for which both local and global components of the displacement vectors are modeled.

The rest of the paper is organized as follows: in section 2 recalling briefly the basic mathematical foundations of OF and MRF, we define the generalized constant intensity constraint (GCIC) and describe the energy function to be minimised. We propose a down-scaling approach, thus allowing to process the image at two different scales and details levels. Illustrations and analysis of the results on various synthetic and real data set are given in section 3. Finally, section 4 presents the conclusions.

THE APPROACH

While extremely simple, the two key points of the approach are (i) the formulation of a generalized constant intensity constraint (GCIC) and (ii) the down-scaling optimization scheme in a MRF framework.

General concept and definitions

We tackle the problem of one or several object(s) that are composed of multi-structures (trees, birds, flowers,..). Each object is animated by a global movement. Each object is itself composed of sub-objects or structures (such as leaves, feathers, petals, ...) which have a local motion independent from the global displacement of the object.

In order to differentiate the notion of global object and local structure, we define two graphs associated to different levels of resolution G :

G l = (S l , L l ) G g = (S g , L g )
where S l = {s l } represents the local nodes (indice l) defined either by the substructures of the objects or simply by the pixels of the image -i.e. card(S l ) = dim(I)-, while S g = {s g } is represents global nodes (indice g) defined by the center of each object in motion in the image -i.e. card(S g ) = number of objects. L l and L g are two distinct levels of vertices, linking independently the neighborhood nodes s l and s g respectively. Note that this definition imposes S l ⊃ S g .

Modeling the GCIC

Considering objects animated of a double movement -local and global ones-, the velocity vector v(i) at each point of the image i is expressed by:

v(i) = v g (i) + v l (i) v l (i) << v g (i) (1)
where v g (i) is the global displacement of the object O at point i and v l (i) is the local displacement of the substructure composing O at point i. Since all the substructures belonging to a given object O should possess the same global movement we have:

v g (i) = constant = v g ∀i ∈ O (2)
If the substructures are of one pixel size and have random independent movements, then local variations can be assimilated to white noise of zero mean and:

i∈O v(i) = N v g ( 3
)
where N is the number of points within the object.

From equation ( 1), the first order generalized optical flow equation (so-called Generalised Constant Intensity Constraint) can be written:

∇I. (v g + v l ) + δI δt = 0 v l << v g (4)
By averaging equation ( 4) over all the points of the object O and knowing from equation ( 2) and ( 3

) that v g + v l = v g + v l = v g = v g ,
thus, for a given object and as a first approximation, we have:

(∇I) T .v g + I t ≈ 0 (5)
with a = 1 N N i=1 a i .

Energy terms of the MRF

The displacement field in the image is given by the v that satisfy equation (4). Knowing that the solution is undefined at points where v is orthogonal to ∇I -so called aperture effect-, some additional constraints -or regularization factor-should be added.

Using an MRF framework, the solution v will be given by the configuration of our random variable x, that maximizes a joint probability function taking the form of a Gibbs distribution:

P (x, y) = 1 Z e -E(x,y) (6)
where Z is the normalization constant and

E(x, y) = -( s∈C1 α d V d (y s , x s )+ s,s ∈C2 α p V p (x s , x s ))) (7
) where y is a function of the observed data. From a general point of view, C 1 and C 2 are single-site and pair-site cliques respectively; the Gibbs energy E is thus the summation of a data term E d = α d V d , and a prior term E p = α p V p independent of the data but dependent of its neighborhood N s ; α d = α d (s) and α p = α p (s, s ) are two weighting coefficients.

For our problem, the data term is naturally given from the GCIC (equation ( 4)). It should be satisfied at each site of the graph (S l , L l ):

|E d | = s∈C1 α d ∇I(s). (v g (s) + v l (s)) + δI(s) δt 2 (8)
with

C 1 = S l .
On the other hand, the prior term is defined such as to constrain the displacement flow to be continuous: amplitude and angular variations between neighborhood sites should be minimized, both at global and local levels. We have therefore:

|E p | = s,s ∈C2 β p (||v l (s) -v l (s )||) 2 (9) + s,s ∈C3 γ p (||v g (s) -v g (s )||) 2 + s,s ∈C3 λ p v g (s).v g (s ) ||v g (s)||||v g (s )|| -1 2 where C 2 = {s l , s l |s l , s l ∈ S l , s l ∈ N l } and C 3 = {s g , s g | s g , s g ∈ S g , s g ∈ N g }.
The neighborhoods N l and N g are defined within a 4-connectivity by the connected sites belonging to G l and G g respectively. The first two terms of equation (9) impose a smooth variation of the amplitude at local scale (first term) and global scale (second term). The last term constrains the motion's direction to change slowly between neighboring objects. The site dependent coefficients α d , β p , γ p , λ p are set such that : α d = 0 if s ∈ O, γ p , λ p = 0 everywhere, and

β p = 0 if s ∈ O, s ∈ O (10)
β p = 0 otherwise. In other words, the smoothing between local vectorial components is to be applied only for intra-object and not interobject neighborhood.

It is worth noticing that, in the case of several objects in the image, the model is properly defined only if the global movement between two neighborhood objects varies slowly. However, we will see that in practice we do not encounter this limitation, because the local term will serve to compensate the possible loss generated by the global smoothing.

Implementation

The optimal solution is retrieved by computing the v that minimizes E(x, y). It is achieved without major difficulty with a ICM (iterated conditional mode) algorithm. However, since the random value x is a four dimensional vector which has components that can take any real value within a given range

[v min l , v max l , v min g , v max g
], the direct optimization of equation ( 7) using ( 8) would be extremely time consuming. In addition, the initialization of ICM algorithm would be twice as critical as traditional approaches (i.e. approaches that do not search for a local and a global component).

For these reasons, we choose to compute the displacement field via a down-scaling approach, following two steps :

• Initialization : compute the optimal solution of equation (7), using ( 5) and ( 9) as data term and prior term respectively. This enables to find a realisation v0 g , which will serve as a first approximation. The process is extremely fast and enables to give a rough picture of the displacement flow.

• Estimation of vg , vl , by substituting equation ( 8) into ( 7) and using v0 g as initialization.

Note that the approach is based on the knowledge of the graph (S g , L g ), which means that, theoretically, one should be able to localize the objects within the image, before running the optical flow. When feasible, a pre-processing segmentation step can be carried out for this purpose. In most cases however, we can perform arbitary segmentation using a regular grid, without affecting the quality of the results. We will illustrate several cases in the next section.

RESULTS ANALYSIS

Results analysis is performed on a set of very different synthetic and real images, thus illustrating various possible applications. All results presented in this section have been obtained with the values (α d , β p , γ p , λ p ) = (1, 10, 50, 100) for forest sequence and (1, 10, 10, 10) for the others. Video sequences have been previously smoothed in space and time with Gaussian filter of variance 1.5; the synthetic forest images, have been spatially smoothed only. The derivation mask we used is similar to [START_REF] Roy | Mrf solution for probabilistic optical flow formulation[END_REF][START_REF] Barron | System and experiment performance of optical flow techniques[END_REF].

Synthetic data : forest

The initial motivation of this work was to analise the Earth ground displacement observed from forest trees aerial images. This phenomena can be observed on terrains of steep slopes and are characteristic of forthcoming landslides. Here we make use of synthetic images simulating a plantation of trees on a steep terrain, generated by the AMAP software [START_REF] De Reffye | Plant faithful to botanical structure and development[END_REF]. Two sequences of two images each have been gene-rated.

The first sequence shows a unidirectional displacement along the slope in the vertical direction, the second is a radial displacement. The position of the camera is unchanged between the two "acquisitions". One of the simulated image and the known displacements are illustrated on figure 1.

The objects we consider are the trees, the local structures being defined by the leaves. The images are particularly difficult to process because the intensity constancy is hardly verified at pixel level.

Figure 2 illustrates the results obtained from our approach (top), compared to those from Horn and Shunk (H&S) implemented by Barron [8,[START_REF] Horn | Determining optical flow[END_REF] (bottom). The computed displacement field, for transverse and radial motions, are both consistant with the ground truth. A contrario, H&S algorithm appears to be more sensitive to the texture effect and non uniform brightness variation of the leaves. Table 1 compares the average angle error between H &S and our approach.

In these images in which segmentation is rather easy to perform, we have analysed the impact of the pre-propressing step on the results. In figure 3, we compare the vector flow obtained with and without presegmentation. In case of presegmentation, each tree is treated as an individual object. Otherwise, the image is organised into a matrix of squared paches, each patch being associate to an object. Table 1 shows that the effect of the square size is negligeable, as expected. Table 1. Average angle error in degrees with presegmentation (seg) and with arbitrary patchs (grid size NxN).

Reference data set : synthetic and real data

Results on synthetic and real video sequences -data are downloaded from ftp.csd.uwo.ca/pub/vision-have been computed.

For the synthetic sequences, we obtained the same range of average angle error than shown by [START_REF] Roy | Mrf solution for probabilistic optical flow formulation[END_REF].We illustrate here only one of them, i.e. the Magic Cube, given in figure 4. The computed displacement (v = v g + v l ) shows a clear smooth motion tracking of the cube and of the bottom part of the tray. The motion of the white part however has not been detected at all, due to the perfect uniformity of the gray level (constant white). Barron's result with Horn and Shunk approach is also illustrated for comparison.

CONCLUSION

We proposed in this work an approach dedicated at first to the movement analysis of objects composed by sub-structures,

1 .Fig. 2 .

 12 (a) Entire image (b) Detail of (a). (c) Transverse displacement (d) Radial displacement. Fig. Simulated forest trees and ground truth motion. Transverse motion Radial motion Results of GCIC (top) -Horn & Shunk (bottom).

Fig. 3 .

 3 v g & segm. (v g + v l ) & segm. v g & grid 40x40 Local vs global motion, with and without segmentation

  (a) Original image (b) GCIC (v g + v l ) (c) H & S Fig. 4. Results on the Magic Cube sequence 3.3. Flower video The last illustration is on a flower video sequence (downloaded data). The sequence visualizes the blooming of the flower. Each petal can be considered as an individual object. The global displacement is first computed in each patch grid of the image. Edge points detection is performed by a Canny filter for each frame of the sequence. The displayed result in figure 5 represents the v g component of the displacement taken at each edge point. Result on the entire video provides clear cue of the flower blooming.

Fig. 5 .

 5 Fig. 5. Two flower frames and the associated computed v g i.e. animated by global and local motions. We illustrated that the introduction of a local displacement vector enables to handle efficiently the problem of discontinuity. With regard to forestry application, ongoing works are dedicated to textural movement analysis. Acknowledgment The authors wish to thank Thierry Fourcaud

Acknowledgment The authors wish to thank Thierry Fourcaud for stimulating discussions and Guillaume Perrin, for the creation of the forest images.