Axelle Hego

Floriane Collin

Hugues Garnier

Rémy Claverie

Sensitivity Analysis on a green roof hydrological model

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

GdR MASCOTNum 2021 Sensitivity Analysis on a green roof hydrological model

Axelle HEGO 1 , Floriane COLLIN 1 , Hugues GARNIER 1 , Rémy CLAVERIE 2 1 Université de Lorraine, CRAN, CNRS UMR 7039, 2 Cerema Est, Team research group, F-54510, Tomblaine, France Context Urban imperviousness a major urban issue during rainfall events Solution → Green Roofs • Rainfall data and real water content measured in a green roof of the CEREMA of Nancy

• Simulation of the water infiltration into the layers using Richards equation ( 1) implemented in Hydrus-1D software

∂θ(h) ∂t = ∂ ∂x   K(θ) ∂h ∂x   - ∂K(θ) ∂x (1)
combined with Van Genuchten model ( 2) and Mualem model ( 3)

θ(h) = θ s -θ r (1 + |αh| n ) m -θ r with m = 1 - 1 n (2) K(S e ) = K s S l e 1 -1 -S 1/m e m 2 with S e (θ) = θ(h) -θ r θ s -θ r (3)
Problem statement

• Input : Rainfall • Output : Water content θ(t) or V W C(t) in (ii) • k = 6 uncertain parameters : θ s , θ r , K s , l,
0.5 1 Q out [cm.h -1 ] Q out nominal value

GSA method

Method based on PCE :

Y (t) = G(X, t) = +∞ j=0 a j (t)ψ j (X 1 , ..., X k ) (4)
Method applied at each time instant : 1. Define the distribution of uncertain parameters to compose ψ j Uniform distribution → Legendre Polynomials 2. Define p, the maximum development order of ψ j 3. Estimate the PC coefficients a j (t) by solving a least square problem 4. Estimate sensitivity index (SI) with : First order SI :

S i (t) ≈ j∈I i a 2 j (t)E[ψ 2 j (X i )] var[Y (t)] (5)
where I i is polynomial index of ψ j which depends only on X i Total SI :

S T i (t) ≈ j∈I #i a 2 j (t)E[ψ 2 j (X i )] var[Y (t)] (6)
where I #i is polynomial index of ψ j which depends on X i and all its interactions.

For the green roof model, 500 samples from Sobol sequence (QMC) to generate Y (t) and a development order p = 3 to obtain indices is adapted

Results on Green Roofs

How vary the water content VWC(t) in the substrate when ... ... substrate parameters vary ?

•

  lower the peak flow rate in water system by 22% to 93% • delay the peak flow by 0 to 30 min Collaboration CEREMA : Green Roofs experts CRAN : Model Analysis skills Collaboration between CEREMA and CRAN for a better understanding of the GR behavior Green

•

  Variations whatever VWC(t) evolution • S i = S T i : no interaction between parameters • 3 influential parameters : saturated water content θ s , pressure head fitting parameter α and porosity distribution n • S θ s follows VWC(t) i.e when it rains • S n inversely follows VWC(t) i.e when it rains • S α varies slightly following VWC(t) • The other parameters are not influential ... drainage parameters vary ? • No variation when VWC(t) is saturated As for the variation of substrate paremeters, we have : • S i = S T i • Same 3 influential parameters and the other parameters uninfluential • Same dynamics for S n , S θ s and S α but with more intensity Parameter uncertainties of the different layers impact the water content with different intensityConclusion and Prospect• 3 influential parameters, saturated water content θ s , pressure head fitting parameter α and porosity n and different influences depending on the layer • Prospects : analyse the outflow and include meteorological uncertainties


Yamine Aït-Ameur
email: yamine@ensma.fr

Patrick Girard
email: girard@ensma.fr

Francis Jambon
email: jambon@ensma.fr

Using the B formal approach for incremental specification design of interactive systems

Keywords: Model oriented notation, B method, specification refinement, interaction properties verification, specification of interactive system

This paper introduces a new technique for the verification of interactive systems. It first presents the use of a model oriented formal method for specifying interactive systems, i.e. the B method. Then, it suggests formally based solutions which allow solving difficulties that are inherent to interactive systems specification, like reachability, observability or reliability. Our claim is that this model-oriented technique that uses proof obligations can be used together with model checking techniques, where automatic proofs of properties can be performed.

INTRODUCTION

Formal specification techniques become more and more used in the area of computer science and particularly for the development of secure systems namely "critical systems". These systems require a high level of correctness and consistency, which encourages formal development. Several approaches in formal methods have been proposed in the last decade. They are divided in different categories depending on the kind of semantics they are based on [START_REF] Brun | A taxonomy and evaluation of formalisms for the specification of interactive systems[END_REF][START_REF] Feather | A Survey and Classification of some program Transformation Approaches and Techniques[END_REF][START_REF] Sannella | A Survey of Formal Software Developement Methods[END_REF]. Conversely, formal specification of interactive systems can be split into different ways. Historically, the first way concerns the Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for , Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}.

dialogue description [START_REF] Dix | Human-Computer Interaction[END_REF]. Related to the natural language decomposition, human-computer interactions have been broken down into three hierarchical levels, the lexical level, the syntactic level and the semantic level. The dialogue description mainly concerns the syntactic level. It involved several formalisms, grammars, state-based diagrams or event models [START_REF] Green | A Survey of three Dialogue Models[END_REF]. More recently, the development of GUI-Builders (Graphical User Interface Builders) has considerably increased the graphical power of user interfaces. GUI-Builders allowed rapid prototyping of interactive systems, and authorised incremental development. Nevertheless, lack of precise specifications is becoming a more and more critical issue.

On the one hand, user-centred design leads to semi-formal but easy to understand notations, such as UAN [START_REF] Hix | Developping user interfaces: Ensuring usability through product & process[END_REF] and MAD [START_REF] Scapin | Towards a method for task description : MAD[END_REF] for interactive design, or GOMS [START_REF] Card | The psychology of Human-Computer Interaction[END_REF] for evaluation. On the other hand, adaptation of well-defined approaches, combined with interactive models, brings partial but positive results. These are for example the interactors and related approaches (Duke and Harrison, 1993b[START_REF] Paternó | A Theory of User-Interaction Objects[END_REF][START_REF] Palanque | Modélisation par Objets Coopératifs Interactifs d'interfaces hommemachine dirigées par l'utilisateur[END_REF], using model oriented approaches (Duke and Harrison, 1993a), algebraic notations [START_REF] Paternó | On the LOTOS use to describe graphical interaction[END_REF], Petri nets [START_REF] Palanque | Modélisation par Objets Coopératifs Interactifs d'interfaces hommemachine dirigées par l'utilisateur[END_REF] or Temporal Logic [START_REF] Brun | XTL: a temporal logic for the formal development of interactive systems[END_REF][START_REF] Abowd | A Formal Technique for Automated Dialogue Development[END_REF] In this paper we deal with model oriented formal methods. State transition networks use finite automata to describe the transition systems, Petri nets and temporal logic gave interesting results from the automatic verification point of view by providing automatic algorithms allowing to check critical properties of interactive systems like liveness, reachability, safety and so on. However, building these transition models incrementally is a heavy task. These approaches are based on the building, by composition, of a whole model (transition system) which represent the system to be described. Then, properties can be checked and the transition system is interpreted to generate a program implementing the behaviour it describes. The difficulty in such techniques is to build the whole [START_REF] Dix | Human-Computer Interaction[END_REF]. Other model-oriented approaches have been suggested. They are neither based on transition systems nor they provide an automatic procedure for the verification of the properties of the system. These systems are based on the generation of proof obligations that are checked by the user (with the help of a theorem prover). Among these techniques, VDM is based on preconditions and postconditions [START_REF] Bjorner | VDM a Formal Method at Work[END_REF] and on the theory of partial functions, Z is based on set theory [START_REF] Spivey | The Z notation: A Reference Manual[END_REF], and B is based on the weakest precondition calculus [START_REF] Abrial | The B Book: Assigning Programs to Meanings[END_REF]. They allow the description, in high abstraction level language, of the different components of a given system. However, these approaches require an important work to describe the different functions of the system.

Our claim is that neither the first approaches nor the second ones solve the whole problems, but the merging of both techniques seems to be a promising approach. Indeed, the first one allows the control of properties by model checking and neglects

Using the B formal approach for incremental specification design of interactive systems

Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for , Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}. the development aspects. In opposite, the second approach allows a complete development of a system and controls all the properties by the verification of all the proof obligations (automatically or by the user). So, several interaction properties can be proved. The more important advantage of this second technique is that it avoids the state explosion problem that becomes crucial when systems grow and it allows the development of the whole system by refinement. As we stated above, our paper deals with the last category of formal methods. We focus on the B method [START_REF] Abrial | The B Book: Assigning Programs to Meanings[END_REF][START_REF] Lano | The B Language Method: A guide to practical Formal Development[END_REF]. Compared to VDM and Z, it allows the definition of a constructive process to build whole applications, with the respect of all the rules by the use of a semi-automatic tool (Steria méditerranée, 1997). Finally, notice that we did not address the other approaches mainly the ones based on algebraic techniques, rewriting, or concurrent languages.

This paper is organised as follows. In the next section, we briefly present a case study, which stems from the French group on formal specification for highly interactive systems FLASHI [START_REF] Palanque | Groupe de travail GP3-FLASHI[END_REF], and we outline the major properties we want to ensure. Section 3 explains the B-method and presents a short overview of proving methods for interactive properties. Section 4 outlines some aspects of the B language over a well-known example, the mouse. Last, section 5 gives examples of B analysis in the context of our example, and details the usage of the B-tool, that allows proving properties.

CASE STUDY

Our case study is a co-operative version of a Post-It®1 Note software. It appears on the screen as a block that can be iconified, but cannot be moved. Clickable areas allow direct manipulation of the block, for iconification, and close (quit). It is possible to enter text into the Post-It® Note on the block, which always exists. Last, it is possible to detach the upper Post-It® Note from the block, and then to drag it anyway. Post-It® Notes have a similar behaviour, that differs in four ways: (1) the detach area is restricted to a drag command area, (2) the close area becomes a kill area, (3) a resize area is defined in the lower-right corner, corresponding to a standard resize behaviour, and (4) a send behaviour is defined. This behaviour consists in emitting the Post-It® Note to a receiver that is visualised as a special icon. The interactive trigger is a drop (mouse up event) onto the icon.

Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}. Defining good properties of Interactive Systems is an open problem. Several approaches have proposed classifications of properties. For example, [START_REF] Dix | Human-Computer Interaction[END_REF] define three main categories of principles to support usability, which are then refined into about fifteen more specific principles. In their article, J. Campos and M. Harrison [START_REF] Campos | Formally Verifying Interactive Systems: A Review[END_REF] give a good framework for classifying user interface properties, separating them among three classes that address the user (visibility), the user interface (reachability), and the underlying system (reliability):

• Visibility relates to feedback and information perception by the user. In our case study, can we ensure that the user can perceive internal state of the system? Does every Post-It® Note move rely to hidden/exposed status of all the perceivable Post-It® Notes? • Reachability deals with what can be done at the user interface and how can it be done. In our application, it concerns for example the way we can move the Post-It® Notes. How can the mouse be taken into account? Is it always possible to move a Post-It® Note? Can it move away from the screen? • Reliability concerns the way the interface works with the underlying system.

Does some predicate on the state of the system always hold? Is it possible to ensure that an empty Post-It® Note cannot be sent?

THE B METHOD AND INTERACTION PROPERTIES

The B method allows the description of different modules, i.e., abstract machines that are combined by programming in the large operators. This combination allows building complex systems incrementally and correctly when all Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}.

the proof obligations are proved. Moreover, the interest of this method in our case is the tool it provides.

The abstract machine notation

The abstract machine notation is the basic mechanism of the B method. J. R. Abrial defined three kinds of machines identified by the keywords MACHINE, REFINEMENT and IMPLEMENTATION. The first one represents the high level of specification. It expresses formal specification in a high abstract level language. The second one defines the different intermediate steps of refinement and finally the third one reaches the implementation level. Note that the development is considered to be correct only when every refinement is proved to be correct with respect to the semantics of the B language. Gluing invariants between the different MACHINES of a development are defined and sets of proof obligations are generated. They are used to prove the development correctness. A theorem prover including set theory, predicate logic and the possibility to define other theories by the user, achieves the proof of these proof obligations. The proving phase is achieved either automatically, by the theorem prover, or by the user with the interactive theorem prover.

Description of abstract machines

J. R. Abrial has described several important clauses for the definition of abstract machines. Depending on the clauses and on their abstraction level, these clauses can be used at different levels of the program development. In this paper, a subset of these clauses has been used for the design of our specifications. We will only review these clauses. A whole description can be found in the B-Book [START_REF] Abrial | The B Book: Assigning Programs to Meanings[END_REF]. The typical B machine starts with the keyword MACHINE and ends with the other keyword END. A set of clauses can be defined in between. In our case, these clauses appear in the following order:

• EXTENDS is a programming in the large clause that allows to import instances of other machines. Every component of the imported machine becomes usable in the current machine. This clause allows modularity capabilities. • SETS defines the sets that are manipulated by the specification. These sets can be built by extension, comprehension or with any set operator applied to basic sets.

• CONSTANTS defines all the constants that are used in the machine. Notice that the constants described can have any type (naturals, elements of sets, constant functions, and so on). • PROPERTIES are logical expressions that are satisfied by the constants described in the previous clause.

Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}.

• VARIABLES is the clause where all the attributes of the described model are represented. In the methodology of B, we find in this clause all the selector functions which allow accessing the different properties represented by the described attributes. • DEFINITIONS is a set of definitions introduced by the user. They are rewritten everywhere they are used in a machine. It allows simplification of machine notation. • INVARIANT clause describes the properties of the attributes defined in the clause VARIABLES. The logical expressions described in this clause remain true in the whole machine and they represent assertions that are always valid. • INITIALISATION clause allows giving initial values to the variables of the corresponding clause. Note that the initial values must satisfy the invariant. • OPERATIONS clause is the last clause of a machine. It defines all the operations (functions and procedures) that constitute the abstract data type represented by the machine. Depending on the nature of the machine, the OPERATIONS clause authorises particular generalised substitutions to specify each operation. The substitutions used in our specifications and their semantics is described below.

Other syntax possibilities are offered in B, and we do not intend to review them in this paper, in order to keep its length short enough.

Semantics of generalised substitutions.

The calculus of explicit substitutions is the semantics of the abstract machine notation and is based on the weakest precondition approach of Dijkstra [START_REF] Dijkstra | A Discipline of Programming[END_REF]. Formally, several substitutions are defined in B. If we consider a substitution S and a predicate P representing a postcondition, then [S]P represents the weakest precondition that establishes P after the execution of S. The substitutions of the abstract machine notation are inductively defined by the following equations. Notice that we restricted ourselves to the substitutions used for our development. The reader can refer to the literature [START_REF] Abrial | The B Book: Assigning Programs to Meanings[END_REF][START_REF] Lano | The B Language Method: A guide to practical Formal Development[END_REF] for a more complete description: The last one represents the predicate P where all the free occurrences of x are replaced by the expression E. Notice that when a given substitution is used, the B checker generates the corresponding proof obligation, i.e., the logical expression on Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}.

the right hand side of the operator "<==>". This calculus propagates a precondition that must be implied by the precondition set by the user. If not, then the user proves the precondition or modifies it.

Interaction properties

Proving interaction properties can be achieved by the way of model checking or theorem proving [START_REF] Campos | Formally Verifying Interactive Systems: A Review[END_REF]. Theorem proving is a deductive approach to the verification of interactive properties. Unless powerful theorem provers are available, proofs must be made "by hand". Consequently, they are hard to find, and their reliability depends on the mathematical skills of the designer. On the opposite, model checking is based on the complete verification of a finite state machine, and may be fully automated. However, one of the main drawbacks of model checking is that the solution may not be computed due to the high number of states [START_REF] Campos | Formally Verifying Interactive Systems: A Review[END_REF]. The last sessions of EHCI'95 and DSV-IS'97 show a wide range of examples of these two methods of verification.

As an example, model checking is used by Palanque et al. who model user and system by the way of object-oriented Petri nets -ICO- [START_REF] Palanque | Validating interactive system design through the verification of formal task and system models[END_REF]. They argue that automated proofs can be done to ensure that: there is no cycle in the task model; a specific task must precede another specific task (enter_pin_code and get_cash in the ATM example); and that the final functional core state is the final user task (get_cash and get_card). These proofs are relatives to reachability. Lauridsen uses the RAISE formalism to show that an interactive application -functional core, dialogue control and logical interaction-can be built using translations from the functional core adapter specification [START_REF] Lauridsen | Systematic methods for user interface design[END_REF]. Then, Lauridsen shows that this refinement method can prove interaction properties relatives to predictability, observability, honesty, and substitutivity.

In the meantime, Paternó and Mezzanotte check that unexpected interaction trajectories expressed in a temporal logic -ACTL-cannot be performed by the user. The system -a subset of an air traffic control application-is modelled by interactors specified with LOTOS [START_REF] Paternó | Formal verification of undesired behaviours in the CERD case study[END_REF]. Brun et al. uses the translation from a semi-formal task-oriented notation -MAD- [START_REF] Scapin | Towards a method for task description : MAD[END_REF]) to a temporal logic -XTL- [START_REF] Brun | XTL: a temporal logic for the formal development of interactive systems[END_REF] and prove reachability [START_REF] Brun | Utilisation des spécifications formelles dans le processus de conception des Interfaces Homme-Machine[END_REF].

Our approach -using the B method-deals with the first method, i.e., theorem proving. Yet, the method does not suffer from the main drawbacks of theorem proving methods, i.e., proving all the system "by hand". Most of the proofs, regarding visibility or reachability, which are compulsory in the building process are checked by the B-Tool "Atelier B". Notice that in our case study, about 95% of the proofs obligations are automatically proved. Moreover, since the specification is incrementally built, the proofs are also incrementally built. Indeed, compositionality Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}.

in B ensures that the proofs of the whole system are built using the ones of the subsystems. This technique considerably simplifies the interaction properties verification. And then, this incremental conception of applications asserts that the proofs needed at the low levels B-machines of the application, i.e. the functional core, are true at the higher levels, i.e. presentation. So, the reliability is checked by construction. The following sections give examples of verification of visibility and reachability properties in our case study using the B technique.

FORMALISATION OF THE MOUSE INTERACTION

This section presents a simple example of the use of the B notation for the specification and for the verification of the operations related to the mouse. It is derived from the case study described in the section 3. The complete formalisation of this case study in B can be found in (Aït-Ameur et al., 1998a, Aït-Ameur et al., 1998b). This specification has been designed using reverse engineering techniques starting from an already existing toolkit implementing mouse manipulation. This reverse engineering task to re-design the mouse specification is a crucial phase in our work. It allows using the B language in a uniform manner even for already designed programs. However, this step of development needs to be achieved for other parts of an interactive application (e.g. keyboard). Below, we specify the only operations we are interested in.

Specification

The machine we define is named POSTIT_MOUSE. It defines two sets: the POST_MOUSE representing all the possible values for a mouse (it behaves as a type) and a finite enumerated set MOUSE_STATE for the states of the mouse.

MACHINE POSTIT_MOUSE

SETS POST_MOUSE; MOUSE_STATE ={up, down, clicked}

For convenience, we have considered three states only. Without loss of generality, we have voluntarily omitted the other states because they are not used in our application. Notice that they could have been included.

Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}. The previous part defines a set of constants. The max_post_mouse constant is the maximum of mouse positions we can have. The x_mouse_position_default and y_mouse_position_default are the default coordinates of the mouse. The max_mouse_position_high and max_mouse_position_wide are the maximum values of the mouse coordinates. They correspond to the dimensions of the screen. For a given mouse in the set the_post_it_mouse, the previous selectors define a set of functions that allow retrieving the coordinates of a mouse, its state and its creation. The last predicate expresses that every mouse position remains in the screen. Several operations on the mouse (creating, moving, clicking…) are defined below. We only give the details for creating and for moving the mouse ( ! xx stands for ∀ xx ).

Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}. The create_mouse_position creates a mouse and gives it the status up, and default position as coordinates. The move_mouse_with_drag allows the moving of the mouse with its state to down and it moves it to the coordinates (aa,bb), where a precondition requires aa and bb to be in the screen. This precondition is mandatory to prove that the mouse never goes out of the screen. In other words this precondition is an example of a visibility property.

Proofs

The previous machine generates a set of 33 proof obligations. All of them were automatically proven by the "Atelier B" tool. Among these proof obligations, let us consider the ones of the move_mouse_with_drag. There are 6 proof obligations, and among them, the ones that says that the invariant assertion (1) is preserved. There, the precondition: Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}.

Let us now, try to write the following for the move_mouse_with_drag operation. We obtain: If we violate the precondition in the move_mouse_with_drag operation by omitting that:

( aa : 1..max_mouse_position_wide & bb : 1..max_mouse_position_high )

Then the system is not capable to prove the correctness of the operation. It generates a proof obligation saying that there is a need to prove the invariant assertion (1) of the INVARIANT clause which is violated.

INTEGRATION OF THE MOUSE INTERACTION

Linking two abstract machines is possible thanks to programming in the large operators offered by the B method. These operators allowed us to incrementally build complex and sound formal specifications. In this section we present an abstract machine which specifies a simple window manager, and we mainly focus on the moving operation of a window. Then, this abstract machine and the one corresponding to the mouse are used to build another complete and sound abstract machine, which specifies the window manager with an interaction by the mouse. We do not give the complete specification and we focus on the proof aspects. The whole-annotated abstract machine is defined in (Aït-Ameur et al., 1998b).

The window manager without mouse interaction

The POSTIT_VISU_WITHOUT_INT is the abstract machine that defines a simple window manager related to our case study.

Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}.

Specification

The following abstract machine defines a set of windows (to support a post it). It represents the module of all the allowed window manipulations.

MACHINE POSTIT_VISU_WITHOUT_INT EXTENDS POSTIT_VISUALIZATION CONSTANTS ... PROPERTIES max_post_visu=card(POST_VISU) & max_post_it_wide=300 & max_post_it_high=250 & VARIABLES ...
The previous properties define the values of the dimensions of the screen. The variables of the INVARIANT describe the accessors to the different components of a window. the_post_it_visu is the set of all the windows effectively created, and get_new_post, block_state and post_it_window_status are the functions which respectively imports a window from the POSTIT_VISUALIZATION machine, gives the state of the block and computes the status of the window from the one on the imported window. The previous logical expression (2) is an important invariant. It states that all (!) the windows of the set the_post_it_visu have their upper-left corner in the screen. This invariant is conserved and proved for all the operations. We will now describe the move_window_position action, and every element it uses. In this machine, move_window_position is not strictly constrained. For example, it is possible to partially quit the visualisation window while moving a Post-It® Note. This constraint will be put later on. We only take into account the constants, variables and invariants that are needed by move_window_position.

Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}. The previous preconditions say that the new coordinates of the upper-left corner of a window (aa,bb) must belong to the screen, that the window pp is effectively created (belongs to the_post_it_visu set), that the block of Post-It® Notes is effectively open and that the window can be displayed or hidden. Here, a parallel substitution is used. It says that after executing this operation the new coordinates of the upper-left corner become (aa,bb) and that the operation update_hidden (of another non described machine) is called. This last operation is called in order to update the status of the windows that become hidden or displayed after the current window has been moved. We take into account here a visibility property we have expressed in section 2.

Proofs

From these previous preconditions, we can infer the following properties:

• Windows never can be moved when they are iconified,

• Windows never can be moved when the block is not opened, • Windows never have their upper-left corner outside of the screen. This is very important for windows manipulation. It is directly derived from the invariant assertion (2).

All these proofs show that reachability properties can be checked in the top-level B-machine.

Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for , Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}.

Specification of the window manager with mouse interaction

Now, we get two abstract machines: one for the mouse and another for the window managing. The goal of the third abstract machine is to merge these two abstract machines in order to build a new one that integrates the manipulation of the windows using a mouse.

Specification

The following abstract machine, named POSTIT_VISU_WITH_INT_MOUSE extends (by a programming in the large operator) the abstract machines for mouse and for windows. The previous properties are named gluing properties. They make connections between the constants of all the imported machines. Indeed, it specifies that the dimensions of a screen for a window are the same as the ones for a mouse. The set the_post_it_visu_with_mouse records all the windows manipulated by a mouse. The selectors define a set of functions that allow extracting a window by get_the_post_it_visu and the mouse by get_the_mouse. Let us give the details of the action move_window_with_mouse that allows moving a window combining the design of interactive systems Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for , Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}.

interaction of the mouse. This action has a set of preconditions, which needs to be valid before the action is performed. They are commented below. The new coordinates of the upper-left corner of the window must define a point in the limits of the screen. Notice that these preconditions imply:

• The ones of the move_window without the use of the mouse. It remains to assert that the window is displayed, • and the ones of move_mouse. It remains to assert that the mouse is down to ensure that the drag is possible. The different elements manipulated by the operation (mouse, a window, a window with mouse interaction) must be already created. The coordinates delimiting the moving zone of the window must belong to the screen, i.e., must appear in the screen.

Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}. The mouse position must be in the moving zone delimited previously. This is an additional precondition which is strictly related to the fact that there is a mouse interaction and that the mouse must be in the moving zone. This precondition could not be expressed in one of the imported machines.

Calling

the move_window_position action of the POSTIT_VISU_WITHOUT_INT moves the window and the mouse is also moved by the action move_mouse_with_drag of the machine POSTIT_MOUSE. Notice that this action is one of the actions that combine the mouse toolkit and the window manager toolkit.

Proofs

From the PROPERTIES assertions, we derive that the coordinates of the upperleft corner of a window and the ones of the mouse take their values in the same domain. Therefore, we can prove that a mouse can manipulate every window. This is an important reachability property. The previous abstract machine gives supplementary preconditions on the objects. These preconditions imply the ones of the corresponding operations in the machines imported by extension. Therefore, the prover is capable to complete the proof of correctness. This is an important issue of the B method that shows that B is not only capable to structure the development of specifications, but it allows the structuration and the modularization of the proofs. Moreover, this approach shows that it is possible to structure the specifications hierarchically with respect to the implication of the preconditions. Here, the implication plays the role of an ordering relation from weak to strong. Indeed, the preconditions of the last machine are stronger than the ones of the imported machines. Finally, this mechanism of weakest precondition conserves the coherence of the whole specification. This previous machine has shown that it is not possible to:

Aït-Ameur Y., Girard P., & Jambon F. Using the B formal approach for incremental specification design of interactive systems. IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'98), Heraklion (Crete), Greece, 14-18 September 1998. p. {to be published}.

• move a window with a mouse whose position is not in the moving zone, • move a window if there is no mouse, • move a window if it is eliminated: this property is inherited form the imported machine.

We can prove the previous properties by removing the corresponding assertions from the preconditions and then the prover will complain because we are not capable to prove some proof obligations.

CONCLUSION AND FUTURE WORK

This paper has shown the use of the B method on a non-trivial case study. It has illustrated the capability of B to handle different aspects of the software life cycle in the area of interactive systems. The described approach showed that: • The approach is completely formalised and most of the proof obligations are proved automatically. The other ones needed only few steps of proof. They allow controlling the development of the whole program. • It is possible to check properties of the specifications, thanks to the weakening of the preconditions (Aït-Ameur et al., 1998a). • Reverse engineering aspects can be handled with this approach and the specifications of already existing programs can be used to develop new ones. Therefore, reusability issues appear. • The specifications are incrementally built, in contrast with state based approaches. Indeed, programming in the large operator allows to compose abstract machines and therefore to build more complex specifications. Yet, this process needs to follow a given methodology issued from the area of interactive system design.

However, several open issues raised from this work: • There is a need to merge both state models and B models in heterogeneous approach. We will get the benefits of both the developments aspects and the model checking ones. • The validation aspects need to be tackled in the context of B. There seems to be a possibility to generate tests from such B specifications. • The B specifications must be developed, in an ascending manner for linking the task analysis to the derivation of specifications and in a descending manner to show the refinement the specifications to implementation.

Finally, we plan to adapt the B approach to the different architectures proposed in the area of interactive systems for handling the formal specification design

Figure 1 .

 1 Figure 1. From the left to the right, The Post-It® block, the three icons (Post-It® block, User, and Post-It®), and the Post-It® Note itself, together with his active areas.

  S2]P <==> [S1]P and [S2]P [PRE E THEN S END ]P <==> E and [S]P [ANY v WHERE E THEN S END]P <==> ∀ v (P =>[S]P) [x:=E]P <==> P(x/E)

(

  aa : 1..max_mouse_position_wide & bb : 1..max_mouse_position_high) is used to prove the invariant assertion (1) in the clause INVARIANT.

  post_it_window_status(get_the_post_it_visu(pp)) = displayed & post_it_mouse_state(get_the_mouse(pp)) = down & block_state = block_open & The block of Post-It® must be open, otherwise the window of a Post-It® Note cannot be moved. post_it_visu_with_mouse_creation(pp) = TRUE & post_it_visu_creation(get_the_post_it_visu(pp)) = TRUE & post_it_mouse_creation(get_the_mouse(pp)) = TRUE &

  THENmove_window_position(get_the_post_it_visu(pp),aa,bb)|| Move_mouse_with_drag(get_the_mouse(pp),aa,bb) END

"Post-it" is a registered trademark of 3M


Yamine Ait-Ameur
email: yamine@ensma.fr

Patrick Girard
email: girard@ensma.fr

Francis Jambon
email: jambon@ensma.fr

A Uniform Approach for Specification and Design of Interactive Systems: the B Method

Keywords: B method, specification refinement, software architecture, interaction properties verification, case study, specification of interactive system max_post_visu, max_post_it_wide, max_post_it_high, PROPERTIES

We have experienced the B Method on a case study which was defined by the French working group on formalisms for interactive systems, i.e. a Post-It® Notes like collaborative application. This experience showed that the B approach allows to cover the description, the formal specification, and the design of each component of basic architecture models, i.e., the five components of the Arch model. Moreover, it has shown that the proposed approach is capable to formally handle large case studies and generate proof obligations which, when proved -automaticallyallows to assert the correctness of the development, and the checking of several user requirements.

Introduction

The past four editions of DSV-IS Workshops have largely focused on formal specification for Interactive Systems. The first approaches attempted to define new semi-formal notations for parts of interactive system design, such as UAN [START_REF] Hix | [END_REF] or MAD [Scapin & Pierret-Golbreich 1990] without defining specific models. The expressive power of these notations is clearly correlated to the domain they are planned to cover, but their formal semantics remains undefined. Conversely, the major researchers' efforts during the past few years have been to endeavour the use of well-known formalisms in interactive system design, such as the Z-notation [Johnson 1995], Petri nets [Accot, Chatty, & Palanque 1996], or functional approaches, whose semantics is clearly defined. However, most of these approaches lead on interactive models such as the York Interactors [Duke & Harrison 1993b], Interactive Cooperative Objects [Palanque 1992] or the CNUCE model [Paterno' 1994 ;Paterno' & Faconti 1992].

Our goal in this work is to explore a third approach: we suggest using a welldefined formal method in interactive design context, without defining or using any interactive model. We propose the B Method [Abrial 1996] which is a model description oriented formalism, such as VDM [Bjorner 1987] or Z [Spivey 1988]. The choice of this method was motivated by the existence of a complete software development tool supporting it [Steria méditerranée 1997]. We tried it out on a case study which has been defined by the French working group on formalisms for highly interactive systems [START_REF] Palanque | [END_REF]: a Post-It® Notes like collaborative application. This paper is organised as follows. The first section discusses some formal approaches that have been studied in the design of interactive systems context. We particularly focus on the scope and the goal of these approaches (specification, validation, or verification) and on the tools that support these methods. The second section describes the case study we have chosen. The third section presents the B method and illustrates it with one abstract machine of the functional core of our case study. Then, the fourth section details the B expression of specific interactive features from the case study. Last, we conclude this paper giving briefly our results either from the formalisation or the verification point of views.

formal approaches overview

As we stated in the introduction, a lot of ad hoc formalisms have been defined for Interactive System description or verification. MAD (Méthode Analytique de Description des Tâches) [Scapin & Pierret-Golbreich 1990] is first and foremost a method for task analysis. The typical user of the MAD method is a human factors specialist. The goal of a MAD study is to collect the set of user's tasks -computerized or not. Recently, the method has been extended to the logical presentation level of user interfaces by the MAD*/SSI models [Gamboa Rodrígez & Scapin 1997]. Supported by a set of tools, IMAD*/ALACIE, the method now bridges the gap from tasks to interaction. UAN (User Action Notation) [START_REF] Hix | [END_REF] proposed another approach: it focus on the description of the interaction level of graphic user interfaces. For example, a basic action of a UAN description is pointing an object with the mouse. In XUAN [Gray, England, & McGowan 1994], the temporal relationships of UAN have been extended, and a subset on XUAN descriptions, eXUAN [McGowan 1995] may be partially executable. UAN may express the same temporal relationships as MAD, but does not provide any methodology to extract them. The well-known GOMS model (Goals, Operators, Methods, Selections) [Card, Moran, & Newell 1983] is meant for the predictive evaluation of interaction between the final system an expert user. The GOMS' tasks are ranked among their duration and complexity. Duration is also one of the main results of a GOMS evaluation.

On the opposite, strongly correlated to Interactive Model definition, several approaches have used well-known formal systems or notation in order to address validation and verification issues. Classical Petri net formalism has been adapted to interactive needs in the ICO model [Palanque 1992], and model oriented Z notation has been used in the York Interactors [Duke & Harrison 1993a ;Duke & Harrison 1993b]. LOTOS has been used in the CNUCE model [Paterno' 1994 ;Paterno' & Faconti 1992]. The last edition of DSV-IS Workshop discussed the actual use of formalisms. Two major needs emerged: verification and validation [Fields, Merriam, & Andy 1997], also called 'verification of implementations against their specifications' and 'verification of specification properties' [START_REF] Campos | [END_REF]. In fact, most of the results focused on the second problem, that is ensuring the correctness of specification. In the review of Campos and Harrison, a framework for the classification of user interface properties has been defined. The current tendency seems today to attempt to correlate different formalisms to cover the aspects of interactive systems. In fact, while the major part of these approaches addresses the validation of specification, using tools appears to be difficult: they do not exist, or are limited in use. When using different formalisms, articulating them together is also very difficult.

In opposite to these options, we will explore the way of using a unique formal notation, suitable for proving, and, so doing, to fulfil verification requirements: the B method. It provides a uniform setting to describe all the parts of an interactive system.

The case study

Our case study is a cooperative version of a Post-It® Note software. It appears on the screen as a Block which can be iconified, but cannot be moved. Clickable areas allow direct manipulation of the block, for iconification, and close (quit). It is possible to enter text into the Post-It® Note on the block, which always exists. Last, it is possible to detach the upper Post-It® Note from the block, and then to drag it anyway. The Post-It® Notes themselves have a similar behaviour, that differs in four ways: (1) the detach area is restricted to a drag command area, (2) the close area becomes a kill area, (3) a resize area is defined in the lower-right corner, corresponding to a standard resize behaviour, and (4) a send behaviour is defined. This behaviour consists in emitting the Post-It® to a receiver which is visualized as a special icon. The interactive trigger is a drop (mouse up event) onto the icon. In this work, we study more particularly the interactive behaviours of the block and the Post-It® Notes. We focus on direct manipulation of these two classes of objects, and we do not expand the "receivers" point of view. We leave the text inputs, that are restricted to "string input". On the opposite, we focus on the mouse actions and their relations with the representation and the behaviour of objets.

The B-Method

Among the increasing number of formal methods that have been described during the last decade, model oriented methods, such as VDM, Z or B, seem to have a good place. These methods are based on model description. They consist in defining a model by the variable attributes which characterize the described system, the invariants that must be satisfied and the different operations that alter these variables. Starting from this observation, Z method uses set theory notations and allows to encode the specifications in a structure named schema. Like VDM, it is based on preconditions and postconditions [Hoare 1969 ;Hoare, et al. 1987]. Moreover, VDM allows the generation of a set of proof obligations which simplify the use of the method regarding to Z. In opposite, B is based on the weakest precondition technique of Dijkstra [Dijkstra 1976]. Starting from this method, J.R. Abrial has defined a logical calculus, named the generalized substitutions calculus. Notice that our choice is B. This choice is motivated by the fact that B is supported by tools which allow a complete formal development. Moreover, since it is based on the weakest precondition calculus, B helps to prove the termination.

The abstract machine notation

The abstract machine notation is the basic mechanism of the B method. J.R. Abrial defined three kinds of machines identified by the keywords MACHINE, REFINEMENT and IMPLEMENTATION:

• MACHINES represent the upper level of a program development.

They represent the higher level of abstraction. They describe the formal specification of a system. • REFINEMENT machines are intermediate steps. They are less abstract than the MACHINES. They are used to refine the MACHINES into structures that are approaching more and more the programming language level. • Finally, IMPLEMENTATIONS are the last development level.

They represent the algorithms that implement the specification described at the MACHINE level. When proved, IMPLEMENTATIONS can be translated into a program written in a given programming language.

Note that the development is considered to be correct only when every refinement is proved to be correct with respect to the semantics of the B language. Gluing invariants between the different MACHINES of a development are defined and sets of proof obligations are generated. They are used to prove the development correctness.

Description of abstract machines

Several important clauses have been described by J.R. Abrial for the definition of abstract machines. Depending on the clauses and on their abstraction level, these clauses can be used at different levels of the program development. In this paper, a subset of these clauses has been used for the design of our specifications. We will only review these clauses. A whole description can be found in the B-Book [Abrial 1996]. The following table shows the syntax of the machines we are using in our case study. Other syntax possibilities are offered in B, and we do not intend to review them in this paper, in order to keep its length short enough.

MACHINE EXTENDS SETS CONSTANTS PROPERTIES VARIABLES DEFINITIONS INVARIANT INITIALISATION OPERATIONS END
Briefly, these clauses mean:

• EXTENDS is a clause that allows to import instances of other machines. Every component of the imported machine becomes usable in the current machine. This clause allows modularity capabilities.

• SETS defines the sets that are manipulated by the specification.

These sets can be built by extension, comprehension or with any set operator applied to basic sets. • CONSTANTS defines all the constants that are used in the machine. Notice that the constants described can have any type (naturals, elements of sets, constant functions and so on). • PROPERTIES are logical expressions that are satisfied by the constants described in the previous clause. • VARIABLES is the clause where all the attributes of the described model are represented. In the methodology of B, we find in this clause all the selector functions which allow accessing the different properties represented by the described attributes. • DEFINITIONS is a set of definitions introduced by the user. They are rewritten everywhere they are used in a machine. It allows simplification of machine notation. • INVARIANT clause describes the properties of the attributes defined in the clause VARIABLES. The logical expressions described in this clause remain true in the whole machine and the represent assertions that are always valid. • INITIALISATION clause allows to give initial values to the variables of the corresponding clause. Note that the initial values must satisfy the invariant.

• OPERATIONS clause is the last clause of a machine. It defines all the operations (functions and procedures) that constitute the abstract data type represented by the machine. Depending on the nature of the machine, the OPERATIONS clause authorizes particular generalized substitutions to specify each operations. The substitutions used in our specifications and their semantics is described below.

Semantics of generalized substitutions.

The calculus of explicit substitutions is the semantics of the abstract machine notation. It is based on the weakest precondition approach of Dijkstra. Formally, several substitutions are defined in B. If we consider a substitution S and a predicate P representing a postcondition, then [S]P represents the weakest precondition that establishes S after execution. The substitutions of the abstract machine notation are inductively defined by the following equations. Notice that we did not give the whole substitutions, we restricted ourselves to the ones used for our development. The reader can refer to the literature [Abrial 1996 ;Lano 1996] for a more complete description:

[SKIP]P <==> P [S1 || S2]P <==> [S1]P and [S2]P [PRE E THEN S END ]P <==> E and [S]P [ANY v WHERE E THEN S END]P <==> ∀ v (P =>[S]P) [x:=E]P <==> P(x/E)
The lst one represents the predicate P where all the free occurrences of x are replaced by the expression E.

An example: Post-It®-mess

Based on the definitions, and for the case study previously exposed, a first abstract machine is defined. It is related to the management of messages written on a given Post-It®. This simple machine is used to illustrate the abstract machine notation. In fact, this machine represents the heart of our application, i.e., the functional core. In our case study, it only contains the message written onto the Post-It®. Additionally, a state variable has been defined, which represents different state possibilities for the Post-It® itself (read, destroyed, stored, etc.). Notice that most choice in this specification do not relate to the initial requirements of our case study (which was very unprecise). We give comments over this machine where necessary:

MACHINE POSTIT_MESS SETS POST_MESS; MESS_STATUS = { read, unread, destroyed, stored} CONSTANTS max_post_mess PROPERTIES max_post_mess=card(POST_MESS)
The set POST_MESS represents the set of all the possible messages to be written. This set behaves as a type for messages. The properties clause asserts that its cardinal is given by the constant max_post_mess. Finally, the set MESS_STATUS enumerates the possible states of a message which are interesting for the application we are currently specifying. Variables define the model; the Invariant clause allows the typing of these variables and finally, the Initialisation clause gives their initial values. In this machine, the_post_it_mess is the set of the effectively created messages. It is included (<:) in the set of all the messages. Three functions the_message, message_status and post_it_mess_creation are functions which return the string corresponding to the message content, the status of the message and a Boolean attesting that the message is effectively created. Notice that these functions represent the properties of a message. Moreover, this is a specification based on the definition of selectors.

Below, a set of operations are defined using the PRE THEN substitution which was described before.

OPERATIONS

The create_post_it_mess operation allows the creation of message containing a String mess, with an unread status. The read_message operation allows the reading of a message represented by pp. Its precondition says that the message is created (since it belongs to the set the_post_it_mess) with an unread status and updates its status when reading is achieved. The destroy_message operation allows the destruction of a message represented by pp. Its precondition says that the message is created (since it belongs to the set the_post_it_mess) with an unread or read status. This means that an eventually unread message can be destroyed. The status is then updated to become destroyed. The store_message operation allows the storage of a message represented by pp. Its precondition says that the message is created (since it belongs to the set the_post_it_mess) with an unread or read status. This means that an eventually unread message can be stored. The status is then updated to become stored. Some choice realized here should be discussed. They are independent from any interactive activity, and can be clearly explained. Hence, it is not possible to read twice a Post-It®: reading it lead it to the read status, while being unread belongs to the precondition of "read_post_it". As we will see later, the B method will ensure these choice in the whole application. Notice that all the abstract machines presented in the case study of this paper are designed following this one. It can be used as a template for the description of the other machines.

Strengths of B

The B Method is based on sound and well known semantics since it is based on predicate logic and on the weakest precondition calculus. But one of the major advantages of this approach is the uniform description of the whole development. Indeed, we will show in the reminder of this paper that the same notation is kept to describe every part that constitutes an interactive system. Moreover, this method gives a technique for proof obligation generation, proving, and refining to code.

Proof obligations (PO)

The calculus of generalized substitutions outlined above is applied for each abstract machine defined in the development. Rewriting techniques are applied to achieve this calculus and they lead to a set of proof obligations which need to be proved in order to have a sound and consistent specification and development.

Proofs and proving

When the proof obligations are generated, they have to be proved. For this purpose, a set of proof rules are provided and the developer can achieve the proof of the PO's if they are provable. Moreover, the tools implementing the B Method have an automatic prover which allows to prove a major part of these PO's. The remaining PO's are proved "by hand" using the interactive prover. This approach allows to check the correctness of the specifications with respect to the user needs. Indeed, some of the PO's are definitely not provable if the abstract machine is not well defined. For example, in the previous abstract machine, we cannot store a message which is destroyed. Finally, in our case study, the 17 PO of the POSTIT_MESS abstract machine have all been proved automatically using the "Atelier B" tool [Steria méditerranée 1997].

Refinement: from the specifications to the code

As stated above, the B Method allows not only to support specifications through abstract machines, but it allows the support of refinement and implementations as well. Indeed, it is possible to set the whole development in a common language, with a common semantics and a common proof technique. This is very important since it provides a uniform approach for the description of program developments.

Experimenting the B-Method

In this section, we explain how the interactive viewpoint can be taken into account during a B design. We base our modular decomposition on the ARCH model [UIMS 1992]. In the B terminology, the architectural modules are called "abstract machines". The figure 2 shows the architectural decomposition, with dependencies between machines. We illustrated the previous section with a machine (Post-It-Mess) which belongs to the functional core. This is the normal use of the B-method. In the following subsections, we explain how B can be used to take into account more specific interactive features. Section 5.1. explains the non-interactive aspects of Post-It® visualization. It includes visual states (iconified or not, greyed, hidden, and so on) and is splitted into two "abstract machines", for B convenience (Visu and Visu-without-mouse). The links with the graphical toolbox is not detailed here. Section 5.2. exposes the necessary reverse engineering of the mouse. It is obvious that the existence of a B mouse "abstract machine" would have skipped this phase. Section 5.3. details the integration of mouse and visualization in order to define the dialogue controller of the Post-It®. Section 5.4. shows how functional core requirements and dialogue requirements can mix to build the whole application. Positioning this machine conforming to the ARCH model is not straightforward. It is concerned with domain adaptation, but also with dialogue control. So, using "slinky" facilities of the ARCH model, we propose including it at the boundary of the domain adapter and the dialogue controller. Lastly, we expose in section 5.5. the practical use of B-Tools, and demonstrate the proving process. Notice that names in figure 2 do not match actual names in the B development, for graphical space reasons. We will ensure the correspondence as needed.

The Post-It® Visualization: the POSTIT_VISU_WITHOUT_INT machine

Two machines were specified for the visualization of the windows. The first one is the POSTIT_VISUALIZATION abstract machine (visu in fig. 2) which manages the state of the windows from display point of view. Indeed, a set named SCREEN_STATE={displayed, hidden, iconified, eliminated} allows recording all the possible states of the windows. Moreover, this abstract machine contains operations like update_hidden which specifies the refreshment of the screen. The second machine (visu without mouse in fig 2), extends the previous one and allows to manage the windows without dealing with any kind of interaction. It is a high level abstraction of a subset of the toolkit. The previous sets describe all the values of the possible states of a window starting from colours, blinking, emitting sounds, reaction and the state of the whole block of Post-It®'s.

These variables describe the accessors to the different components of a window. The the_post_it_visu is the set of all the windows effectively created, and get_new_post, block_state and post_it_window_status are the function which respectively imports a window from the POSTIT_VISUALIZATION machine, gives the state of the block and computes the status of the window from the one on the imported window. The previous logical expression is an important invariant. It states that all (!) the windows of the set the_post_it_visu have their upper-left corner in the screen. This invariant is conserved and proved for all the operations. We will now describe the "move_window_position" action, and every elements it uses. In this machine, move_window_position is not strictly constrained. For example, it is possible to partially quit the visualization window while moving a Post-It®. This constraint will be put later on. We only take into account the constants, variables and invariants that are needed by move_window_position. The previous preconditions say that the new coordinates of the upper-left corner of a window (aa,bb) must belong to the screen, that the window pp is effectively created (belongs to the_post_it_visu set), that the block of Post-Its is effectively open and that the window can be displayed or hidden.

From these previous precondition, we can infer the following properties:

• a window is never moved if it is iconified,

• a window is never moved if the block is not open,

• a window will never have its upper-left corner outside from the screen. This is very important for the window manipulation. Here, a parallel substitution is used. It says that after executing this operation the new coordinates of the upper-left corner become (aa, bb) and that the operation update_hidden is called. This last operation is called in order to update the status of the windows that become hidden or displayed after the current window has been moved.

Reverse engineering of the mouse: the POSTIT_MOUSE machine (mouse in fig 2)

In order to allow the interaction using a mouse, thanks to reverse engineering techniques, we have extracted a set of specifications which describe the behaviour and the actions performed on the mouse. Let us briefly summarize them.

MACHINE POSTIT_MOUSE

SETS POST_MOUSE; MOUSE_STATE ={up, down , clicked}

The mouse can be in three states. Without loss of generality, we have voluntarily omitted the other states because they are not used in our application. Notice that they could have been included. These constants define the size of the screen for the window together with the default position for a mouse. For a given mouse in the set the_post_it_mouse, the previous accessors define a set of functions which allow to retrieve the coordinates of a mouse, its state and its creation. Several operations on the mouse (creation, moving, clicking, and so on ... ) are defined below.

CONSTANTS

OPERATIONS

pp <--create_mouse_position= ... Move_mouse_with_drag(pp, aa,bb)= ... move_mouse(pp, aa, bb)= ... mouse_up(pp)= ... mouse_down(pp)= ... mouse_clicked (pp)= ... END This reverse engineering task to re-design the mouse specification is a crucial phase in our work. It allows to use the B language in a uniform manner even for already designed programs. However, this steps of development needs to be achieved for other parts of an interactive application (e.g. keyboard).

The interaction: Post-it-visu-with-int

The following abstract machine, named POSTIT_VISU_WITH_INT_MOUSE (visu with mouse in fig 2), allows the use of mouse interaction on the windows. Therefore, this machine extends the two machines corresponding to windows and mouse.

MACHINE POSTIT_VISU_WITH_INT_MOUSE EXTENDS POSTIT_MOUSE , POSTIT_VISU_WITHOUT_INT SETS POSTIT_VISU_WITH_MOUSE CONSTANTS max_post_it_visu_with_mouse PROPERTIES max_post_it_visu_with_mouse = card(POSTIT_VISU_WITH_MOUSE) & screen_wide = max_mouse_position_wide & screen_high = max_mouse_position_high & max_post_it_wide=max_mouse_position_wide & max_post_it_high=max_mouse_position_high
The previous properties express that the screen for the mouse and for the windows are of the same dimensions. These properties are mandatory to prove the correctness of the development from the positions point of views. The set the_post_it_visu_with_mouse records all the windows manipulated by a mouse. The selectors define a set of functions which allow to extract the properties of a given window which is manipulated by a mouse. It gives the window using the get_the_post_it_visu function and the mouse using the get_the_mouse function. Let us give the details of the action move_window_with_mouse which allows to move a window combining the interaction of the mouse. This action has a set of preconditions which needs to be valid before the action is performed. They are commented below. The new coordinates of the upper-left corner of the window must define a point in the limits of the screen.

block_state = block_open &

The block of post'its must be open, otherwise the window of a post'it cannot be moved.

post_it_visu_with_mouse_creation(pp)=TRUE & post_it_visu_creation(get_the_post_it_visu(pp))=TRUE & post_it_mouse_creation(get_the_mouse(pp))=TRUE &
The different elements manipulated by the operation (mouse, a window, a window with mouse interaction) must be already created.

post_it_window_status(get_the_post_it_visu(pp))=displayed & post_it_mouse_state(get_the_mouse(pp))= down &
The mouse must be in a state down and the window must be displayed. The mouse position must be in the moving zone delimited previously. The window is moved by calling the move_window_position action present in the POSTIT_VISU_WITHOUT_INT and the mouse is also moved bt the action move_mouse_with_drag of the machine POSTIT_MOUSE. Notice, that this action is one of the actions which combines the mouse toolkit and the window manager tool kit.

END

The previous abstract machine gives supplementary preconditions on the objects. These preconditions imply the ones of the corresponding operations in the machines imported by extension. Therefore, the prover is capable to complete the proof of correctness. This is an important issue of the B method which shows that B is not only capable structure the development of specifications, but it allows the structuration and the modularization of the proofs. Finally, this mechanism of weakest precondition conserves the coherence of the whole specification.

This previous machine has shown that it is not possible to :

• move a window with a mouse whose position is not in the moving zone,

• move a window if there is no mouse, • move a window if it is eliminated. Note that this property is inherited form the imported machine. • …

Complementary machines: POSTIT_EMISS and POSTIT_USERS

Two other machines are necessary to have a complete development of the specifications.

• the POSTIT_EMISS abstract machine defines a simple protocol allowing to emit, receive and create messages. These messages are intended to be linked to a Post-It window in the final application. In this machine, the messages have the state emitted, received, non_emitted and so on. Operations like emit_post, receive_post and create_post are described in this machine.

• the POSTIT_USERS abstract machine is devoted to the management of the users. Each user is defined by an icon of constant dimension, which can be moved on the screen.

Notice that we have restricted these two machine to simple operations. The management of the protocol of emission and users is not a main part of this application.

The final application: POSTIT_FINAL

After having defined all the different components of our application, extracted from figure 2, we are capable to describe the whole application. This application is an extension of all the machines described above. It defines the set of Post-Its and variables -selectors-which extract the objects coming from each submachine, i.e., extended machines. The set the_post_it is the set of all the effectively created Post-Its. The other functions are used to access the different components of the objects. We omit describing the invariants of this machine.

Let us describe the use of the emission of a Post-It. The user creates a Post-It, drag it on the icon corresponding to the user and then it is emitted. The icon corresponding to the receiver must be created. This precondition invokes an operation of the POSTIT_USERS abstract machine. The icon is effectively visible in the screen i.e. it is not outside the limits of the screen. The message contained in this Post-It must be unread.

emission_status(get_the_post_it_emiss(pp))=non_emitted &

The status of the message to be sent is not emitted. The positions of the Post-It and of the mouse must be in the screen. Moreover, the moving zone of the Post-It must be visible in the screen. The Post-It is emitted and the window is moved using the move to the position of the receiver identified by the icon_receiver user. The message becomes emitted, the window Post-It is eliminated and the mouse stays on the position of the receiver.

All the other operations have been described in this machine. The complete case study is available on our web site. We cannot insert it in whole in the present paper.

Proofs

For all the development, the proof obligations have been generated. They all have been automatically proved. However, this specification has not been built at the first attempt. We had to enrich the preconditions and to remove other preconditions. Indeed, the prover behaves following:

• preconditions are not complete, therefore the proof cannot be achieved, • preconditions are contradictory, then the user has to make new choices and to check the requirements.

Finally, about 160 proof obligations are generated for this application. We had to prove only 4 proof obligations using the interactive prover, i.e., "by hand". This shows that when the application is well specified following sound software engineering concepts, the proof phase can be considerably reduced.

Conclusion and future work

In this paper, we expose the use of the B method in the area of HCI. We relate it to other approaches in this area: it can be considered as a third approach between the definition of ad hoc new formalisms and the use of well defined formal notations through HCI models. It consists in giving a model-independent method that can be customized to specific HCI models.

The great strength of the B method is its ability to refinement. That is the possibility to finally derive concrete programs form abstract specifications. While doing that, one part of the main objective of formal method can be achieved: it is to say the verification that implementation satisfies its specification. This work has shown, that interaction properties can be expressed a priori at any level of the chosen architecture model -ARCH in our example. We show in this work that interactive specific properties, like visualization or dialogue properties can be expressed, and, so doing, ensured. For example, ensuring that a Post-It® cannot leave its visualization screen is possible. This is made via formal proofs established by the use of tools. This work exposes preliminary results. We do not claim that the B method is able to solve every problem we may encouteer in DSV-IS. Nevertheless, it seems to be a promising way of investigations. We have now to work in three directions: first, defining a specific method to help designers to build interactive applications is essential; second, and probably linked to the first point, it seems important to relate our process to HCI models, such as these we noticed upper. Correlations with other formalisms should be very important too, in order to help to validate our B-specification against users needs. This step, which is obviously out of the scope of formal method senso strictu, supposes translations between B-formal semantics and understandable users' needs representation. Last, there is a strong need for building reusable abstract machines once for all in the HCI area. The possibility to reuse these machines would considerably reduce testing and verifying costs.

Figure 1 :

 1 Figure 1: From the left to the right, The Post-It® block, the three icons (Post-It® block, User, and Post-It®), and the Post-It® itself, together with their active areas.

  pp <--create_post_it_mess(mess)= PRE the_post_it_mess /= POST_MESS &Because of the limit, we must ensure that we can create another Post-It.

  store_post_it(pp) = PRE pp : the_post_it_mess & (message_status(pp)=unread or message_status(pp)=read ) THEN message_status(pp):=stored END END

Figure 2 :

 2 Figure 2: architectural ARCH-like decomposition of cooperative Post-It® Notes application, with the reference to the ARCH model

  THENmove_window_position(get_the_post_it_visu(pp),aa,bb) || Move_mouse_with_drag(get_the_mouse(pp),aa, bb)

  OPERATIONSpp <--create_post_it (pp_emiss, pp_visu,pp_mess )= ... emit_post_it(receiver,icon_receiver,sender,pp)= PRE receiver : NAT1 & sender : NAT1 &The sender and the receiver are valid. They are defined as a positive integer.icon_receiver : the_post_it_users & post_it_user_creation(icon_receiver)=TRUE &

  It, the corresponding mouse, the corresponding window associated to the mouse and the corresponding window without mouse are effectively created. (pp))=sender & The user which sends the Post-It is the one who created this post-it. message_status(get_the_post_it_mess(pp))=unread &

  The coordinates delimiting the moving zone of the window must belong to the screen i.e. must appear in the screen.

	x_post_it_position(get_the_post_it_visu(pp))+5 :
	1..max_mouse_position_wide &
	y_post_it_position(get_the_post_it_visu(pp))+5 :
	1..max_mouse_position_high &
	x_post_it_window(get_the_post_it_visu(pp))-5 :
	1..max_mouse_position_wide &
	x_post_it_mouse_position(get_the_mouse(pp)):
	x_post_it_position(get_the_post_it_visu(pp))+5..
	x_post_it_window(get_the_post_it_visu(pp))-5 &
	y_post_it_mouse_position(get_the_mouse(pp)):
	y_post_it_position(get_the_post_it_visu(pp))..
	y_post_it_position(get_the_post_it_visu(pp))+5

  No Post-It can be sent if the block of Post-Its is not open.The current Post-It to be sent must be displayed.The associated mouse must be in a down state.

	block_state=block_open &
	post_it_window_status(get_the_post_it_visu(
	get_the_post_it_visu_with_mouse (pp)))=displayed &
	post_it_mouse_state(get_the_mouse(
	get_the_post_it_visu_with_mouse (pp)))=down &
	x_post_it_position(get_the_post_it_visu(
	get_the_post_it_visu_with_mouse (pp)))+5 :
	1..max_mouse_position_wide	&
	x_post_it_window(get_the_post_it_visu(
	get_the_post_it_visu_with_mouse (pp)))-5 :
	1..max_mouse_position_wide	&
	y_post_it_position(get_the_post_it_visu(
	get_the_post_it_visu_with_mouse (pp)))+5 :
	1..max_mouse_position_high	&
	x_post_it_mouse_position(get_the_mouse(
	get_the_post_it_visu_with_mouse (pp))) :
	x_post_it_position(get_the_post_it_visu(
	get_the_post_it_visu_with_mouse (pp)))+5
	x_post_it_window(get_the_post_it_visu(
	get_the_post_it_visu_with_mouse (pp)))-5	&
	y_post_it_mouse_position(get_the_mouse(
	get_the_post_it_visu_with_mouse (pp))):
	y_post_it_position(get_the_post_it_visu(
	get_the_post_it_visu_with_mouse (pp)))
	y_post_it_position(get_the_post_it_visu(
	get_the_post_it_visu_with_mouse (pp)))+5

& * max_post_it_high=250 & VARIABLES the_post_it_visu, get_new_post , block_state, post_it_window_status,