Christine Azevedo Coste
email: christine.azevedo@inria.fr

Winfried Mayr
email: winfried.mayr@meduniwien.ac.at

Manfred Bijak
email: manfred.bijak@meduniwien.ac.at

Antonio Musarò
email: antonio.musaro@uniroma1.it

Ugo Carraro
email: ugo.carraro@ospedalesancamillo.net

FES in Europe and Beyond: Current Translational Research

Keywords: FES, denervated muscle, mobility impairment, aging, prevention and assistive technology, rehabilitation, biomedical technology

Ability of neural and muscle tissues to respond to external Electrical Stimulation (ES) is the sound biological basis of established therapeutic managements of mobility impairments, assistive technology and of the current research activities aimed to extend its clinical applications. All the body tissues, however, respond to ES and, indeed, the most successful application of Functional Electrical Stimulation (FES), though known under other names or acronyms, is the electrical stimulation of the heart to revert or limit effects of arrhythmias (Pace-makers and Defibrillators). We would like to list and discuss here results of current research activities on FES, in particular those published in the European Journal of Translational Myology after presentation during the 2015 XI Meeting of the Italian Institute of Myology (IIM), [START_REF]-Reggio Emilia, Italy, Abstracts[END_REF] the 2016 Spring PaduaMuscleDays, 2 the 2016 Vienna FES Workshop and the 2016 International Conference of IFESS society held in Montpellier France. [START_REF] Azevedo-Coste | Ejtm Special: 20th Conference of the International Table 7[END_REF] In Table 1 are listed the subtopics of FES research and applications published in the European Journal of Translational Myology that will be discussed in the following sections. They are only some of a much longer list that represent the many subtopics of FES, i.e., i) Biological bases of FES for Neuromuscular Mobility Impairments; ii) FES for Arm, Leg and Body Motility; iii) FES for Swallowing, Micturition, Gastric function restoration; iv) FES as a countermeasure of muscle weakness and atrophy; v) FES and mechanical devices (wearable robots, cycles...); vi). FES for Pain Management; vii) Sensor interfaces to control FES (BCI, EMG, IMUand more); viii) FES advanced technology to improve efficiency and selectivity.

XI Meeting of IIM, Italy and 2016 Spring PaduaMuscleDays

Among other scientific topics, during the 2015 IIM meeting the molecular mechanisms of muscle atrophy, wasting and diseases were deeply discussed. One of the remarkable features of skeletal muscle is, indeed, the capacity to adapt its morphological, biochemical, and molecular properties in response to several events. The continual synthesis and degradation of cell proteins is the result of normal intracellular metabolism and represents an important homeostatic function of muscle tissue. Muscle wasting, in contrast, is a process in which the delicate balance between anabolic and catabolic processes is impaired. In recent years, age-related diseases and disabilities have become of major interest and importance for health. The pathological process associated with aging is known as sarcopenia, characterized by a progressive loss of mobility and a decrease of the life quality. Society at large will benefit from delaying, as much as possible, the sarcopenia economic and social consequences. In elderly, muscles become atrophic (loss in muscle mass) and weaker (loss in muscle force), more susceptible to damage and consequently regenerate and recover more slowly than in younger individuals. [START_REF] Carraro | Biology of Muscle Atrophy and of its Recovery by FES in Aging and Mobility Impairments: Roots and By-Products[END_REF] During the IIM-Myology meeting, several signaling pathways have been discussed as key maintenance regulators of muscle mass or triggers of muscle wasting. [START_REF]-Reggio Emilia, Italy, Abstracts[END_REF] Nevertheless, despite the new discoveries in this field, no effective therapies are still available. Therefore, it is of fundamental importance to gain greater knowledge about the cellular and molecular processes controlling this debilitating condition to find effective countermeasures. [START_REF] Carraro | Recovery from muscle weakness by exercise and FES: lessons from Masters, active or sedentary seniors and SCI patients[END_REF] FES is one of the approaches that attracted much attention in the last 10 years, based on practical considerations: i) ES can be applied to people that cannot carry out normal physical activity; ii) it modulates similar factors associated with physical exercise; iii) it improves muscle mass and function in sedentary elderly people. In particular, it has been demonstrated that ES activates, at the level of skeletal muscle, the growth factor IGF-1, which in turn promotes anabolic pathways increasing protein synthesis while reducing protein degradation. IGF-1 and FES appear to be responsible for the increase in muscle performance. Interestingly, ES, similarly to physical exercise, attenuates the functional decline associated with aging, improving muscle strength and mass, maintaining the overall size of muscle fibers (decreasing during aging), activating satellite cells and guaranteeing muscle adaption. [START_REF] Kern | Longterm denervation in humans causes degeneration of both contractile and excitation-contraction coupling apparatus, which is reversible by functional electrical stimulation (FES). A role for myofiber regeneration?[END_REF] Based on several evidences, we can also speculate that FES mimics the effects of endurance training, since they do not induce muscle damage, and activate comparable molecular networks. Many of these mechanisms were discussed in recent papers published in the European Journal of Translational Myology and during the 2016Spring PaduaMuscleDays as the main determinants of the positive effects of physical exercise and FES when applied to therapeutic and rehabilitation strategies aimed to prevent or revert the consequences of aging and mobility impairments. stimulation. The notion of hybridity can also be seen from the perspective of the multidisciplinary face of the field. Three special sessions were dedicated specifically to this theme with articles associating FES to 1) wearable robotics, 2) CNS stimulation and 3) cycling devices. Electrical stimulation can be applied in a large panel of situations and some of the emerging applications have been presented in the special session: "Emerging FES interventions, with original and promising studies". Electrical stimulation activates both efferent and afferent pathways. This property is extremely appealing in the context of functional rehabilitation and neurological recovery. The engagement of patients is mandatory to increase the potential of the training. This was the object of the special session "FES and fun" which explores different approaches to motivate the patients to actively participate into their rehabilitation protocol. In the regular sessions, articles insisted in the recent advances in technology to improve stimulation efficiency and selectivity, to explore new modalities and applications of FES. Engineers and Clinicians demonstrated in their articles the importance and potential of this very active research field. We wish to thank all authors of the articles that have contributed to EJTM (Tables 2 to7)

and for making the Ejtm Special Section on 2016 IFESS Conference an exciting and intriguing read. 9,16-64

  pathological conditions skeletal muscle loses its adaptability, leading to atrophy and wasting.

Table 1 .

 1 List of subtopics of Functional Electrical Stimulation research and management _________________________________________

	1. Biological bases of FES for neuromuscular
	mobility impairments
	2. FES for upper and lower body mobility
	3. FES for swallowing, micturition, gastric and
	other vital functions
	4. FES as a countermeasure of muscle atrophy,
	weakness and aging
	5. FES combined with mechanical devices
	(wearable robots, cycles and more ...)
	___________________________________________

12th Vienna International Workshop on FES, September 8th-9th, 2016

		The conference started with two Pre-Conference
		Courses "FES of Denervated Muscles -An Essential
	The "Vienna Workshop on Functional Electrical Stimulation" was held the first time in 1983 in Vienna, Austria. Since then it is organized by the Center for Medical Physics and Biomedical Engineering (former: Center for Biomedical Engineering and Physics), the Medical University of Vienna and the Austrian Society for Biomedical Engineering every three years in Vienna or locations close to Vienna. This scientific conference provides a platform for researchers to present and discuss their recent work whilst visitors can expect a representative and actual overview of the state of the art of FES. Traditionally, parallel sessions are avoided. Since the 10th Workshop (2010) all conference proceedings are available on DVD: "30 years of FES	Therapeutic Option after Peripheral Nerve Lesion", (Organizers: Mayr W., Krenn M., Biowski P., all from Vienna, Austria) and "Non invasive posterior root stimulation for assessment and modulation of spasticity and motor control" (Organizers: Mayr W., Krenn M., both Vienna, Austria and Dimitrijevic M., Houston, TX, USA) designed as hands-on workshops with a comprehensive introduction on physiological, clinical and technical basics, safety issues, handling of equipment, guidelines and protocols. As FES of denervated muscles differs fundamentally from classical neuromuscular ES, the main particularities were addressed in an open interactive discussion, scientifically based on the strong clinical, functional and structural results of the EU Program
		RISE 6-8 . 6-8

history on one click" (http://fesworkshop.org). This year's Workshop was held at the renovated Campus of the Medical University Vienna, a place with a long history in medical research.

Table 2 .

 2 European Journal of Translational Myology, 2016. FES papers: Subtopic 1. Biological bases of FES for neuromuscular mobility impairments __________________________________________________________________________________________ Review Barberi L, Scicchitano BM, Musaro A. Molecular and Cellular Mechanisms of Muscle Aging and Sarcopenia and Effects of Electrical Stimulation in Seniors. Eur J Transl Myol 2015;25:231-6. doi: 10.4081/ejtm.2015.5227. 16 Article Tramonti C, Rossi B, Chisari C. Extensive functional evaluations to monitor aerobic training in Becker Muscular Dystrophy: A case report. Eur J Transl Myol 2016;26:81-6. 17 Article Hiroux C, Vandoorne T, Koppo K, De Smet S, Hespel P, Berardi E. Physical activity counteracts tumor cell growth in colon carcinoma C26-injected muscles: an interim report. Eur J Transl Myol 2016;26:67-75. 18 Review Coletti D, Daou N, Hassani M, Li Z, Parlakian A, Serum Response Factor in muscle tissues: from development to ageing. Eur J Transl Myol 2016;26:87-92. 19 Article Guiho T, Azevedo Coste C, Delleci C, Chenu J-P, Vignes J-R, Bauchet L, Guiraud D. An intermediate animal model of spinal cord stimulation. Eur J Transl Myol 2016;26:150-4. 20 Article Totzeck A, Mummel P, Kastrup O, Hagenacker T. Clinical features of neuromuscular disorders in patients with N-type voltage-gated calcium channel antibodies. Eur J Transl Myol 2016;26:301-6. 21 Article Carotenuto F, Coletti D, Di Nardo P, Teodori L.-linolenic acid reduces TNF-induced apoptosis in C2C12 myoblasts by regulating apoptotic proteins expression. Eur J Transl Myol 2016;26:317-22. 22ConclusionsAltogether, evidence demonstrates that FES basic, translational and clinical research in Europe and beyond is alive. Translation of results to clinical therapies for a large population of patients is much more than a hope.

	Review Carraro U, Kern H. Severely atrophic human muscle fibers with nuclear misplacement survive many years
		of permanent denervation. Eur J Transl Myol 2016;26:76-80. 15
	Article	Zampieri S, Mosole S, Löfler S, et al. Physical Exercise in Aging: Nine Weeks of Leg Press or Electrical
		Stimulation Training in 70 Years Old Sedentary Elderly People. Eur J Transl Myol 2015; 25: 237-242. doi:
		10.4081/ejtm.2015.5374. 9

Table 6 .

 6 European Journal of Translational Myology, 2016. FES papers of Subtopic 4. FES as a countermeasure of muscle weakness, atrophy and aging _________________________________________________________________________________________ Myo News XII IIM -Myology Meeting, October 1st to 4th 2015 -Reggio Emilia (Italy), Abstracts. Eur J Transl Myol 2016;26:2-24. 1 Myo News 2016Spring PaduaMuscleDays, April 13th to 16th -Terme Euganee, Padova (Italy), Abstracts. Eur J Transl Myol 2016;26:37-60. 2 Article Edmunds KJ, Gíslason MK, Arnadottir ID, Marcante A, Piccione F, Gargiulo P. Quantitative Computed Tomography and image analysis for advanced muscle assessment. Eur J Transl Myol 2016;26:93-100. 51 _________________________________________________________________________________________

Acknowledgments

CAC thanks the International Functional Electrical Stimulation society (IFESS) and INRIA for support. Work in the Laboratories of AM has been supported by Telethon (GGP14066) and Fondazione Roma. UC thanks the IRCCS Fondazione Ospedale San Camillo, Venice (Italy) for scientific support and hospitality.

Author's contributions

All authors equally organized the draft and wrote the typescript.

Conflict of Interest

The authors declare no potential conflict of interests.


Kalou Cabrera Castillos

Frédéric Dadeau
email: frederic.dadeau@lifc.univ-fcomte.fr

Jacques Julliand
email: jacques.julliand@lifc.univ-fcomte.fr

Safouan Taha
email: safouan.taha@supelec.fr

Measuring Test Properties Coverage for evaluating UML/OCL Model-Based Tests

Keywords: Model-Based Testing, UML/OCL, temporal property, coverage, model animation

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

Introduction and Motivations

Critical software validation is a challenge in software engineering and a convenient context for Model-Based Testing [START_REF] Beizer | Black-Box Testing: Techniques for Functional Testing of Software and Systems[END_REF]. Indeed, the cost of writing a formal model to support the test case generation phase is made profitable by the necessity of increasing the confidence in the safety and the security of the system. MBT is well-suited to conformance testing, as the model describes the expected behavior of a system. The system under test is then checked against the model on specific execution traces called test cases. A conformance relationship, usually based on the observation points provided by the SUT, is then used to establish the test verdict.

This work is done in the context of the ANR TASCCC project 3 , we are interested in the validation of smart card products security by means of model based tests. The tests are produced by the CertifyIt tool, provided by the Smartesting company 4 . This test generator takes as input model based tests in UML/OCL and generated tests aiming at the structural coverage of the OCL code describing the behaviors of the class operations. CertifyIt is an automated test generator, in the sense that, apart from the model, no further information is required to generate the tests.

We propose to consider user-defined test properties to express test patterns associated to the requirements of the software. The contribution is twofold. First, we propose a test property language based on Dwyer's property patterns [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF] and applied to UML/OCL models. In this context, the considered events are either controllable (the invocation of an operation) or observable (a state predicate becomes satisfied at a given state). The properties describe the apparition of these events, in given scopes. Second, we propose to assist the validation engineer, by measuring the coverage of the property. Indeed, a property exhibits a set of model executions that are authorized, expressed as an automaton. In order to evaluate the exhaustiveness of the testing phase, we measure and report the coverage of the underlying automaton. In addition, uncovered parts of the property indicate which part has not been tested and, as a consequence, on which part the tester should focus his efforts.

The remainder of the paper is organized as follows. Section 2 presents the test generation process of the CertifyIt tool based on the structural coverage of the OCL code. Then, the property language is defined in Sec. 3 and its semantics is provided in Sec. [START_REF] Beizer | Black-Box Testing: Techniques for Functional Testing of Software and Systems[END_REF]. Section 5 defines the notion of property coverage and explains how this action is processed. Finally, we conclude and present the related and future works in Sec. 6.

Test Generation from UML/OCL Models

We present here the test generation principles of the CertifyIt test generation tool. First, we introduce the subset of UML/OCL that is considered and we illustrate it with a simple running example. Then, we present the test generation strategy of CertifyIt.

Considered Subset of UML/OCL

The model aims at being used by the CertifyIt tool, commercialized by the Smartesting company. This tool generates automatically model-based tests from a UML model [START_REF] Bouquet | A subset of precise UML for model-based testing[END_REF] with OCL code describing the behaviors of the operations. CertifyIt does not consider the whole UML notation as input, it relies on a subset named UML4ST (UML for Smartesting) which considers class diagrams, to represent the data model, augmented with OCL constraints, to describe the dynamics of the system. It also requires the initial state of the system to be represented by an object diagram. Finally, a statechart diagram can be used to complete the description of the system dynamics. Concerning modelling, some restrictions apply on the class diagram model and OCL constraints that can be written. The system under test (SUT) has to be modelled by a class, which carries all the operations representing the API provided by the SUT. CertifyIt does not allow inheritance, nor stereotypes like abstract or interface on the classes. Objects can not be created when executing the model. As a consequence, the object diagram, representing the initial state, has to provide all the possible class instances, possibly isolated (i.e., not associated to the SUT object or any other object) if they are not supposed to exist at the initial state.

OCL provides the ability to navigate the model, select collections of objects and manipulate them with universal/existential quantifiers to build boolean expressions. Regarding the OCL semantics, UML4ST does not consider the third logical value undefined that is part of the classical OCL semantics. All expressions have to be defined at run time in order to be evaluated. CertifyIt interprets OCL expressions with a strict semantics, and raises execution errors when encountering null pointers. The overall objective is to dispose of an executable UML/OCL model. Indeed, the test cases are produced by animating the model in order to satisfy a given coverage criterion. Before describing this process, we first introduce a simple running example.

Running Example

We illustrate the UML/OCL models that are considered using a simple model of a web application named eCinema. This application provides a means for registered users to book tickets for movies that are screened in a cinema.

The UML class diagram, depicted in Fig. 1 contains the classes of the application: ECinema, Movie, Ticket and User. The ECinema class models the system under test (SUT) and contains the API operations offered by the application. Several requirements are associated to the system, for example: the user must be registered and connected to access the proposed services, the registration is valid only if the user's name and password are valid and if the user is not already registered, the user must be connected in order to buy tickets, etc.

The initial state contains a single instance of the system under test class eCinema, identified by sut, two instances of movies linked with the sut instance (instanciating the offers association), twenty-five isolated instances of tickets, and two users, one registered (i.e. linked to the SUT using the knows association) and one not registered (isolated instance).

This model contains several operations whose meaning are straightforward: unregister, showBoughtTickets, registration, logout, login, deleteTicket, deleteAllTickets, closeApplication, buyTicket.

Figure 2 shows the OCL code of the buyTicket operation used by an authenticated user to buy a ticket. This operation can only be invoked with a valid movie title and if all the tickets are not already assigned to users. To be successful, the user has to be authenticated, and at least one tickets for the movie should be available. Otherwise, error messages report the cause of the failure. Upon successful execution, an available ticket is chosen and assigned to the user for the corresponding movie, and the number of available seats is decremented.

In the OCL code, there are non-OCL annotations, inserted as comments, such as ---@AIM: id and ---@REQ: id. The ---@AIM:id tags denotes test targets while the ---@REQ: id tags mark requirements from the informal specifications. These tags are used by CertifyIt to know which tags were covered during the execution of the model, and, consequently, inside the test cases.

CertifyIt Test Selection Criterion

Smartesting CertifyIt is a functional test generator that aims at exercising the atomic transitions of the model, provided by the class operations. The CertifyIt context ECinema::buyTicket(in_title : ECinema::TITLES): oclVoid pre:

self.all_listed_movies->exists(m : Movie | m.title = in_title) and Ticket.allInstances()->exists(t : ticket | t.owner_ticket.oclIsUndefined()) post :

---@REQ: BASKET_MNGT/BUY_TICKETS if self.current_user.oclIsUndefined() then message = MSG::LOGIN_FIRST ---@AIM: BUY_Login_Mandatory else let target_movie: Movie = self.all_listed_movies->any(m: Movie | m.title = in_title) in if target_movie.available_tickets = 0 then message= MSG::NO_MORE_TICKET ---@AIM: BUY_Sold_Out else let avail_ticket: Ticket = (Ticket.allInstances())->any(owner_ticket.oclIsUndefined()) in self.current_user.all_tickets_in_basket->includes(avail_ticket) and target_movie.all_sold_tickets->includes(avail_ticket) and target_movie.available_tickets = target_movie.available_tickets -1 and message= MSG::NONE ---@AIM: BUY_Success endif endif Fig. 2. OCL code of the buyTicket operation test generation strategy works in two steps. First, it identifies test targets and, second, it builds a test case that is a trace, composed of successive operation calls, reaching the considered target.

In the first part of the test generation process, the test targets are computed by applying a structural test selection criterion on the OCL code of the class operations (Decision Coverage criterion). Each test target is thus associated to a predicate that describes the set of possible concrete states from which the operation can be invoked. Each test aims at covering a specific target (possibly characterized by a set of @AIM tags). There are three test targets for the buyTicket operation, one for each available @AIM tags.

The second part of the test generation process consists in performing an automated state exploration, from the initial state, in order to reach a state satisfying the state predicate associated to the test target. This sequence is called a preamble. The preamble computation is based on a Breadth First Search algorithms that stops when the targeted state is reached. To obtain the test case, the preamble is concatenated with the invocation of the targeted operation with the appropriate parameter values.

The test selection criterion ensures that one test is built for each target. Nevertheless, some targets may be covered several times, if they are found in the preambles of others targets. Table 1 shows the tests generated for the operation buyTicket displayed in Fig. 1.

Notice that the undetermined state of the test BTTest 3 declared by CertifyIt refers to internal limitations of the tool in terms of depth search bound. Indeed, in our initial state, we specified that the two movies could deliver 20 tickets each, which needs to build a test sequence in which all 20 tickets are already bought. Since this configuration could be reached (the number of ticket instances is set to 25), this message does not conclude on the general unreachability of the test targets.

Since CertifyIt is a functional test generator, it is not intended to cover specific sequences of operations, or states. Nevertheless, the tool provides a means to complete automatically generated tests with test scenarios, built using the simulator (the internal model animator) and exported as test cases.

Test Property Language

The Object Constraint Language is quite similar to first-order predicate logic. OCL expressions are used in invariants, pre-and postconditions. They describe

Test name Test sequence Target

BTTest1 init ; sut.login(REGISTERED USER,REGISTERED PWD) ; @AIM: BUY_Success sut.buyTicket(TITLE1) ; BTTest2 init ; sut.buyTicket(TITLE1) ; @AIM: BUY_Login_Mandatory BTTest3 declared as ''Undetermined'' @AIM: BUY_Sold_out Table 1. Generated tests for the buyTicket operation a single system state or a one-step transition from a previous state to a new state upon the call of some operation.

Several OCL extensions already exist to support temporal constraints [START_REF] Cengarle | Towards OCL/RT[END_REF][START_REF] Flake | Formal Semantics of Static and Temporal State-Oriented OCL Constraints[END_REF][START_REF] Ziemann | An OCL Extension for Formulating Temporal Constraints[END_REF]. They only add to OCL unary and binary temporal operators (e.g., always, next and until) in order to specify safety and liveness properties. Unfortunately, most developers are not familiar with temporal logics and this is a serious obstacle to the adoption of such OCL extensions. We propose to fill in this gap by adding to OCL a pattern-based temporal layer to ease the specification of temporal properties.

A temporal extension to UML/OCL

For specifying the temporal aspects of system properties, we adopt the work of Dwyer et al. [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF] on specification patterns for temporal properties. Although formal methods are largely automated today, most engineers are not familiar with formal languages such as linear temporal logic (e.g. LTL) or tree logic (e.g. CTL). The effort required to acquire a sufficient level of expertise in writing these specifications represents a serious obstacle to the adoption of formal methods. Therefore, Dwyer et al. have introduced a new property specification language based on patterns in which a temporal property is a combination of one pattern and one scope.

Patterns There are 8 patterns organized under a semantic classification. We distinguish occurrence patterns from order patterns.

Occurrence patterns are: (i) Absence: an event never occurs, (ii) Existence: an event occurs at least once, (iii) Bounded Existence has 3 variants: an event occurs k times, at least k times or at most k times, and (iv) Universality: an event/state is permanent.

Order patterns are: (v) Precedence: an event P is always preceded by an event Q, (vi) Response: an event P is always followed by an event Q, (vii) Chain Precedence: a sequence of events P 1 , . . . , P n is always preceded by a sequence Q 1 , . . . , Q m (it is a generalization of the Precedence pattern), (viii) Chain Response: a sequence of events P 1 , . . . , P n is always followed by a sequence Q 1 , . . . , Q m (it is a generalization of the Response pattern).

Scopes A scope is the discrete time interval over which the property holds. There are five kinds of scopes, illustrated on Fig. 3 (taken from [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF]):

(a) globally covers the entire execution, (b) before Q covers the system's execution up to the first occurrence of Q, (c) after Q covers the system's execution after the first occurrence of Q, (d) between Q and R covers time intervals of the system's execution from an occurrence of Q to the next occurrence of R, (e) after Q until R is the same as the between scope in which R may not occur. Dwyer et al. provide a complete library5 mapping each pattern/scope combination to the corresponding formula in many formalisms (LTL, CTL, µ-calculus, Figure 2 illustrates the portions of an execution that are designated by the di erent kinds of scopes. We note that a scope itself should be interpreted as optional; if the scope delimiters are not present in an execution then the speci cation will be true. Scope operators are not present in most speci cation formalisms interval logics are an exception. Nevertheless, our experience indicates that many informal requirements are speci ed as properties of segments of program executions. Thus a pattern system for properties should mirror this view to enhance usability. We note that the various speci cation formalisms have di erent semantics and expressive power, and that a property that can be expressed easily in one formalism may be unnatural, or even impossible to capture precisely, in a di erent formalism. For instance, in statebased formalisms such as LTL or CTL, it is reasonable to specify that a certain proposition hold throughout a scope the Universality pattern, and to regard this as being in some sense dual to the Absence property stating that a proposition holds at no state in the scope.

Q and R After Q until R Before Q Q Q R Q Q State Sequence R
occurrence of an event indicating t has become true and the absence of that it has become false, which do ple relation to the Absence pattern. that some formalisms can express c in nite executions, while others are quences of states or events. Althou in practice, almost all of the proper can be expressed in almost all of t formalisms, the pattern system sho di erences to the user.

A System of Speci cation Patte

We have developed a system of pro patterns for nite-state veri cation system is a set of patterns organize hierarchies, with connections betwe to facilitate browsing. A user would propriate pattern to match the requ i ed, use the mapping section to ob the property in the formalism used b and then instantiate that template state formulas or events speci c to t In de ning a speci cation formalism give a small set of independent co a large class of interesting speci c structed. With the collection of spe however, we are neither trying to giv can generate the useful speci catio listing of speci cations. Patterns ar cause they appear frequently as prop We hypothesize that only a small fra properties that can be speci ed usi expressions commonly occur in prac ties, and simple variants of them, m system. We expect the set of pat time as developers encounter prope real systems that do not easily ma patterns.

The Patterns

Space limitations prohibit descript in full detail; for that we have set The full patterns contain additional tion of relationships among the patt to various formalisms. A list of o with short descriptions, follows. In t brevity, we use the phrase a given to mean a state in which the giv true, or an event from the given di occurs." Fig. 3. Property scopes such patterns dramatically simplifies the specification of temporal properties, with a fairly complete coverage. Indeed, they collected hundreds of specifications and they observed that 92% fall within this small set of patterns/scopes [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF]. For these reasons, we adopt this pattern-based approach for the temporal part of our OCL extension. We now present its syntax.

Syntax

We extended the OCL concrete grammar defined within the OMG standard [START_REF]Object Constraint Language[END_REF] in order to express temporal properties that will provide our test properties. The syntax of our language is summarized in Fig. 4. In this figure, nonterminals are designated in italics, terminals are underlined and construct (. . .)?

Scope LTL globally (P ⇒ ♦S) before R ♦R ⇒ (P ⇒ (¬R U (S ∧ ¬R))) U R after Q (Q ⇒ (P ⇒ ♦S)) between Q and R ((Q ∧ ¬R ∧ ♦R) ⇒ (P ⇒ (¬R U (S ∧ ¬R))) U R) after Q until R (Q ∧ ¬R ⇒ ((P ⇒ (¬R U (S ∧ ¬R))) W R)
Table 2. LTL mapping of the S follows P pattern designates an optional part. Terminal name designates an identifier that represents the name of a temporal property, an instance name, an operation name (when separated by ::) or tag names (REQ or AIM, as shown in Sec. 2.3). The OCLExpression terminal designates an OCL predicate according to the supported syntax of UML4ST (as explained in Sec. 2.1).

As explained before, a temporal property TempExpr is a combination of a pattern TempPattern and a scope TempScope whose respective meanings have been informally described before. Events are of two kinds. A ChangeEvent is parameterized by an OCL predicate P , and designates a step in which P now becomes true, i.e. P was evaluated to false in the preceding step. This event represents an observable event, that is triggered after the execution of an operation of the system (but it is not possible to know a priori which operation will cause this event). A CallEvent represents the invocation of an operation on a given instance. Optional field pre provides a precondition, namely an OCL predicate that has to be true before the invocation of the operation (or at the beginning of the invocation if the expression refers to input parameter values). Optional field post provides a postcondition that has to be true after the execution of the operation. Finally, optional field including (resp. excluding) provides the set of tags for which at least one has to be covered (resp. none shall be covered) by the execution of the operation. For example, event isCalled(sut::buyTicket, pre: in title=TITLES::Tron and not self.current user.oclIsUndefined(),including:{@AIM:BUY Success}) is triggered when operation buyTicket is invoked on the sut instance, with parameter in title representing a given movie title (provided as an enumeration class TITLES), when a user is logged on the system and the operation terminates by a successful buying of a ticket for this movie.

Example 1 (Temporal property). Let us consider the example of the eCinema application described in Sec. 2.2. We can formalize the following test requirements of the application as temporal properties. Users can only buy tickets when logged on the system. This statement can be expressed as a test property using a between scope as follows:

eventually isCalled(buyTicket, including:{@AIM:BUY_Success}) at least 0 times between becomesTrue(not(self.current_user.isOclUndefined())) and becomesTrue(self.current_user.isOclUndefined()).

Even though the presence of at least 0 in the pattern may be strange, it describes the optional occurrence of the event C. But, this statement may also be expressed as a robustness test property: never isCalled(buyTicket, including:{@AIM:BUY_Success}) after becomesTrue(self.current_user.isOclUndefined()) until isCalled(login, including:{@AIM:LOGIN_Success}).

In this section, we formally define substitution automata that are used to describe the semantics of the properties, and we give a definition of the substitution process. The motivation behind the use of such automata is to have a compositional semantics, so as to be able to build an automaton representing a test property. The latter is thus a combination of a scope and a pattern. Each of them is formalized using substitution automata defined in Def. 1. The resulting automaton will capture all the executions of the system and highlight specific transitions representing the events used in the property. We first define the substitution automata modelling scopes and patterns. Then we present the labels of the transitions representing the events in properties. Finally, we give the definition of the substitution that applies.

Substitution automata

Substitution automata are labelled automata where the labels are defined from the events (see Event in Fig. 4). The states in S are substitution states that represent a property provided with generic patterns. They will be replaced by an automaton defining a particular pattern. For some property, such as P attern between E 1 and E 2 , it is necessary to avoid that E 2 is triggered in the automaton of the pattern. For that, we formalise this restriction (R) labelling the substitution state by a set of labels. These labels are events that will not be triggered by the internal transitions of the pattern automaton.

Definition 1 (Substitution automaton). Let Σ be the set of labels. A substitution automaton is a 6-tuple a = Q, F, q 0 , S, R, T where: Q is a finite set of states, F is a set of final states (F ⊆ Q), q 0 is an initial states (q 0 ∈ Q), S is a set of substitution states (S ⊆ Q), R is a function that associates a set of labels to any substitution state (R ∈ S → P(Σ)), T is a set of transitions (T ∈ Q × P(Σ) × Q) labelled by a set of labels.

Graphically, substitution states will be depicted as squares (instead of regular circles). If the substitution state presents a restriction on the alphabet, the restricted elements are written as state labels.

Scopes and patterns will be formalized as substitution automata whose labels are events that occur in the scopes and patterns. More precisely, a scope is modelled as a substitution automaton with one substitution state, whereas a pattern is modelled as a substitution automaton without substitution states.

Example 2 (Substitution Automaton for Scopes and Patterns). Figures 5 and6 respectively give the graphical representation of the automata of the temporal property T P between A and B in which the square state represents the generic pattern T P and pattern eventually C at least 0 times. For the latter, the automaton clearly identifies a reflexive transition that represents the occurrence of C. Its presence originates from the motivation of coverage measure, and will make it possible to see if C has been called, or not. Before describing the substitution operation, we now present the alphabet of labels that is used in our automata.

Events and Labels

The events triggered in a property description and described by the rules Cal-lEvent and ChangeEvent in the grammar described in Fig. 4 are represented by labels in automata.

The isCalled structure can be divided in four parts: the operation name, the precondition for this call to happen, the postcondition that has to be satisfied after the call, and a list of tags that may be activated. Thus, we will use the following notation to denote the alphabet elements in our automata:

[operation name, precondition, postcondition, tags].

Note that there can be unspecified slots in this notation: for example, one can specify the activation of a specific operation op provided with a precondition pre, but leaves the postcondition and tags slots free, denoted by [op,pre, , ], in which symbol " " designate a free slot, meaning that it can be any operation, the predicate true and any tag. A such label represent a set of atomic events that are triggered by the transition. For example, in example 3 the label C represent one atomic event whereas the label A represent the set of atomic events for any tag in any operation. Also, the tag list references the tags that may be activated. If the isCalled specifies a list of excluded tags, we can extract the set of tags that may be used (the complementary set of tags) as we know all the tags of a specific operation from the model.

The ChangeEvent can be seen as a free operation call with a pre-and postcondition without specifying the operation name nor the tags to be used. Notice that any operation can be called. The precondition is the negation of the becomesTrue predicate, illustrating the fact that, before the call, the execution of the operation has made the predicate become true. Therefore, all becomesTrue(P ) events can be denoted by the label [ ,¬P ,P , ].

Each scope and pattern are associated to a skeleton of substitution automata whose transition labels are instantiated with the events appearing in the property that they define.

Example 3 (Labels). Consider the first property given in Example 1. According to the label notation introduced in Sec. 4.2, the labels A, B and C in Fig. 5 and Fig. 6 are respectively [ , self.current user.isOclUndefined(), not(self.current user.isOclUndefined()), ], [ , not(self.current user.is-OclUndefined()), self.current user.isOclUndefined(), ] and [buyTicket, , , {@AIM:BUY Success}].

Notice that two labels can be the same set of events even if they are not written with the same 4-uplet. It is also possible that the set of atomic events of a label includes the set of atomic events of another label. In practice, these cases must represent an ambiguous test property. Therefore, we assume that all the events labelling the outgoing transitions of the automata states are mutually exclusive, producing, in that, deterministic automata.

When the two automata, the scope and the pattern, have been defined, they have to be combined to obtain a single automaton, that does not contain any substitution state. We now describe how substitution works.

Substitution

The substitution operation defined in Def. 2 replaces the substitution state s, representing a generic pattern, by an automaton as, representing an instance of a pattern, in an automaton a, representing a test property. For an automaton a, we denote by X a the component X of a. For the definition, we assume that there is only one substitution state in a and no substitution state in as, i.e. S as = ∅ and R as = ∅. We also assume that the label of transitions in a and in as are different and that the set of states of a and as are disjoint.

The set of states of the resulting automaton c is the set of states of a without its substitution states S a union each state of the substituted automaton as. When s is a final (resp. initial) state, the set of final (resp. initial) states of c is the set of a without its final (resp. initial) substitution states union each final (resp. initial) state of the substituted automaton as. Otherwise, the set of final (resp. initial) states is this of a. c contain no substitution state and consequently no restriction.

We denote by q a non-substitution state (q ∈ Q -S), s a substitution state (s ∈ S) and E a set of labels, the transitions of c are defined in four cases:

1. any transition q E → q in a is a transition of c, 2. for a transition q E → s in a, there is a transition q E → q in c for the initial state of as, 3. for a transition s E → q in a, there is a transition q E → q in c for any final state q of as, 4. any transition q E → q in as becomes a transition q E → q in c where E is the set of labels E reduced by the labels R(s).

Definition 2 (Substitution Operation). Let a be an automaton such that S a = {s}. Let as be an automaton such that S as = ∅. The substitution of the state s by the automaton as in a is the automaton c defined as:

-Q c = (Q a -S a ) ∪ Q as , -when s ∈ F a , F c = (F a -{s}) ∪ F as , otherwise F c = F a ,
when s = q 0a , q 0c = q 0as , otherwise q 0c = q 0a , -S c = ∅ and R c = ∅, q E → q ∈ T c if and only if:

1. q, q ∈ Q a -S a and q E → q ∈ T a , 2. q ∈ Q a -S a and q E → s ∈ T a and q = q 0as , 3. q ∈ Q a -S a and s E → q ∈ T a and q ∈ F as , 4. ∃E ∈ P(Σ) such that q E → q ∈ T as and E = E -R(s).

Example 4 (Substitution Automata Composition). Consider again the scope and the property substitution automata represented in Fig. 5 and Fig. 6. Figure 7 shows the flattened automaton obtained by applying the substitution operation. This is the automaton of the property given in Example 1.

The resulting automaton represents the executions of the system allowed by the property. We now measure the coverage of this automaton to establish a metrics that will be used to evaluate the exhaustiveness of a test suite.

Property Coverage Measure

This section presents the technique used to measure the coverage of the property. It is based on the semantics of the property language that was previously introduced.

Automata Completion

Before performing the coverage measure, we need to complete our property automaton so as to match every possible event on our property automaton. In the example given in Fig. 7, the automaton is complete in the sense that any event will be matched from any state of the automaton. Nevertheless, in practice, the automaton is not necessarily complete. Indeed, the substitution can result in an incomplete automaton: it only represents all valid paths for the property. The complete form of the automaton thus represents all possible paths, including all faulty (with respect to the property) execution. The completion process simply creates a new state that can be seen as a rejection state while final states represent acceptance states. If a state does not allow the triggering of a transition for an alphabet element, we create a transition from this state to the newly created state. Figure 8 illustrates this completion where the rejection state is the circle marked of one cross.

Remark. Ideally, in a Model-Based Testing process, the model describes faithfully the system, and it has no risk of violating a given (temporal) property that is supposed to hold on the system. However, in reality, the model may contain faults and thus, invalidate the property. The completion of the automaton is used to capture events that lead to an invalidate state, which detects the violation of the property. If the model satisfies the property, these additional transitions are useless, since they will never be activated on the model. Nevertheless, we add them to be able to detect possible violations of the property w.r.t. the model execution, indicating a fault in the model or in the property. Thus, we are able to partially verify (i.e. test) the model using existing test sequences, by monitoring the absence of property violation.

Performing the Measure

The evaluation of the property coverage is based on the coverage of its underlying automaton. Using the CertifyIt animation engine 6 , it is possible to replay a set of existing test cases on a model. At each step (i.e. after each operation invocation), the corresponding state can be used to evaluate a given OCL predicate.

The algorithm for measuring the coverage of the property is quite straightforward, and sketched in Fig. 9. This algorithm takes as input a model M , a test suite T S and a completed substitution automaton A, supposed to represent a property. For each test, the automaton exploration starts from its (single) initial state. At each step of the test, the corresponding event on the automaton is matched. If it triggers an outgoing transition from the current state, then the exploration of the automaton progresses, and corresponding transition and states are marked by the test, and the corresponding step. When an rejection state is reached, the exploration stops and an error is returned. Once all the steps have been performed, the algorithm moves to the next test. In the end, we have, for each test, the states and transitions of the automaton reached by the test. When the test is replayed and the coverage of the underlying automaton is performed, three alternatives may happen: (i) the test leads to a rejection state, then the model does not respect the property, (ii) the test explores at least one transition of the automaton and reaches at least one final state (i.e. it should not stay in a initial and final state), then we say that the test "covers" the property, (iii) the test explores the automaton but does not reach any final state (except a final state that is also an initial state), then the test does not cover the property.

Finally, we measure classical automata coverage criteria (all-nodes, all-edges, etc.) and report the coverage of a test suite w.r.t. these criteria. Notice that only the test covering the property are considered.

Example 5 (Measure of the CertifyIt test suite coverage). As explained before, the CertifyIt test generation strategy aims at producing functional test suites. Consider the three test cases dedicated to the buyTicket operation, for which we want to evaluate their relevance w.r.t. the two test properties represented by the two automata depicted in Fig. 7 and Fig. 8. None of these tests do cover the property as defined in (ii) hereabove, as they never reach a final state (the only final state covered is also initial) in which the user disconnects from the system.

A test suite that satisfies the all-nodes and all-edges coverage criterion for the first property could be the following:

{ init; sut.login(REGISTERED USER,REGISTERED PWD); sut.showBoughtTickets(); sut.logout(), init; sut.login(REGISTERED USER,REGISTERED PWD); sut.buyTicket(TITLE1); sut.logout(); }

Conclusion, Related and Future Works

We have presented in this paper a property language for UML/OCL models, based on scopes and patterns, and aiming at expressing test properties. We have proposed to evaluate the relevance of a given test suite by measuring the coverage of an automaton representing the admissible traces of the model's execution that cover the property. This approach is tool-supported (a tool prototype has been made available for the members of the TASCCC project) and experimented on the GlobalPlatform7 case study, a last generation smart card operating system, provided by Gemalto 8 . This approach has several interesting features. First, the evaluation of a test suite is relevant w.r.t. a Common Criteria evaluation [START_REF]Common Criteria for Information Technology Security Evaluation, version 3.1[END_REF] of a security product which requires specific security requirements to be covered by the test cases during the validation phase. Second, the uncovered parts of the properties that have been discovered indicate precisely on which part of the system the validation engineer has to focus to complete the existing test suite. In addition, the existing tests can be used to identify relevant pieces of model executions that make it possible to reach a given state in the property automaton, helping the validation engineer to design complementary test cases, that do not only rely on its own interpretation of the property.

Related works. This approach is inspired from property monitoring approaches. Many related works fall into the category of passive testing, in which properties are monitored on a system under test [START_REF] Ayache | Observer: a concept for on-line detection of control errors in concurrent systems[END_REF][START_REF] Arnedo | Fast testing of critical properties through passive testing[END_REF]. This kind of approach is particularly used in security testing, where the violation of security properties can be detected at run-time and strengthen the test verdict [START_REF] Bayse | A passive testing approach based on invariants: application to the wap[END_REF]. The closest work is reported in [START_REF] Falcone | More testable properties[END_REF] which uses a similar approach, also based on Dwyer's property patterns and the classification of occurrence/precedence patterns, in order to monitor test properties. Our approach differs in the sense that we aim at evaluating test cases w.r.t. properties. Also, [START_REF] Li | Property-oriented testing: An approach to focusing testing efforts on behaviours of interest[END_REF] proposes the generation approach of relevant test sequences from UML statecharts guided by temporal properties. A test relevance criterion is also defined. In [START_REF] Giorgetti | Verification of class liveness properties with Java modeling language[END_REF], temporal properties written in Java Temporal Pattern Language (also inspired by Dwyer's patterns) are designed and translated into JML annotations that are monitored during the execution of Java classes.

Future works. We are currently investigating the way of building these missing test cases automatically using a Scenario-Based Testing approach [START_REF] Cabrera Castillos | Scenario-based testing from UML/OCL behavioral models -application to POSIX compliance[END_REF]. In addition, we are also looking for the automated generation of robustness test cases, to be extracted from these user-defined test properties, by using a mutation based testing approach applied to the property, also coupled with a Scenario-Based Testing approach. Another extension of this work will be to define dedicated temporal property coverage criteria e.g. inspired from [START_REF] Fraser | Complementary criteria for testing temporal logic properties[END_REF].

Fig. 1 .

 1 Fig. 1. Class Diagram of the eCinema Model

Figure 2 :

 2 Figure 2: Pattern Scopes

Fig. 5 .Fig. 6 .

 56 Fig. 5. between A and B

Fig. 7 .

 7 Fig. 7. Graphical representation of the composition for property eventually C at least 0 times between A and B

6Fig. 8 .

 8 Fig. 8. Completion with rejection states (automaton for never C between A and B)

Funded by the French National Research Agency ANR-09-SEGI-014http://lifc. univ-fcomte.fr/TASCCC

www.smartesting.com

http://patterns.projects.cis.ksu.edu

www.globalplatform.org/specifications.asp

www.gemalto.com


Ivan Enderlin
email: ivan.enderlin@edu.univ-fcomte.fr

Frédéric Dadeau
email: frederic.dadeau@univ-fcomte.fr

Alain Giorgetti
email: alain.giorgetti@univ-fcomte.fr

Abdallah Ben Othman
email: abdallah.benothman@edu.univ-fcomte.fr

Praspel: A Specification Language for Contract-Based Testing in PHP

Keywords: PHP, Design-by-Contract, annotation language, unit testing, formal specifications

We introduce in this paper a new specification language named Praspel, for PHP Realistic Annotation and SPEcification Language. This language is based on the Design-by-Contract paradigm. Praspel clauses annotate methods of a PHP class in order to both specify their contracts, using pre-and postconditions, and assign realistic domains to the method parameters. A realistic domain describes a set of concrete, and hopefully relevant, values that can be assigned to the data of a program (class attributes and method parameters). Praspel is implemented into a unit test generator for PHP that offers a random test data generator, which computes test data, coupled with a runtime assertion checker, which decides whether a test passes or fails by checking the satisfaction of the contracts at run-time.

Introduction

Over the years, testing has become the main way to validate software. A challenge is the automation of test generation that aims to unburden the developers from writing their tests manually. Recent development techniques, such as Agile methods, consider tests as first-class citizens, that are written prior to the code. Model-based testing [START_REF] Beizer | Black-box testing: techniques for functional testing of software and systems[END_REF] is an efficient paradigm for automating test generation. It considers a model of the system that is used for generating conformance test cases (w.r.t. the model) and computing the oracle (i.e. the expected result) that is used to decide whether a test passes or fails.

In order to ease the model description, annotation languages have been designed, firstly introduced by B. Meyer [START_REF] Meyer | Applying "design by contract[END_REF], creating the Design-by-Contract paradigm. These languages make it possible to express formal properties (invariants, preconditions and postconditions) that directly annotate program entities (class attributes, methods parameters, etc.) in the source code. Many annotation languages exist, such as the Java Modeling Language (JML) [START_REF] Leavens | JML: A notation for detailed design[END_REF] for Java, Spec# [START_REF] Barnett | The Spec# Programming System: An Overview[END_REF] for C#, or the ANSI-C Specification Language (ACSL) [START_REF] Baudin | ACSL: ANSI C Specification Language[END_REF] for C. Design-by-Contract considers that a system has to be used in a contractual way: to invoke a method the caller has to fulfil its precondition; in return, the method establishes its postcondition.

Contract-Driven Testing. Annotations can be checked at run time to make sure that the system behaves as specified, and does not break any contract. Contracts are thus well-suited to testing, and especially to unit testing [START_REF] Leavens | How the design of JML accommodates both runtime assertion checking and formal verification[END_REF]. The idea of Contract-Driven Testing [START_REF] Aichernig | Contract-based testing[END_REF] is to rely on contracts for both producing tests, by computing test data satisfying the contract described by the precondition, and for test verdict assessment, by checking that the contract described by the postcondition is ensured after execution. On one hand, method preconditions can be used to generate test data, as they characterize the states and parameters for which the method call is licit. For example, the Jartege tool [START_REF] Oriat | Jartege: A Tool for Random Generation of Unit Tests for Java Classes[END_REF] generates random test data, in accordance with the domain of the inputs of a given Java method, and rejects the values that falsify the precondition. The JML-Testing-Tools toolset [START_REF] Bouquet | Automated Boundary Test Generation from JML Specifications[END_REF] uses the JML precondition of a method to identify boundary states from which the Java method under test will be invoked. The JMLUnit [START_REF] Cheon | A simple and practical approach to unit testing: The JML and JUnit way[END_REF] approach considers systematic test data for method input parameters, and filters irrelevant ones by removing those falsifying the method precondition. On the other hand, postconditions are employed similarly in all the approaches [START_REF] Bouquet | Automated Boundary Test Generation from JML Specifications[END_REF][START_REF] Campbell | Testing concurrent object-oriented systems with spec explorer[END_REF][START_REF] Cheon | A simple and practical approach to unit testing: The JML and JUnit way[END_REF]. By runtime assertion checking, the postcondition is verified after each method execution, to provide the test verdict.

Contributions. In this paper, we present a new language named Praspel, for PHP Realistic Annotation and SPEcification Language. Praspel is a specification language for PHP [START_REF] Schroeder | The PHP website[END_REF] which illustrates the concept of realistic domains. Praspel introduces Design-by-Contract in PHP, by specifying realistic domains on class attributes and methods. Consequently, Praspel is adapted to test generation: contracts are used for unit test data generation and provide the test oracle by checking the assertions at runtime.

Our second contribution is a test framework supporting this language. This online test generation and execution tool works in three steps: (i) the tool generates values for variables according to the contract (possibly using different data generators), (ii) it runs the PHP program with the generated values, and (iii) the tool checks the contract postcondition to assign the test verdict.

Paper outline. The paper is organized as follows. Section 2 briefly introduces the concept of realistic domains. Section 3 presents an implementation of realistic domains in the Praspel language, a new annotation language for PHP. Section 4 describes the mechanism of automated generation of unit tests from PHP files annotated with Praspel specifications. The implementation of Praspel is described in Section 5. Section 6 compares our approach with related works. Finally, Section 7 concludes and presents our future work.

Realistic Domains

When a method precondition is any logical predicate, say from first-order logic, it can be arbitrarily difficult to generate input data satisfying the precondition.

One could argue that the problem does not appear in practice because usual preconditions are only simple logical predicates. But defining what is a "simple" predicate w.r.t. the problem of generating values satisfying it (its models) is a difficult question, still partly open. We plan to address this question and to put its positive answers at the disposal of the test community. In order to reach this goal we introduce the concept of realistic domains.

Realistic domains are intended to be used for test generation purposes. They specify the set of values that can be assigned to a data in a given program. Realistic domains are well-suited to PHP, since this language is dynamically typed. Therefore, realistic domains introduce a specification of data types that are mandatory for test data generation. We introduce associated features to realistic domains, and we then present the declination of realistic domains for PHP.

Features of realistic domains

Realistic domains are structures that come with necessary properties for the validation and generation of data values. Realistic domains can represent all kinds of data; they are intended to specify relevant data domains for a specific context. Realistic domains are more subtle than usual data types (integer, string, array, etc.) and are actually refinement of those latters. For example, if a realistic domain specifies an email address, we can validate and generate strings representing syntactically correct email addresses, as shown in Fig. 1.

Realistic domains display two features, which are now described and illustrated.

Predicability. The first feature of a realistic domain is to carry a characteristic predicate. This predicate makes it possible to check if a value belongs to the possible set of values described by the realistic domain.

Samplability. The second feature of a realistic domain is to propose a value generator, called the sampler, that makes it possible to generate values in the realistic domain. The data value generator can be of many kinds: a random generator, a walk in the domain, an incrementation of values, etc.

We now present our implementation of realistic domains in PHP and show some interesting additional principles they obey.

Realistic domains in PHP

In PHP, we have implemented realistic domains as classes providing at least two methods, corresponding to the two features of realistic domains. The first method is named predicate($q) and takes a value $q as input: it returns a boolean indicating the membership of the value to the realistic domain. The second method is named sample() and generates values that belong to the realistic for($i = 0; $i < $nbparts; ++$i) { if($i > 0) // add separator or arobase $q .= ($i == $nbparts -1) ? '@' : '.';

$len = rand(1,10); for($j=0; $j < $len; ++$j) { $index = rand(0, strlen($chars) -1); $q .= $chars[$index]; } } $q .= '.' .

$doms[rand(0, count($doms) -1)]; return $q; } } Fig. 1. PHP code of the EmailAddress realistic domain domain. An example of realistic domain implementation in a PHP class is given in Fig. 1. This class represents the EmailAddress realistic domain already mentioned. Our implementation of realistic domains in PHP exploit the PHP object programming paradigm and benefit from the following two additional principles.

Hierarchical inheritance. PHP realistic domains can inherit from each other.

A realistic domain child inherits the two features of its parent and is able to redefine them. Consequently, all the realistic domains constitute an universe.

Parameterizable realistic domains. Realistic domains may have parameters. They can receive arguments of many kinds. In particular, it is possible to use realistic domains as arguments of realistic domains. This notion is very important for the generation of recursive structures, such as arrays, objects, graphs, automata, etc.

Example 1 (Realistic domains with arguments). The realistic domain boundinteger(X, Y ) contains all the integers between X and Y . The realistic domain string(L, X, Y ) is intended to contain all the strings of length L constituted of characters from X to Y Unicode code-points. In the realistic domain string(boundinteger(4, 12), 0x20, 0x7E), the string length is defined by another realistic domain.

PHP Realistic Annotation and Specification Language

Realistic domains are implemented for PHP in Praspel, a dedicated annotation language based on the Design-by-Contract paradigm [START_REF] Meyer | Applying "design by contract[END_REF]. In this section, we present the syntax and semantics of the language.

Praspel specifications are written in API documentation comments as shown in Fig. 3, 4, 5 and 6. Praspel makes it possible to mix informal documentations and formal constraints, called clauses and described hereafter. Praspel clauses are ignored by PHP interpreters and integrated development environments. Moreover, since each Praspel clause begins with the standard @ symbol for API keywords, it is usually well-handled by pretty printers and API documentation generators.

The grammar of Praspel annotations is given in Fig. 2. Notation (σ)? means that σ is optional. (σ) r s represents finite sequences of elements matching σ, in which r is either + for one or more matches, or * for zero or more matches, and s is the separator for the elements in the sequence.

Underlined words are PHP entities. They are exactly the same as in PHP. A predicate is a valid logical PHP expression that returns a boolean. An identifier is the name of a PHP class or the name of a method or method parameter. It cannot be the name of a global variable or an attribute, which are respectively prohibited (as bad programming) and defined as invariants in Praspel. The syntax of identifiers strictly follows the syntax of PHP variables.

The other syntactic entities in this grammar are explained in the PHP manual [START_REF] Schroeder | The PHP website[END_REF]. Praspel expressions are conjunctions of realistic domain assignments and of relations between realistic domains, explained in Section 3.1. The special case of array descriptions is explained in Section 3.2. Finally, clauses are described in Section 3.3.

Assigning realistic domains to data

We now explain how to declare the realistic domains of method parameters and we give the semantics of these declarations w.r.t. the method inputs and output.

The syntactic construction:

i: t 1 (. . . ) or . . . or t n (. . . )
associates at least one realistic domain (among t 1 (. . . ), . . . , t n (. . . )) to an identifier (here, i). We use the expression "domains disjunction" when speaking about syntax, and the expression "domains union" when speaking about semantics. The left-hand side represents the name of some method argument, whereas the right-hand side is a list of realistic domains, separated by the "or" keyword.

The semantics of such a declaration is that the realistic domain of the identifier i may be t 1 (. . .) or . . . or t n (. . .), i.e. it is the union (as in the C language) of the realistic domains t 1 (. . .) to t n (. . .). These realistic domains are (preferably) mutually exclusive.

Example 2 (An identifier with many realistic domains). The declaration: y: integer() or float() or boolean() means that y can either be an integer, a floating-point number or a boolean.

The domainof operator describes a dependency between the realistic domains of two identifiers. The syntactic construction: identifier domainof identifier creates this relation. The semantics of i domainof j is that the realistic domain chosen at runtime for j is the same as for i.

When an object is expected as a parameter, it can be specified using the class(C) construct, in which C is a string designating the class name.

Array description

A realistic domain can also be an array description. An array description has the following form:

[from T 1 1 ( . . . ) or . . . or T 1 i ( . . . ) to T 1 i+1 ( . . . ) or . . . or T 1 n ( . . . ), . . . from T k 1 ( . . . ) or . . . or T k j ( . . . ) to T k j+1 ( . . . ) or . . . or T k m ( . . . )]
It is a sequence between square brackets "[" and "]" of pairs separated by symbol ",". Each pair is composed of a domain introduced by the keyword "from", and a co-domain introduced by the keyword "to". Each domain and co-domain is a disjunction of realistic domains separated by the keyword "or". The domain is optional.

The semantics of an array description depends of the realistic domain where it is used. We detail this semantics in the most significant case, when the array description is a parameter of the realistic domain array. Notice that an array description and the realistic domain array are different. The realistic domain array has two arguments: the array description and the array size.

Example 4 (Array specification). Consider the following declarations: a1: array([from integer() to boolean()], boundinteger(7, 42)) a2: array([to boolean(), to float()], 7) a3: array([from integer() to boolean() or float()], 7) a4: array([from string [START_REF] Demillo | Constraint-Based Automatic Test Data Generation[END_REF] to boolean(), to float() or integer()], 7)

a1 describes an homogeneous array of integers to booleans. The size of the yielded array is an integer between 7 and 42. In order to produce a fixed-size array, one must use an explicit constant, as in the subsequent examples. a2 describes two homogeneous arrays: either an array of booleans, or an array of floats, but not both. In all cases, the yielded array will have a size of 7. If no realistic domain is given as domain (i.e. if the keyword "from" is not present), then an autoincremented integer (an integer that is incremented at each sampling) will be yielded. a2 is strictly equivalent to array([to boolean()], 7) or array([to float()], 7). a3 describes an heterogeneous array of booleans and floats altogether. Finally, a4 describes either an homogeneous array of strings to booleans or an heterogeneous array of floats and integers.

Designing Contracts in Praspel

This section describes the syntax and semantics of the part of Praspel that defines contracts for PHP classes and methods. Basically, a contract clause is either the assignment of a realistic domain to a given data, or it is a PHP predicate that provides additional constraints over variables values (denoted by the \pred construct).

Invariants. In the object programming paradigm, class attributes may be constrained by properties called "invariants". These properties must hold before and after any method call and have the following syntax. @invariant I 1 and . . . and I p ;

Classically, invariants have to be class C { /** * @invariant a: boolean(); */ protected $a; } Fig. 3. Example of invariant clause satisfied after the creation of the object, and preserved through each method execution (i.e. assuming the invariant holds before the method, then it has to hold once the method has terminated). Invariants are also used to provide a realistic domain to the attributes of an object.

Example 5 (Simple invariant). The invariant in Fig. 3 specifies that the attribute a is a boolean before and after any method call.

Method contracts. Praspel makes it possible to express contracts on the methods in a class. The contract specifies a precondition that has to be fulfilled for the method to be executed. In return, the method has to establish the specified postcondition. The contract also specifies a set of possible exceptions that can be raised by the method. The syntax of a basic method contract is given in Fig. 4. The semantics of this contract is as follows.

Each R x (1 ≤ x ≤ n) represents ei-/** * @requires R1 and ... and Rn; * @ensures E1 and ... and Em; * @throwable T1, ..., Tp; */ function foo ( ... ) { ... } Fig. 4. Syntax of Method Contracts ther the assignment of a realistic domain to a data, or a PHP predicate that provides a precondition. The caller of the method must guarantee that the method is called in a state where the properties conjunction R 1 ∧ . . . ∧ R n holds (meaning that the PHP predicate is true, and the value of the data should match their assigned realistic domains). By default, if no @requires clause is declared, the parameter is implicitly declared with the undefined realistic domain (which has an always-true predicate and sample an integer by default).

Each E z (1 ≤ z ≤ m) is either the assignment of a realistic domain to a data (possibly the result of the method) after the execution of the method, or an assertion specified using a PHP predicate that specifies the postcondition of the method. The method, if it terminates normally, should return a value such that the conjunction E 1 ∧ . . . ∧ E m holds.

Each T y (1 ≤ y ≤ p) is an exception name. The method may throw one of the specified exceptions T 1 ∨ . . . ∨ T p or a child of these ones. By default, the specification does not authorize any exception to be thrown by the method.

Postconditions (@ensures clauses)

/** * @requires x: boundinteger(0,42); * @ensures \result: eveninteger() * and \pred(x >= \old(x)); * @throwable FooBarException; */ function foo ( $x ) { if($x === 42) throw new FooBarException(); return $x * 2; } Fig. 5. Example of Simple Contract usually have to refer to the method result and to the variables in the prestate (before calling the function). Thus, PHP expressions are extended with two new constructs: \old(e) denotes the value of expression e in the pre-state of the function, and \result denotes the value returned by the function. Notice that our language does not include first-order logic operators such as universal or existential quantifiers. Nevertheless, one can easily simulate such operators using a dedicated boolean function, that would be called in the PHP predicate. Example 6 (Simple contract). Consider the example provided in Fig. 5. This function foo doubles the value of its parameter $x and returns it. In a special case, the function throws an exception.

Behavorial clauses. In addition, Praspel makes it possible to describe explicit behaviors inside contracts.

A behavior is defined by a name and local @requires, @ensures, and @throwable clauses (see Fig. 6(a)). The semantics of behavioral contracts is as follows.

The caller of the method must guarantee that the call is performed in a state where the property R 1 ∧ . . . ∧ R n holds. Nevertheless, property A 1 ∧ . . . ∧ A k should also hold. The called method establishes a state where the property (A 1 ∧ . . . ∧ A k ⇒ E 1 ∧ . . . ∧ E j ) ∧ E j+1 ∧ . . . ∧ E m holds, meaning that the postcondition of the specified behavior only has to hold if the precondition of the behavior is satisfied. Exceptions T i (1 ≤ i ≤ t) can only be thrown if the preconditions R 1 ∧ . . . ∧ R n and A 1 ∧ . . . ∧ A k hold.

The @behavior clause only contains @requires, @ensures and @throwable clauses. If a clause is declared or used outside a behavior, it will automatically be set into a default/global behavior. If a clause is missing in a behavior, the clause in the default behavior will be chosen.

Example 7 (Behavior with default clauses). The specification in Fig. 6(b) is an example of a complete behavioral clause. This contract means: the first argument $x is always an integer and the result is always a boolean, but if the second argument $y is a positive integer, then the third argument $z is a boolean (behavior foo), else if $y is a negative integer, and the $z is a float and then the method may throw an exception (behavior bar).

Automated Unit Test Generator

The unit test generator works with the two features provided by the realistic domains. First, the sampler is implemented as a random data generator, that satisfies the precondition of the method. Second, the predicate makes it possible to check the postcondition (possibly specifying realistic domains too) at runtime after the execution of the method.

Test Verdict Assignment using Runtime Assertion Checking

The test verdict assignment is based on the runtime assertion checking of the contracts specified in the source code. When the verification of an assertion fails, a specific error is logged. The runtime assertion checking errors (a.k.a. Praspel failures) can be of five kinds. (i) precondition failure, when a precondition is not satisfied at the invocation of a method, (ii) postcondition failure, when a postcondition is not satisfied at the end of the execution of the method, (iii) throwable failure, when the method execution throws an unexpected exception, (iv) invariant failure, when the class invariant is broken, or (v) internal precondition failure, which corresponds to the propagation of the precondition failure at the upper level.

The runtime assertion checking is performed by instrumenting the initial PHP code with additional code which checks the contract clauses. The result of the code instrumentation of a given method foo is shown in Fig. 7. It corresponds to the treatment of a behavioral contract, as shown in Fig. 6. The original method foo is duplicated, renamed (as foo body) and substituted by a new foo method which goes through the following steps:

-First, the method checks that the precondition is satisfied at its beginning, using the auxiliary method foo pre. -Second, the \old expressions appearing in the postconditions are evaluated and stored for being used later.

-Third, the replication of the original method body is called. Notice that this invocation is surrounded by a try-catch block that is in charge of catching the exception that may be thrown in the original method. -Fourth, when the method terminates with an exception, this exception is checked against the expected ones, using the auxiliary method foo exception. Then the exception is propagated so as to preserve the original behavior of the method. -Fifth, when the method terminates normally, the postconditions and the invariants are checked, using the auxiliary method foo post. -Sixth, and finally, the method returns the value resulting of the execution of foo body.

Test cases are generated and executed online: the random test generator produces test data, and the instrumented version of the initial PHP file checks the conformance of the code w.r.t. specifications for the given inputs. The test succeeds if no Praspel failure (listed previously) is detected. Otherwise, it fails, and the log indicates where the failure has been detected.

Random Test Data Generation

To generate test data, we rely on a randomizer, a sampling method that is in charge of generating a random value for a given realistic domain. The randomizer works with the realistic domain assignments provided in the @requires clauses of the contracts.

Assume that the precondition of a method specifies the realistic domain of parameter i as follows: @requires i: t 1 (. . .) or . . . or t n (. . .);. When this method is randomly tested, a random value for i is generated in the domain of one of its n declared realistic domains. If n ≥ 2, then a realistic domain t c (. . .) is first selected among t 1 (. . .), . . . , t n (. . .) by uniform random generation of c between 1 and n. Then, the randomizer generates a value of domain t c (. . .) for i using the sampling method provided by this realistic domain.

When the data to be generated is an object of class C, the invariant of class C is analyzed in order to recover the realistic domains associated to the class attributes, and it recursively generates a data value for each class attribute. An instance of class C is created and the generated data values are assigned to the class attributes.

By default, the test case generation works by rejection of irrelevant values, as described in the simplified algorithm in Fig. 8. This algorithm has three parameters. The first one, nbTests, represents the number of tests the user wants to generate. The second parameter, maxTries, is introduced in order to ensure that the generator stops if all the yielded values are rejected. Indeed, the generator may fail to yield a valid value because the preconditions lay down too strong constraints. The third and last parameter, methods, represents the set of methods to test.

For many realistic domains this default test generation method can be overloaded by more efficient methods. We have already implemented the following enhancements: -Generation by rejection is more efficient when the rejection probability is low. Therefore, the hierarchy of realistic domains presented in Section 2.2 is constructed so that each class restricts the domain of its superclass as little as possible, and rejection always operates w.r.t. this direct superclass for more efficiency. -Realistic domains representing intervals are sampled without rejection by a direct call to a uniform random generator, in fact two generators: a discrete and a continuous one.

The users are free to add their own enhancements and we plan to work in this direction in a near future.

Tool Support and Experimentation

The Praspel tool implements the principles described in this paper. Praspel is freely available at http://hoa-project.net/. It is developed in Hoa [START_REF] Enderlin | Hoa Framework project[END_REF] (since release 0.5.5b), a framework and a collection of libraries developed in PHP. Hoa combines a modular library system, a unified streams system, generic solutions, etc. Hoa also aims at bridging the gap between research and industry, and tends to propose new solutions from academic research, as simple as possible, to all users. Praspel is a native library of Hoa (by opposition to user libraries). This deep integration ensures the durability and maintenance of Praspel. It is provided with an API documentation, a reference manual, a dedicated forum, etc. Moreover, we get feedbacks about the present research activity through Hoa user community.

A demonstration video of the Praspel tool is also available at the following address: http://hoa-project.net/Video/Praspel.html. As shown in this demonstration, the Praspel language is easy to learn and to use for developers. The tool support makes it possible to produce test data and run test cases in a dedicated framework with little effort. Praspel has been presented and demonstrated at the ForumPHP'10 conference, which gathers the PHP community, and was received very favourably.

We applied Praspel to web application validation. In such applications, PHP functions are used to produce pieces of HTML code from simple inputs. Being also teachers, we have decided to test the (buggy!) code of our students of the "Web Languages" course. Using a dedicated library of Hoa to build LL(k) parsers, we easily designed the realistic domains associated with the expected output HTML code, that had to be well-structured, and respecting some structural constraints (e.g. exactly one <option> of a <select> has to be set by default). We analysed their functions using this mechanism.

To save space, we have reported this experimentation on a web page at the following address: http://lifc.univ-fcomte.fr/home/ ~fdadeau/praspel.html, along with the links to download the Hoa framework (implementing Praspel), and some samples of the possibilities of Praspel.

Related Works

Various works consider Design-by-Contract for unit test generation [START_REF] Bouquet | Automated Boundary Test Generation from JML Specifications[END_REF][START_REF] Cheon | A simple and practical approach to unit testing: The JML and JUnit way[END_REF][START_REF] Ciupa | ARTOO: Adaptive Random Testing for Object-Oriented Software[END_REF][START_REF] Heidegger | Contract-Driven Testing of JavaScript Code[END_REF][START_REF] Madsen | Unit Testing using Design by Contract and Equivalence Partitions[END_REF]. Our approach is inspired by the numerous works on JML [START_REF] Leavens | JML: A notation for detailed design[END_REF]. Especially, our test verdict assignment process relies on Runtime Assertion Checking, which is also considered in JMLUnit [START_REF] Cheon | A simple and practical approach to unit testing: The JML and JUnit way[END_REF], although the semantics on exceptions handling differs. Recently, JSConTest [START_REF] Heidegger | Contract-Driven Testing of JavaScript Code[END_REF] uses Contract-Driven Testing for JavaScript. We share a common idea of adding types to weakly typed scripting languages (JavaScript vs PHP). Nevertheless our approach differs, by considering flexible contracts, with type inheritance, whereas JSConTest considers basic typing informations on the function profile and additional functions that must be user-defined. As a consequence, due to a more expressive specification language, Praspel performs more general runtime assertion checks. ARTOO [START_REF] Ciupa | ARTOO: Adaptive Random Testing for Object-Oriented Software[END_REF] (Adaptative Random Testing for Object-Oriented software) uses a similar approach based on random generation involving contracts written in Eiffel [START_REF] Meyer | Eiffel: programming for reusability and extendibility[END_REF], using the AutoTest tool. ARTOO defines the notion of distance between existing objects to select relevant input test data among the existing objects created during the execution of a program. Our approach differs in the sense that object parameters are created on-the-fly using the class invariant to determine relevant attributes values, in addition to the function precondition. Praspel presents some similarities with Eiffel's types, especially regarding inheritance between realistic domains. Nevertheless, realistic domains display the two properties of predicability and samplability that do not exist in Eiffel. Moreover, Praspel adds clauses that Eiffel contracts do not support, as @throwable and @behavior, which are inspired from JML.

Our test generation process, based on random testing, is similar to Jartege [START_REF] Oriat | Jartege: A Tool for Random Generation of Unit Tests for Java Classes[END_REF] for JML. Jartege is able to generate a given number of tests sequences of a given length, for Java programs with JML specifications. Jartege uses the type of input parameters to compute random values for method parameters, that are then checked against the precondition of the method, using an online test generation approach.

Also for JML, Korat [START_REF] Boyapati | Korat: Automated Testing based on Java Predicates[END_REF] uses a user-defined boolean Java function that defines a valid data structure to be used as input for unit testing. A constraint solving approach is then used to generate data values satisfying the constraints given by this function, without producing isomorphic data structures (such as trees). Our approach also uses a similar way to define acceptable data (the predicate feature of the realistic domains). Contrary to Korat, which automates the test data generation, our approach also requires the user to provide a dedicated function that generates data. Nevertheless, our realistic domains are reusable, and Praspel provides a set of basic realistic domains that can be used for designing other realistic domains. Java PathFinder [START_REF] Visser | Test input generation with Java PathFinder[END_REF] uses a model-checking approach to build complex data structures using method invocations. Although this technique can be viewed as an automation of our realistic domain samplers, its application implies an exhausive exploration of a system state space. Recently, the UDITA language [START_REF] Gligoric | Test generation through programming in UDITA[END_REF] makes it possible to combine the last two approaches, by providing a test generation language and a method to generate complex test data efficiently. UDITA is an extension of Java, including non-deterministic choices and assumptions, and the possibility for the users to control the patterns employed in the generated structures. UDITA combines generator-and filter-based approaches (respectively similar to the sampler and characteristic predicate of a realistic domain).

Finally, in the domain of web application testing, the Apollo [START_REF] Artzi | Finding bugs in dynamic web applications[END_REF] tool makes it possible to generate test data for PHP applications by code analysis. The tests mainly aim at detecting malformed HTML code, checked by an common HTML validator. Our approach goes further as illustrated by the experimentation, as it makes it possible not only to validate a piece of HTML code (produced by a Praspel-annotated function/method), but also to express and check structural constraints on the resulting HTML code. On the other hand, the test data generation technique proposed by Apollo is of interest and we are now investigating similar techniques in our test data generators.

Conclusion and Future Works

In this paper, we have introduced the concept of realistic domain in order to specify test data for program variables. Realistic domains are not types but may replace them in weakly-typed languages, such as Web languages like PHP, our implementation choice. Realistic domains are a (realistic) trade-off between two extreme ways to specify preconditions: a too coarse one with types and a too fine one with first-order formulas. They provide two useful features for automated test generation: predicability and samplability. Predicability is the ability to check the realistic domain of a data at run time, whereas samplability provides a means to automatically generate data values matching a given real-istic domain. Realistic domains are specified as annotations in the code of the language. We have implemented these principles on PHP, in a dedicated specification language named Praspel, based on the Design-by-Contract paradigm. This approach is implemented into a test generator that is able to (i) generate automatically unit test data for PHP methods, using a random data generator that produces input parameter values that satisfy the precondition, (ii) run the tests and (iii) check the postcondition to assign the test verdict. Praspel implements the two features of runtime assertion checking and test data generation independently. As a consequence, the user is not restricted to use a random test data generator and can write his own test data generator.

We are currently investigating the improvement of our data generator, to replace randomly generated values by a constraint-based approach [START_REF] Demillo | Constraint-Based Automatic Test Data Generation[END_REF] for which the realistic domains of input parameters would be used to define data domains. Constraint solving techniques will then be employed to produce test data that satisfy the precondition of the method, as in Pex [START_REF] Tillmann | Pex: White box test generation for[END_REF]. We are also planning to consider a grey-box testing approach that would combine a structural analysis of the code of PHP methods, coupled with the definition of the realistic domains of their input parameters. Finally, we are interested in extending (and generalizing) the concept of realistic domains to other programming languages, especially those already providing a type system, to illustrate the benefits of this concept.

Fig. 2 .

 2 Fig. 2. Grammar of the concrete syntax

Example 3 (

 3 Use of a class as a realistic domain). The following declaration: o: class('LimitIterator') or class('RegexIterator') specifies that o is either an instance of LimitIterator or RegexIterator.

Fig. 6 .

 6 Fig. 6. Behavioral Contracts

  public function foo ($x1 ...) { $this->foo pre(...); // evaluation of \old(e) try { $result = $this->foo body($x1 ... ); } catch ( Exception $exc ) { $this->foo exception($exc); throw $exc; } $this->foo post($result, ...); return $result; } public function foo pre(...) { return verifyInvariants(...) && verifyPreCondition(...); } public function foo post(...) { return verifyPostCondition(...) && verifyInvariants(...); } public function foo exception($e) { return verifyException($e) && verifyInvariants(...); } public function foo body($x1 ... ) ...

Fig. 7 .

 7 Fig. 7. PHP Instrumentation for Runtime Assertion Checking

Fig. 8 .

 8 Fig. 8. Test Cases Generation Algorithm