Pr Farouk Rémi Toumani

Dr Marinette Bastide

Pr Michel Bouet

Schneider

Yahia, Lakhder, Karima, Kawther, Nader, Maxime, Raksmey, Libo, Diyé Marie I Doutoum

Keywords: Timed Automata, Domain Specic Language, UPPAAL Model Checker, Home Care Plan. Contents Conclusion Bibliography

also would like to thank my friends who are having become meantime as my little family here in Clermont-Ferrand. Meriem

Résumé

Dans cette thèse nous nous sommes intéressés aux problèmes concernant la conception et la gestion des plans de soins à domicile. Un plan de soins à domicile dénit l'ensemble des activités médicales et/ou sociales qui sont menées jour après jour au domicile d'un patient. Ce plan de soins est généralement construit à travers un processus complexe impliquant une évaluation complète des besoins du patient ainsi que son environnement social et physique. La spécication de plans de soins à domicile est dicile pour plusieurs raisons: les plans de soins à domicile sont par nature des processus non structurés qui impliquent des activités répétitives mais irrégulières, dont la spécication requiert des expressions temporelles complexes. Ces caractéristiques font que les plans de soins à domicile sont diciles à modéliser en utilisant les technologies traditionnelles de modélisation de processus. Tout d'abord, nous présentons l'approche basée sur les DSL (Langage spécique au domaine) qui permet d'exprimer les plans de soins à domicile en utilisant des abstractions de haut niveau et orientées utilisateur. Le DSL nous permet à travers cette thèse de proposer un langage de temporalités permettant de spécier les temporalités des activités du plan de soins à domicile. Ensuite, nous décrivons comment les plans de soins à domicile, formalisés grâce aux automates temporisés, peuvent être générés à partir de ces abstractions. Nous proposons une approche en trois étapes qui consiste à: (i) le mapping entre les spécications temporelles élémentaires et les automates temporisés appelés "pattern automata", (ii) la combinaison des "patterns automata" an de construire les automates d'activités en utilisant l'algorithme de composition que nous avons déni, et aussi (iii) la construction de l'automate de plan de soins à domicile global. L'automate de plan de soins à domicile résultant englobe tous les schedules autorisés des activités pour un patient donné. Enn, nous montrons comment la vérication et le suivi de l'automate du plan de soins à domicile résultant peuvent être faits en utilisant des techniques et des outils existants, en particulier en utilisant l'outil de verication UPPAAL.

Mots clés : Automates temporisés, Langage spécique au domaine, Outils de verication UPPAAL, Plan de soins à domicile.

List of Figures

General introduction

A general trend that can be observed these recent years in health domain is the development of the home care. Home care refers to health care or supportive care delivered by health care professionals at patients' homes. The target objective for social and economic reasons is to enable people who require care to remain at home instead of having longterm stays in hospitals or health establishments. Several types of care may be provided at patient's home including health services, specialized care such as parenteral nutrition or activities related to daily living such as bathing, dressing, toilet, etc. All the medical and social activities delivered for a given patient according to certain frequencies are scheduled in a so-called home care plan. In [START_REF] Fnehad | La télésanté: un nouvel atout au service de notre bien-être[END_REF], the home care plan is dened as "a provisional list of treatments to achieve which may include activities and treatments, prescribed or not, associated with the frequency and schedules". Hence, the notion of a home care plan is a key concept in home care. As a part of the project Plas'O'Soins1 (Plateforme d'Aide au Suivi et à la cOordination des activités de Soins à domicile), we are interested by the problems underlying the design and management of the home care plans in order to bring some comfort to the coordinator, avoid the collision when planning activities or to ensure the feasibility of the home care plan, etc.

The design of a home care plan is challenging for several reasons. First, process modeling in the medical eld is in general not an easy task [START_REF] Dadam | Clinical workows -the killer application for process-oriented information systems ? Business[END_REF]. Indeed, medical processes require usually complex coordination and interdisciplinary cooperation due to involvement of actors from various health care institutions. Moreover, home care plans display the following features that make them dicult to handle with traditional Business Process Management (BPM) technologies:

• Home care plan can be viewed as a collection of repetitive activities (e.g., medical activities) which are repeated during a given period. The activities are however enacted according to an irregular schedule. The irregularities of an activity have two main causes. First, the activity very often has to follow the evolution of the needs which is usually irregular. This type of irregularity is characterized by strengthening or weakening in the rhythm of realization. Then, an activity which requires human resources has to respect life cycles appropriate to this type of resources and in particular rest time of the weekend. This type of irregularity induces interruptions 2 General introduction in the rhythm of the realization. Specication of irregular activities requires the use of suitable temporal constraints.

• Home care plans are essentially unstructured processes in the sense that each patient has his/her own specic care plan. Indeed, the home care plan for each patient is developed on an individual basis because each patient is unique whether at his/her pathology or needs. Therefore, it is simply not possible to design a unique process capturing in advance the care plans of all the patients. In other words, the traditional approach model once, execute many times is not sustainable in our context.

• Home care plans are associated with complex temporal constraints. Indeed, the design of a home care plan requires the specication of the frequencies of the delivered home care activities. Such specications are expressed by healthcare professionals in natural language, using usually a compact repetitive form: everyday in the morning, once every 2 days in the evening during 15 days, etc. But they may also have irregularities or exceptions: Mondays and Fridays, except public holidays.

Given the crucial role played by temporal constraints in home care plans, it appears clearly that such specication could take benet from existing theory and tools in the area of timed systems. There exist in the literature many formal models enabling explicit representation of timed systems [START_REF] Alur | Model-checking for real-time systems[END_REF][5] [START_REF] Alur | A theory of timed automata[END_REF][8][9] [START_REF] Berthomieu | Modeling and verication of time dependent systems using time petri nets[END_REF]. Among the well-known formalisms, we have time extensions for Petri Nets(PNs) [START_REF] Bowden | A brief survey and synthesis of the roles of time in petri nets[END_REF] and Timed Automata(TA) [START_REF] Alur | A theory of timed automata[END_REF] [START_REF] Cassez | Structural translation from time petri nets to timed automata[END_REF].

Petri Nets were introduced in the 1960's by Carl Adam Petri as a graphical and mathematical modeling tool. It consists of four elements: places (represented by circles), transitions (represented by rectangles), edges also called arcs (represented by directed arrows) and tokens (represented by small solid (lled) circles). The initial model of Petri Nets was atemporal. There exist several extensions that take into account time constraints among which: Time Petri Nets (TPNs) [START_REF] Meir | A Study of the Recoverability of Computing Systems[END_REF] where a time interval is assigned to each transition, Timed Petri Nets (TdPNs) [START_REF] Ramchandani | Analysis of asynchronous concurrent systems by timed petri nets[END_REF] whose transitions have exact duration.

Other representations of time may involve places, called timed places Petri nets [START_REF] Sifakis | Use of petri nets for performance evaluation[END_REF] or arcs, called timed arc Petri nets [START_REF] Hanisch | Analysis of place/transition nets with timed arcs and its application to batch process control[END_REF]. Among all these time variants, TPNs are most widely used for the expression of a large majority of temporal constraints [START_REF] Berthomieu | An enumerative approach for analyzing time petri nets[END_REF][ 36] [START_REF] Jerey | Timing constraint petri nets and their application to schedulability analysis of real-time system specications[END_REF].

In addition to Petri Nets, another well-known model has been extended to represent the time constraint: Timed Automata were introduced in [3] [START_REF] Alur | A theory of timed automata[END_REF] as an extension of nite state automata that enables explicit modeling of time. Informally, Timed Automata are nite states automata enriched with clock variables. Moreover, transitions of timed automata are annotated with guards, expressed as time constraints, and clock resets.

Several contributions aiming to compare TPN and TA have been made [START_REF] Berthomieu | Bridging the gap between timed automata and bounded time petri nets[END_REF][32] [33][38].

Formalisms of TPN and TA show lots of common characteristics such as: they allow both to model real-time systems and have specic tools for properties verication [START_REF] Srba | Comparing the expressiveness of timed automata and timed extensions of petri nets[END_REF]. Also they show the extreme diculties to handle algorithmic analysis of timed models, for example, Timed Automata suer from undecidability problems of language inclusion and complementation [START_REF] Alur | A theory of timed automata[END_REF], and Time Petri Nets from undecidability problem of reachability [START_REF] Neil | Complexity of some problems in petri nets[END_REF]. Even though both are likely to meet our expectations, we use in our approach Timed Automata. The advantage of TA formalism is that the problem of reachability is decidable in polynomial space [START_REF] Alur | A theory of timed automata[END_REF]. Also Timed Automata benet from a very active theoretical research, which among other things allowed to develop very ecient tools such as Uppaal [START_REF] Behrmann | A tutorial on uppaal[END_REF] or Kronos [START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF]. In our work, Timed Automata will be used as a basis to develop a formal framework to analyze home care plans.

As mentioned, we adopt as referring formal model for the specication of home care plans, the model of Timed Automata. However, due to the complex features of home care plans, it is not feasible to ask home care professionals to construct such formal specications nor to use traditional process modeling technologies [START_REF] Weske | Business Process Management: Concepts, Languages, Architectures[END_REF], usually based on GUI (Graphical User Interface), to design a home care plan process and then to automatically generate the corresponding timed automaton. To cope with such diculties, we describe below the main features of our approach:

• The cornerstone of our approach lies in the denition of a Domain Specic Language (DSL) and a user centred specication language tailored to express home care plans using high level abstractions. We conducted a thorough analysis of current practices of home care professionals, in particular home care coordinators, in order to identify the main elementary temporal expressions used in this context. The DSL framework incorporates a GUI which is intended to be used in particular by the coordinator, to specify patient's home care plans.

• In order to ensure the feasibility of the home care plan and the non collision of dened activity, we propose an automatic transformation of user specications into timed automata. This approach enables home care professionals to continue using a constrained form of a natural language to express complex temporal constraints (through a GUI), while being able to generate automatically timed automata-based

General introduction

specications of home care plans. In fact, the home care plan consists of a set of activities which are at their turn dened by a set of elementary temporal specications that specify their scheduling. Thereby, building the home care plan timed automata involves the following steps:

1. Pattern automaton construction: The identication of the elementary patterns that are useful to specify home care plans. Each elementary temporal expression is formalized in the form of a timed automaton called pattern automaton. This pattern captures the temporal constraints of an elementary temporal specication and also the duration of the associated activity.

Activity automaton construction:

The use of these elementary patterns to specify atomic activities. In fact, pattern automata are combined together using specic composition operator tailored to take into account the specic semantics of health care activities. The composition generates the activity automaton (i.e., the timed automaton specifying the schedule of a given activity).

3. Home care plan automaton construction : The automatic construction of a global home care plan by composition of the basic activities. The global home care plan automaton is generated using the composition operator. A timed word of such an automaton corresponds to a possible legal schedule of the activities and hence a care plan automaton describes all the possible legal schedules of a home care plan for a specic patient.

• The obtained formal specications are exploited to support automatic verication and monitoring of home care plans. For example, we show that realizability of home care plan, which asks wether there is a schedule of activities that satises the plan, is reduced to the emptiness of the corresponding timed automaton while some monitoring issues are reduced to the membership or language recognition.

Interestingly, the important task of the coordinator consists in grouping together the activities of home care plan in a set of Interventions while trying to minimize the total number of interventions at patient's home and also to reduce the overall cost of home care. Interventions generation can be computed automatically using a specic composition operator while ensuring some required properties (e.g., interleaving interventions are not allowed, idle time between the activities of a same intervention is controlled, etc. ).

The thesis is organized as follows. Chapter 1 describes the general context of this work and its main challenges. Chapter 2 introduces main concepts of Domain Specic Languages (DSL) and Timed Automata and application of these approaches in the medical eld. Chapter 3 presents the contribution of this thesis which consists in modeling and analyzing home care plans. First, we describe the DSL based approach in which we identify the main building blocks in the home care plan and we propose a language that enables to express regular or irregular repetitions of an activity within some period in a condensed form similar to that used by doctors. Then, the general modeling process is presented together with the construction of the proposed automata, i.e., pattern automata, activity automata and home care plan automata. We also present some verication and monitoring issues using UPPAAL Model Checker. The validation step of our work is presented in the prototyping part (Chapter 4) in which we show the architecture of the prototype and we describe the implementation details. Finally, we conclude this manuscript by recalling the contribution of this thesis and discuss some future research directions.

Chapter 1

Context and problematic

Chapter 1. Context and problematic

The home care is a starting point of this thesis. The trend is to consider the home care as a unied way, even if it encompasses intervention of dierent types of structures.

To ensure a good organization, quality and eciency of care, coordinators organize and translate the various treatments to achieve in a corresponding home care plan. The home care plan is the main component of the home care, since it allows to coordinate dierent activities being performed and the various actors (physician, nurse, nurse auxiliary, liberal helper, etc.) involved in the home care as well as it's the input element to the intervention planning.

In this chapter, we present the context in the eld of home care, highlighting its major challenges which prompted in this context the development of projects based on Information and Communication Technologies (ICT) among which the Plas'O'Soins project 1 . This latter will be described in the second part. Finally, we present the contribution of this thesis associated with this project.

Home care area

In recent years, home care landscape has undergone a signicant evolution. This is mainly due to the major concerns of actual societies which aim to manage ageing population and to cope with the congested hospitals and centers [START_REF] Jagger | Economic evaluation of hospital at home versus hospital care: cost minimisation analysis of data from randomised controlled trial[END_REF]. Indeed, elderly people with loss of autonomy are especially vulnerable and often exhibit chronic diseases requiring continuous care for a long term. Keeping such a population in its social environment is a key point to avoid any risk of depression or exclusion, especially, when other factors are involved such as: children living further away, or family dispersal [START_REF] Bergman | Vieillissement et soins, l'urgence d'orir des services de santé intégrés aux familles du xx1ème siècle[END_REF] [START_REF] Gagnon | Intégrer les services pour le maintien de l'autonomie des personnesprisma (prog. de recherche sur l'intégration des services pour le maintien de l'autonomie)[END_REF]. Thus, alternative structures to traditional hospitalizations have emerged. For example: (a) Hospitalization At Home, a sanitary alternative which is generally provided for patients with serious diseases; (b) Nursing Home Service, a medico-social logic which provides nursing care and general hygiene to elderly people; and (c) Maintaining At Home, a set of home services, which provides help to the addict people to allow them staying at home as long as possible, help (such as domestic help, etc.).

The development of home care is motivated by economical and political reasons [START_REF] Fnehad | La télésanté: un nouvel atout au service de notre bien-être[END_REF][91] that try to control the health care costs; the demographic issue related to the ageing population; the social aspects related to the patient's wishes, as well as by technology advances where the progress on ICT contributes to the improvement of the home 10 Chapter 1. Context and problematic

Home care actors

The home care area implies an interdisciplinary cooperation due to the involvement of actors from various health care institutions. We can distinguish several types of actors [START_REF] Ben | Pilotage opérationnel des structures d'hospitalisation à domicile[END_REF][20] [START_REF] Chahed | Modelisation et analyse de l'organisation et du fonctionnement des structures d'hospitalisation á domicile[END_REF][98]:

• Treating physician: he is freely chosen by the patient. Her agreement is a necessary condition for the patient's home care acceptance.

• Home care coordinator: he is the physician who is in charge of the control activities and care coordination between dierent health professionals. Her main tasks are [START_REF] Bastide | Plas'o'soins: A software platform for modeling, planning and monitoring homecare activities[END_REF]:

Elaborating the patient's home care plans and updating them according to the evolution of the patient's health state on the advice of the treating physician.

Monitoring the execution of the home care activities: from the information provided by dierent involved actors, the coordinator can be informed about the duration in the performance of activities.

• External or internal actors: actors can be full time employees (internal actors of the home care structure) or part-time employees (external actors). These actors are regularly involved at the patient's home such as:

Nurse: she evaluates the conditions of the patient receiving home care services and provides skilled nursing care and veries if other services are required.

Nurse auxiliary: she is involved in the general hygiene care (toilet, dressing, bathing, etc) in the oversight of treatment taking, transfer, displacement inside home, etc.

Nutritionist: he supports the patient for the nutrition phases.

Therapist: such as pathologist who takes into account therapy needs.

• Social workers: they assist the patient and his/her family in their formalities to obtain material and nancial support.

• Patient's family, friends, etc.: they contribute in the patient's home care for free. Family members or neighbors participate regularly or occasionally to provide various services to overcome the patient's disability. The medical and social care delivered for a given patient during the home care can be listed as follows [START_REF] Tarricone | The solid facts: Home care in europe[END_REF]:

• Punctual care: it represents technical and complex care adapted to a not stabilized pathologies for determined period.

• Continuous care: it represents technical care of varying complexity. This type of care can vary from nursing care to maintain functioning levels for progressive pathologies.

• Rehabilitation care: this care is intended for patients after the acute phase of a neurological disease, orthopedic, cardiology or poly pathology for a xed duration.

• Home help services: these services are provided by social service structures such as household duties (shopping, cooking, cleaning, etc) and general hygiene services (bathing, dressing, toilet, etc).

Home care processes

Home cares involve complex and various processes and information exchanges. Figure 1. 3 shows a generic vision of the home care processes proposed by FNEHAD [START_REF] Fnehad | La télésanté: un nouvel atout au service de notre bien-être[END_REF]. This cartography follows the ISO 9000 standard which classies the home care processes into three types: (1) Management processes, these processes contribute to set the target objectives of the home care, (2) Support processes (human resources, purchasing and logistics, IS management, etc.); these processes are essential for the proper functioning of the home care, they allow the allocation of necessary resources to ensure that the home care meets the patient's needs, (3) Operational processes (processing of admission request, delivery of care, coordination and monitoring of care, etc), these are the most important processes in home care; indeed they manage the care in order to ensure the patient's satisfaction.

Operational processes have already been considered in the literature [START_REF] Rajeb | Proposition d'un cadre méthodologique pour le management de la continuité d'activité : application à la prise en charge à domicile[END_REF] [START_REF] Zefouni | Aide à la conception de workows personnalisés : application à la prise en charge à domicile[END_REF]. One of their most important features is the "singularity", i.e. each process is specic to each patient. This is mainly reected by the design of Home care plan which is specic to each patient [START_REF] Zefouni | Aide à la conception de workows personnalisés : application à la prise en charge à domicile[END_REF].

Chapter 1. Context and problematic ity (I2HOME), a solution allowing the elderly or disabled people to control the various electronic devices of their homes using their mobile phones or other objects [START_REF] Rajeb | Proposition d'un cadre méthodologique pour le management de la continuité d'activité : application à la prise en charge à domicile[END_REF]. (2) Remote monitoring (CAALYX, eCAALYX), solution dedicated to older or elderly persons at their home, it consists to collect ve various vital signs and detect anomalies [START_REF] Rajeb | Proposition d'un cadre méthodologique pour le management de la continuité d'activité : application à la prise en charge à domicile[END_REF]. (3) COPLINTHO 3 , a communication platforms allowing the interaction between all involved actors in the care process and which puts the patient in a central position, etc. We will present in what follows some ICT tools used in the home care area.

Overview on main software tools

There are a multitude of tools based on the ICT domain that improve the quality of the patient home care. Some are based on remote monitoring systems PROSAFE [START_REF] Estéve | Prosafe-extended, a telemedicine platform to contribute to medical diagnosis[END_REF]), others on telealarm systems (presence verte4 [START_REF] Zefouni | Aide à la conception de workows personnalisés : application à la prise en charge à domicile[END_REF]), or systems enabling to remotely establish the medical diagnosis (ViSaDom [START_REF] Provost | Téléassistance en hospitalisation à domicile: le programme visadom[END_REF], DIATELIC5 [START_REF] Zefouni | Aide à la conception de workows personnalisés : application à la prise en charge à domicile[END_REF]). In the following we present some tools in order to identify their specicity, their covered activities, their operating mode and their limitations.

• AtHome of ARCAN6 : ARCAN is a software editor for managing personal home care coordination. AtHome is a software solution specic to each home care structure.

AtHome manages all home care information (patient, billing, purchasing, inventory, communication and administration, etc.).

• Apozem7 : is a software designed for some home care structures. Apozem manages all forms of home care support of the elderly people. It also manages the patient and his/her home care support (home care plan, transmission, etc.), and the edition of regulatory statements (medical register, annual activity report, etc.).

• Medlink8 : is an integrated IT solution, specic to each home care structure.

Medlink allows to improve the quality of care while reducing administrative tasks and costs. It also provides an access control (read, write, view) according to the role of involved actors.

• Hippocad9 : oers an application architecture based on a process approach and focuses on the operational home care of the patient's therapeutic project. Hippocad includes control services in the realization of home services, manages emergencies, unforseen and delay in a reactive manner, and integrates automatically the various reports.

In spite of the fact that these tools have the advantage of improving the home care support by providing means of traceability, driven alerts to the involved actors and information restitution in a real time (e.g., personalized report), etc., they are still far from meeting the identied diculties. Indeed, these tools are not suitable, they are dicult to handle.

They are not able to deal with patient constraints (patient constraints in a textual form and are unexploited, no patient agenda, etc.). The home care plan description is made in an unstructured manner, and the planned interventions are adjusted manually. And generally these tools lack of patient-centred sharing infrastructure.

Plas'O'Soins Project

Plas'O'Soins is a cooperative project nanced by the ANR 10 , the French National Research Agency (Agence Nationale de la Recherche). The project consortium brings together academic and industrial of the ICT and health domain and end-users from dierent home care structures in France. The objective of Plas'O'Soins is to set up a hardware and software platform designed to address the needs of the home care structures. The needs in terms of coordination, planning and monitoring of patient's care and actor's activities ensuring continuity of care for a patient in his overall care support.

The proposed hardware and software platform allows to store all useful information (patient's prole, protocols, prescriptions, interventions, analysis results, etc) and their evolution, in order to provide at any moment :

• The restitution of the current state of the patient's home care process, globally or with a specic vision tailored to the concerned actor's prole.

• The timely reporting of information (alerts, arrived on site, delays, schedule changes, etc) towards the appropriate actor whether a service emergency, a social actor, doctor, family, etc. • "Patient discharge" process: it allows the edition of the exit documents, as well as archiving and transmission of eventual information tailored to another concerned structure.

• "Home care organization" process: this central process of the platform is specic to each patient. Indeed the patient's home care is carried out through three main activities: the design of the home care plan, the planning of the home care and the monitoring of the home care. The design of the home care plan is the initial activity that determines the two others. Collaborations between these activities can be dened as shown in Figure 1.4 (the numbers refer to those in Figure 1.4):

1: First, the platform assists the coordinator in the design of the home care plan (provisional list of activities, involved actors, etc) which corresponds to the provisional home care plan. The information which compose the provisional home care plan are made available to the planning activity; 2: The planing activity indicates that the home care plan was planned within a determined time (e.g., week 51 of the current year). If a solution is not found, the home care plan should be reviewed and re-planned or manual planning is imposed by the coordinator; 3: The planned home care plan is available at any moment by the monitoring activity;

4: An identied problem at the care execution can lead to the modication of current planning, but keeping the same home care plan; 5: An identied problem at the care execution can require the modication of the current home care plan (and thus the creation of a new version of the home care plan) thus, a new planning is necessary; 6: An identied problem at the care execution may require warnings for continuing the home care support without trigger a change in the planning or a modication in the home care plan. This decomposition into three activities induces three visions of the home care plan:

(1) the provisional home care plan, which consists of scheduled activities to do at patient's home, [START_REF] Alur | Symbolic analysis of hybrid systems[END_REF] the planned home care plan, which consists of planned activities to do at patient's home, and (3) the realized home care plan,which consists of activities Chapter 1. Context and problematic already realized at patient's home. These three home care plans VISIONS must be managed simultaneously.

Our contribution within Plas'O'Soins project

Our work focuses on the design and analysis of the home care plan. To achieve this goal, we conduct the following steps:

• The Requirement analysis;

• The Denition of the Domain Specic Language (DSL);

• The denition of the formal model using Timed Automata theory;

• The implementation of the proposed model.

Note that, In the rest of this thesis, we will talk about the home care plan referring to the provisional home care plan. In the following, we will describe the requirement analysis. The other steps will be presented in the next chapters.

Requirement analysis

We conducted an on site analysis to understand the main concepts underlying the home care plan in the patient's home care. More precisely, we carried out interviews and observation phases with two home care structures: UMT-Mutualité Tarnaise and Centre Hospitalier d'Albi. During this phases, we were able to access and to collect several anonymized home care plans.

Thanks to the collected information, we could understand the manipulated data, the work of the involved actors especially the coordinators and the various diculties related to the design of the home care plan. Thus, home care plan is dened as a provisional list of care activities to be performed in the patient's home care. Home care plan encompasses all the services provided for a given patient and is essential to scheduling the delivery of such services at patient's home by health care professionals. More precisely, home care plan is a personalized list of care to achieve in a considered home care. It regroups activities which comprise a frequency (e.g., 3 times a week, everyday, on June 12th, etc), a period (e.g., from 01/01/2015 to 05/31/2015), an interval (e.g., morning, afternoon or evening), a duration in terms of 1.3. Requirement analysis minutes (e.g., 30mn, 15mn, etc.), and a required qualication (e.g., nurse auxiliary, nurse, etc.). During the patient's home care period, the home care plan may change or evolve according to the evolution of the patient's health conditions.

In the following, we will present the results concerning this requirement analysis.

Involved actors in home care plan

Once the patient is supported by a home care structure, a comprehensive assessment of his/her needs must be taken into account, e.g., medical, social and psychological needs. This evaluation which usually takes place at patient's home, can be realized in one or more stages and involves various actors. Each actor brings his/her skills and contributes to the evaluation depending on the patient's health complexity. Among these actors we nd social worker, therapist, attending physician, nurse, etc. Patient's family and helpers can contribute in this evaluation stage in order to be involved in the home care plan.

All the collected information will allow to the home care coordinator producing the home care plan.

Home care plan activities

A home care plan can be viewed as a collection of repetitive activities. A home care plan activity corresponds to the notion of medical or social activity (e.g., nursing activity or dressing, bathing activities). The care activity duration can vary from few minutes to hours. A same activity may occur several times in the same day. Some activities can take place at any time (e.g., monitoring of some parameters ), others must be conducted in a fairly specic interval (e.g., between 8am and 9am for mobilization activity) or in a precise time (e.g., at 6pm for example for the lovenox injection activity). A home care plan activity is also dened by a period, which can be the same as the period of the home care plan or dierent (e.g., from 01/01/2013 to 03/31/2015) and the required qualication (e.g., nurse , nurse auxiliary, etc).

Irregular activities are inherent to the home care plans because the activity very often has to follow the evolution of needs of the patient. For example, a given activity toilet may be associated with complex frequency, e.g., every two days except Sunday evening.

Example of a home care plan

The home care plan is used in all home care structures and is mainly expressed through a paper format. Figure 1.5 shows a real example of home care plans that have been made anonymous for condentiality reasons. The home care plan content may vary form one home care structure to another. Here we give the general elements that can be described in a home care plan.

• Period of the home care plan: corresponds to the period of validity of the home care plan (e.g., from 01/01/2015 to 01/01/2016).

• Activities: in the home care plan all the activities are described with their temporalities (e.g., Toilet every day in the morning, dress on Monday Wednesday and Friday evening, etc). Each activity is associated with a duration and an actor type (in some cases the number of involved actors is specied).

• Medicine: drug prescription by the attending physician is managed by the home care structure through the home care plan. Each drug is described by a name and temporalities which correspond to the administering time.

• Material: in the home care structures, the patient must have a material prescription in adequacy with his/her pathology. e.g., anti-bedsore mattress, medical bed, etc.

Each material is associated with a temporal information.

• Consumable: a set of consumable is used to support the patient's home care. e.g., syringes, examination gloves, thermometers, etc.

As a part of this thesis, we focus on the activities.

Elaboration of home care plan

The home care plan is present in all home care structures. Designing and monitoring of the patient's home care plan are fundamental activities for a successful patient's home care. Figure 1.6 which is based on the corpus of on-site information analysis, shows how the patient's home care plan is carried out:

1. Design the home care plan. Firstly the coordinator creates the home care plan for each patient using a comprehensive assessment of the patient needs as well as his/here social and physical environment. The care plan is generally written in a paper format and can be updated at any moment by the coordinator; • A home care plan is associated to complex temporal constraints. Indeed, it is necessary to specify the frequency (more or less regular) of every home care plan. This specication is expressed by health care professionals in natural language by using specic expressions: every day in the morning and in the evening, once every 2 days in the evening during 15 days, etc.

• A home care plan is needed for planning. In fact during the existing analysis in dierent home care structures, we noticed the absence of interventions generation mechanism. Everything is done manually by the coordinator. Manual support of the planning activity can in some cases (for a complex home care plan) increase the error risk. For example, planning an intervention that will be impossible because the coordinator forgot to take into account the involved actor's unavailability. Another possibility is the diculty to propose an optimal planning. This diculty is mainly due to the fact that the human capacity can not compute all possible combinations of interventions in order to choose the best conguration.

In this context, and within Plas'O'Soins project, we are interested in the problem underlying the elaboration of the home care plan by the coordinator.

Objective of the thesis

To cope with the aforementioned problems, we propose to adopt the following approach:

• The denition of the user-centred DSL, used to describe the main concepts of the home care plan at a high abstraction level. DSLs are already widely used in the elds of computer science an mathematics, and are recently used in the medical area [START_REF] Van Den Berg | A domain specic language for performance evaluation of medical imaging systems[END_REF]. The DSL will describe the home care plan activities and their relationships. It will be dened through a temporality model that will allow to specify intervals of realization for repetitive activities of the home care plan, where the repetitions can present irregularities and exceptions. This model will allow the coordinator to describe by himself the specicities of the home care plan. The DSL framework incorporates a GUI which is intended to be used in particular by the coordinator in their daily activities, which consists to manage and to evolve the home care plan, and to monitor the execution of the programmed activities by the involved actors at home.

[53][56][83][84][109]

Chapter 1. Context and problematic

• The denition of an automatic transformations of user specications into formal model based on timed automata. This transformation is indispensable to perform any kind of verication and monitoring of the home care plan.

• The verication and monitoring execution of the home care plan. Among the verication that we have identied, there is a realizability checking of the home care plan, the intervention generation, and the monitoring of the home care plan. While checking the realizability is proper to our work, the monitoring and interventions generation are identied within the project. However, the last two are developed separately from our work using a traditional approach based on existing algorithm and on business rules. As part of this thesis we propose an approach based on timed automata.

Conclusion of Chapter 1

In this chapter, we presented the home care area and highlighted its main modeling challenges. Much work has already been achieved in this area, but there is still not a satisfactory solutions. We described the conducted requirement analysis which consist in carrying a set of interviews and collect and analyse some scripts documents. This requirement analysis has led us to dene problems faced by the coordinator during the home care plan elaboration. Response elements were outlined, especially by addressing two scientic aspects regarding DSL and timed automata.

The domain specic language and the timed automata formalism will be subject of a detailed presentation in the next chapter.

Chapter 2 In section 2.1 of this chapter, we present an overall view of the DSL concepts, its denition, its main advantages that have strengthened our choice together with some disadvantages, its development process steps, as well as some related work that used DSL in the medical eld.

State of the art

The section 2.2 is dedicated to the presentation of timed automata. We begin with some background knowledge on timed automata. Then we describe some extensions and subclasses of timed automata that we consider useful in the context of this thesis. We consider mainly the extension that takes into account activities with duration. Also, we present the software tools that enable model checking using timed automata. Before concluding, we present some existing works that use timed automata in the medical eld.

Domain specic language

With the increasing of human needs, software engineering becomes more and more complex and sophisticated. Applications must be at the height of performance expected by the users. Over the years the trend of software engineering is to always increase the abstraction level of the programming languages [START_REF] Helène | Des langages de modélisation dédiés aux environnements de métamodélisation dédiés[END_REF].

The level of programming languages can be summarized as follows (1) low-level programming languages, which are more machine oriented languages (e.g., Assembler, etc.),

(2) third-generation programming languages, which are more problem-oriented languages that try to answer to a wide class of problems (e.g., C, C++, etc.), and more recently (3) Domain Specic Language. While the (1) and (2) do not always permit optimal way to answer to a given problem, the DSL on the contrary allows to oer a solution more specic and less complex [START_REF] Mercadal | Approche langage au développement logiciel : application au domaine des systèmes d'informatique ubiquitaire[END_REF] [START_REF] Tolvanen | Domain-specic modeling for full code generation[END_REF]. Indeed, by focusing on a particular domain, it is easier to learn about the standard concepts of the domain and thus optimize and specialize the oered solution. Both for the programmer during development or modeling, than for the end user (who may not have a priori knowledge in computing) when using the solution.

Denition of DSLs

Several denitions of a DSL exist in the literature [START_REF] Fowler | Domain Specic Languages[END_REF] [62] [START_REF] Paulo | A systematic mapping study on domain-specic languages[END_REF] [80] [START_REF] Van Deursen | Domain-specic languages: An annotated bibliography[END_REF], depending on the application domain. In the technical domain for example we usually talk about domain specic programming languages, because they involve computer science experts and require programming competences. In software engineering or business domain, we talk rather about domain specic modeling languages, because they are user-centred and require domain competences only [START_REF] Latry | Approche langage au développement logiciel : Application au domaine des services de téléphonie sur ip[END_REF] [START_REF] Daniel | Prototyping domain-specic language semantics[END_REF]. Among the domains where we nd DSL, there are [START_REF] Van Deursen | Domain-specic languages: An annotated bibliography[END_REF]: drawing and 3D animation [START_REF] Elliott | An embedded modeling language approach to interactive 3d and multimedia animation[END_REF] [66], nancial products [START_REF] Arnold | An algebraic specication of a language for describing nancial products[END_REF], telecommunications and telephony [START_REF] Ladd | Two application languages in software production[END_REF] [72], protocols [START_REF] Chandra | Experience with a language for writing coherence protocols[END_REF], driver device [START_REF] Révéillère | Approche langage au développement de pilotes de périphérique robustes[END_REF], robotic [START_REF] Bjarnason | Applab: A laboratory for application languages[END_REF] [START_REF] Peterson | Lambda in motion: Controlling robots with haskell[END_REF],

and more recently the medical domain [START_REF] Menezes | Using archetypes and domain specic languages on development of ubiquitous applications to pervasive healthcare[END_REF] [84] [START_REF] Van Den Berg | A domain specic language for performance evaluation of medical imaging systems[END_REF]. This variety of the applications domains shows the increasing importance of DSLs in the software engineering landscape.

The development of a DSL in a domain is often argued by prots such as reliability, productivity and exibility [START_REF] Kieburtz | A software engineering experiment in software component generation[END_REF].

In the context of this work, we use DSL emphasizing more on the modeling language rather than the programming language. Because the solution that we oer is user-centred for the home care domain. Briey, the domain specic modeling language (DSML) is a particular type of the DSL that is user-centred, and allows to propose a solution using a high level of abstraction. The solution corresponds to directly model the concepts domain.

The DSML development enables users to fully engage in the proposed solution [START_REF] Mercadal | Processing domain-specic modeling languages: A case study in telephony services[END_REF] [START_REF] Latry | Approche langage au développement logiciel : Application au domaine des services de téléphonie sur ip[END_REF]. Thus, users do not have to worry about the code, because it's generated automatically from the model using specic DSM tools1 [START_REF] Tolvanen | Domain-specic modeling: How to start dening your own language[END_REF].

Main features of a DSL

Here we give the main advantages that prompted and still prompt today to development of the DSLs [START_REF] Van Deursen | Domain-specic languages: An annotated bibliography[END_REF]:

• Easier programming: DSLs are dened by a syntax that is similar to that used by the domain experts, which enables these (usually) non-programmers to be able to fully engage in the language programming. Among the advantage of this implication, we nd the reduction of the language learning eort by the domain expert and the ease of its understanding. In addition, DSLs unlike general-purpose programming languages are known to be concise, this is mainly due to the oered abstraction level. This features have the advantage to facilitate the developed programs analysis and thus to detect and correct errors earlier and quickly.

• Improved safety/quality: Unlike general-purpose programming languages, the use of DSLs enables automatic verication of a set of properties [START_REF] Thibault | Domain-specic languages: Conception, implementation and application[END_REF]. Thanks to the high level abstraction oered by the DSL, it is possible to use the traditional program analysis by reusing some verication tools [START_REF] Révéillère | Approche langage au développement de pilotes de périphérique robustes[END_REF]. These verications allow Chapter 2. State of the art to quickly detect problems in the veried application and thus increase productivity.

Moreover, focusing on specic domain enables both the optimization at compile time of the DSL as well as the development of specic tools such as, editors, debuggers, etc [START_REF] Latry | Approche langage au développement logiciel : Application au domaine des services de téléphonie sur ip[END_REF].

• Systematic reusing: Unlike general-purpose language that allows to abstract the common operations in libraries that are not always automatically reused, the DSLs are designed to lead to the systematic reuse. Indeed, DSL is characterized by a set of abstraction corresponding to concepts and knowledge domain. These abstractions are each of them associated with a code pattern that will be automatically generated and thus lead to the reuse of code at design time of the DSL. Besides, the code reuse in term of DSL also involves all the domain expertise that is captured during the design time of the DSL [START_REF] Révéillère | Approche langage au développement de pilotes de périphérique robustes[END_REF].

These features are introduced to ensure gains in productivity and quality in DSL-based approach [START_REF] Mernik | When and how to develop domain-specic languages[END_REF]. Hence, drawbacks associated with this approach are identied in the literature • The cost: Much eort should be given in the design and the implementation processes. It is also necessary to add cost of training and education for the endusers.

• Portability and Compatibility: Since DSL is designed for a particular domain, it lies in a non-standard and redundant language inducing hard problem in compatibility and portability.

Knowing the advantages and drawbacks facilitates the decision to dene the DSL.

Among the tools that are used to dene DSLs there is Meta-modeling tools. Metamodeling tools are development tools that allow to generate code from domain specic model [START_REF] Kahlaoui | Méthode pour la dénition des languages dédiés basée sur le métamodéle iso/iec24744[END_REF]. Example of the most often used tools: (1) Eclipse modeling project 30 Chapter 2. State of the art as an essential and major step in the domain identication approach. This concept has been dened for the rst time by Neighbors [START_REF] Milne | Software construction using components[END_REF] and was later revisited by McCain [START_REF] Mccain | Reusable software component construction -a product-oriented paradigm[END_REF],

Arango [START_REF] Arango | Domain analysis: From art form to engineering discipline[END_REF] and Pietro-Diaz [START_REF] Prieto-Díaz | Domain analysis: An introduction[END_REF].

The domain analysis consists in studying an application domain in a precise manner and determine its common information elements in order to reuse them systematically. This domain study is done in order to collect relevant information using dierent information sources, such as: interviews with domain experts, existing tools (systems), various documents (reports, manuals, etc. ). Besides the common characteristic of the domain, the domain analysis identies also the terminology, the key concepts of the domain and the various involved actors in the domain as well as their needs and objectives [START_REF] Czarnecki | Generative Programming: Methods, Tools, and Applications[END_REF] [START_REF] Thibault | Domain-specic languages: Conception, implementation and application[END_REF].

Even if in some cases the domain analysis allows to design a DSL, it remains insucient in general.

Program family analysis

Program family analysis corresponds to a complementary approach of the domain analysis. Indeed, domain analysis is interested only to the commonalities between domain element and not to particularities. In [START_REF] Parnas | On the design and development of program families[END_REF], a program family analysis is dened as follows: "We consider a set of programs to be a program family if they have so much in common that it pays to study their common aspects before looking at the aspects that dierentiate them". Thus, a program family in addition to being dened as a domain [START_REF] Milne | Software construction using components[END_REF], it also has the particularity to take into account specic properties of the domain elements [START_REF] Thibault | Domain-specic languages: Conception, implementation and application[END_REF].

Several methodologies exist to develop a program family. [START_REF] Parnas | On the design and development of program families[END_REF] provides for example a methodology to develop a program family based on the successive renement. Another newest work proposes an approach called FAST (Family-oriented Abstraction, Specication, and Translation) [START_REF] David | Family-oriented abstraction specication and translation : the fast process[END_REF] that allows to dene program families from identifying the domain terminology, commonalities among all members of the programs and variations.

The gathered information in the domain analysis and program family analysis are then used for the denition of the DSL. We will see in the following how this information are exploited to design a dedicated language.

Language denition DSL design or more precisely language denition corresponds to dene the syntax and semantic of the language.

Abstract syntax/Concrete syntax: Using the information gathered during the domain analysis and program family analysis phases, DSL designer should be able to dene the syntax of the dedicated language. there exist two types of syntax: (1) The abstract syntax, which corresponds to the vocabulary and grammar of the DSL. And (2) the concrete syntax, which corresponds rather to the specication of the notation of DSL elements [START_REF] Kahlaoui | Méthode pour la dénition des languages dédiés basée sur le métamodéle iso/iec24744[END_REF]. There are several notations for representing the DSL syntax, such as BNF (Backus-Naur Form), meta-modeling tools, etc.

Semantic: Once the syntax is dened it is necessary to dene the semantics of the language in order to give it a sense. There are two types of semantics: static semantic and dynamic semantic [START_REF] Peter | Formal semantics of programming languages: An overview[END_REF]. Static semantic is interested in the verication program or model before its execution (e.g., type verication, etc.). Dynamic semantic is rather interested in the program or model behavior during its execution.

Implementation

There are several implementations techniques of DSL. The choice of one technique depends mainly on the DSL type whether internal or external [START_REF] Fowler | Domain Specic Languages[END_REF]. Briey, an external DSL is an independent language develop from scratch and it's not based on any other language. An internal DSL is a language developed on the basis of an existing language called the host language. External DSL implementation requires the creation of tools and support such as: the interpreter and compiler [START_REF] Mernik | When and how to develop domain-specic languages[END_REF]. Internal DSL implementation requires the creation of a pre-processor [START_REF] Mernik | When and how to develop domain-specic languages[END_REF] or extension of the compiler or interpreter of the host language [START_REF] Ousterhout | Scripting: higher level programming for the 21st century[END_REF].

Using DSL in medical eld

Here, we cite two recent works concerning the use of a DSL-based approach in the medical eld.

In the context of Medical Imaging System, [START_REF] Van Den Berg | A domain specic language for performance evaluation of medical imaging systems[END_REF] propose iDSL, a domain specic language that enables performance evaluation of the medical imaging system. Authors denes the grammar of the iDSL language based on a set of concepts (process, resource, system, etc.) relative to the domain. And its semantic through an automatic transformation into MoDeST (Modeling and Description language for stochastic Timed Systems) model [START_REF] Bohnenkamp | Modest: A compositional modeling formalism for hard and softly timed systems[END_REF]. The transformation into MoDest enables automatic performance evaluation Chapter 2. State of the art for model checking and simulation. [START_REF] Hannes; Burwitz | Modeling clinical pathways -design and application of a domain-specic modeling language[END_REF] proposes an approach for modeling the Clinical pathway using domain specic modeling languages. Clinical pathway is dened as a plan that enables to describe a set of patients goals, and how to achieve them in an eciency manner [START_REF] Stanislao | Reducing clinical variations with clinical pathways: do pathways work?[END_REF]. Authors propose to develop the domain specic language considering some requirements such as, temporal dependencies and indenite order relations between treatments steps, etc. The modeling language was implemented using MetaCase-tool and was tested on the example of "Wisdom tooth treatment".

Discussion with respect to DSL

Studying and analyzing the DSL development steps allow us to position our work as follows: The domain analysis and program family analysis correspond to our requirement analysis. The language denition corresponds to the denition of the temporalities language expressed using a BNF notation (we will give more detail in the next chapter). For verication and monitoring purpose, we opted for another DSL implementation approach based on formalizing using timed automata.

With respect to related work in the medical eld, the approach proposed in [START_REF] Hannes; Burwitz | Modeling clinical pathways -design and application of a domain-specic modeling language[END_REF] is close to our work. The proposed DSL may be associated in our case to the home care plan.

However, authors have used the meta-modeling tools for implementing the DSL, which is not our case. In fact, as a part of this thesis, the DSL concepts allow us to describe the home care domain concepts through the UML class diagrams in collaboration with end-users, in order to dene temporalities specication language which can assist the coordinator during the elaboration of the home care plan. The language implementation is achieved using among others HCI framework (Vaadin 7 ).

Timed automata

Timed automata were introduced in [START_REF] Alur | A theory of timed automata[END_REF] as a nite state automata enriched with a clock variable. Figure 2.2 shows a sample example of timed automaton A which is composed of a set of states (e.g., s 0 and s 1 ), where s 0 the initial state and s 1 the accepting state (nal state), as well as transitions with labels over the alphabet Σ = {a, b} and a clock which is a continuous variable over the set of real-valued numbers R ≥0 . Initially, the 7 https://vaadin.com/home

t ≤ t s o s 1 a, t 0 a, t n t i a t 0 ≤ t 0 ≤ ... ≤ t n 6 6 6 D W E W ! W R ≥0 ∈ ∈ ≤ ≥ ∈ N φ v v → R ≥0 v(x) R X ≥0 ∈ R ≥0 v(x) ∈ ∈ ← v v (x) ∈ associates 0 value to clocks of r) and v (x)= v(x) if x ∈ X\ r.
Denition 2.2.1 (Timed automaton) is a tuple A = (S, S 0 , Σ, X, Inv, T, F ) where:

• S is a nite set of locations or states of the automaton;

• F ⊆ S is a set of nal states;

• S 0 ⊆ S is a set of initial states;

• Σ is a nite set of transition labels;

• X is a nite set of clocks;

• Inv: S → φ(X) associates an invariant to each state of the automaton;

• T ⊆ S × Σ × φ(X) × 2 X × S is a set of transitions. A transition (s, a, φ, λ, s )
represents an edge from location s to location s on symbol a. φ is a clock constraint, and the set λ ⊆ X gives the clocks to be reset after ring such a transition.

The set of timed words recognized by the automaton of Figure 2.2 constitutes the timed language noted L(A).

Semantic of timed automata

The semantics of timed automaton is dened as a transition system where each state of the automaton is represented by a pair (s, v) where s ∈ S and v is a valuation over X s.t.

v satises the invariant Inv(S). The semantic of a timed automaton is then expressed in terms of two types of transitions [START_REF] Alur | A theory of timed automata[END_REF]:

• Action transition: this type of transition can be triggered instantaneously if the current value of the guard is satised. Formally:

For a state (s, v)and a real-valued time increment d 0, (s, v) → d (s, v + d) if for all 0 d' d, v+ d' satises the invariant Inv(s).

• Time transition: this type of transition consists of staying in the same state and increasing the values of clocks respecting the invariant. Formally:

For a state (s, v) and a transition (s, a, φ, λ, s ) such that v satises φ, (s, v) → a (s , v[λ :=0]).

Resuming the timed automaton shown in Figure 2.2, a possible run of the automaton is:

(s 0 , 0) → 0.5 (s 0 , 0.5)→ 1 (s 0 , 1.5) → a (s 1 , 0) → 1 (s 1 , 1) → 3 (s 1 , 4) → b (s 0 , 0).

Timed automata 35

Properties of timed automata

We recall briey in this section some interesting properties on timed automata. Note that we use as a reference the original model proposed by Alur and Dill [START_REF] Alur | A theory of timed automata[END_REF]. Indeed, decidability and complexity results vary depending on the considered timed automata model [START_REF] Alur | A theory of timed automata[END_REF].

• Closure of timed automata Timed automata are closed under the union, projection and intersection however they are not closed under the complementation [START_REF] Alur | A theory of timed automata[END_REF]. The union and intersection closure of timed automata are based on a same closure as for untimed automata [START_REF] Hopcroft | Introduction to automata theory, languages, and computation, 2nd edition[END_REF].

The closure under projection8 is reduced to replace transitions with ε (empty word) on the not mapped alphabet. Concerning the non closure of the complementation, a detailed proof was presented in [START_REF] Alur | A theory of timed automata[END_REF] and a new proof can also be found in [START_REF] Alur | Decision problems for timed automata: A survey[END_REF].

• Language inclusion

The timed language inclusion problem consists, given two timed automata A and B in deciding whether or not L(A) ⊆ L(B). This problem has been shown undecidable since it can be reduced to A ∩ B=∅ and knowing that timed automata are not closed under complementation [START_REF] Alur | A theory of timed automata[END_REF].

• Langage equivalence

The timed language equivalence problem consists to check if L(A)= L(B). This problem has been shown undecidable since it can be reduced to L(A) ⊂ L(B) and L(B)⊂ L(A) [START_REF] Alur | A theory of timed automata[END_REF].

• Universality

The universality problem of timed automata consists to check, if a timed automaton A dened over an alphabet Σ, can recognize all possible timed words over Σ. In [START_REF] Alur | A theory of timed automata[END_REF] it is shown that this problem can be reduced to the inclusion problem, making the universality problem undecidable.

• Reachability and langage emptiness Chapter 2. State of the art

The rechability/emptiness problems are fundamental properties that make easy the verication of some systems behavior. Indeed, the emptiness problem consists to check if L(A)= ∅ and the reachability problem consist to determine if there is a run that allows to reach some identied states of the automaton. These problems are equivalent since, checking if the language L(A) is empty, consists to ask if there is an execution (run) that allows to reach a nal state (or some other states) from the initial state of the automaton. These problems have shown to be Pspace-complet and the detailed proof can be found in [START_REF] Alur | A theory of timed automata[END_REF][10].

These decision problems, especially the non closure under complementation, make dicult the use of timed automata to solve some verication problems. This situation has thus prompted the emergence of some variants and extensions of timed automata that allow to remedy to this problematic.

Variants of Timed automata

In order to solve the decision problems that are undecidable, several studies and researches have been realized on the model of Alur and Dill [START_REF] Alur | A theory of timed automata[END_REF]. We expose in the following some interesting classes and extensions of timed automata which will be useful in the context of this work.

Deterministic timed automata

A timed automaton is called deterministic if it satises the following conditions:

1. Only one start location;

2. Given two transitions from the same source and with the same alphabet, their clock constraints are disjoint. i.e., for all s ∈ S, for all a ∈ Σ, for every pair of transitions (s, a, φ 1 , λ, s ) and (s, a, φ 2 , λ, s ), the clock constraints φ 1 and φ 2 are mutually exclusive.

In [START_REF] Alur | A theory of timed automata[END_REF], it has been proved that the deterministic timed automata is closed under the complementation (can be complemented), thus languages inclusion is decidable. Deterministic timed automata are strictly less expressive than (non-deterministic) timed automata [START_REF] Alur | Decision problems for timed automata: A survey[END_REF]. The problem of the determinization of non-deterministic timed automata is undecidable [START_REF] Tripakis | Folk theorems on the determinization and minimization of timed automata[END_REF].

Event-clock automata

The class of Event-clock Automata has been dened in [START_REF] Alur | Event-clock automata: A determinizable class of timed automata[END_REF]. This model which englobes Event-recording automata and Event-predicting automata has been introduced to make decidable universal problem and the languages inclusion problem of timed automata. An

Event-recording automaton is a timed automaton containing, for each symbol a, a clock that records the time of the last occurrence of a. An Event-predicting automaton is timed automaton containing clocks which provide the time of the next occurrence of a symbol.

The problem of the determenization 9 of the event-recording automata is decidable.

Timed automata with silent transitions

Timed automata with silent transitions correspond to timed automata augmented with a non observable action-labeled transitions, also called ε-transitions. Among the properties of timed automata with ε-transitions is that they are more expressive than timed automata without ε-transitions, more specically when ε-transitions reset clocks, i.e., s → ε,g,{x} s [START_REF] Gastin | On the power of non observable actions in timed automata[END_REF][31] [START_REF] Gastin | Removing ε-transitions in timed automata[END_REF]. Several methods were proposed to remove ε-transitions when they do not reset clocks [21][46]. These methods are complex and can only be applied when ε-transitions do not reset clocks [START_REF] Gastin | On the power of non observable actions in timed automata[END_REF]. Timed automata with ε-transitions are not close under complementation [START_REF] Alur | A theory of timed automata[END_REF][21].

Timed automata with action duration

There exist a limited works that propose modeling action with duration using timed automata. Among the few existing models we found: Timed Automata With non Instantaneous Action Transition and Durational Action Timed Automata (DATA). Timed Automata With non Instantaneous Action Transitions was introduced for the rst time in [START_REF] De | Timed automata with non-instantaneous actions[END_REF] in order to specify the actions of systems which can take some time to be completed. Thus to model a non instantaneous actions in this type of model, each transition must be equipped with two kinds of constraints, initiation-constraint (to specify the beginning of the action) and completion-contraint (to specify the end of the action). It has been shown in [START_REF] Barbuti | Timed automata with non-instantaneous actions[END_REF][102] [START_REF] Tesei | Specication and verication using timed automata[END_REF] that Timed Automata With non Instantaneous Actions are more expressive than timed automata and less expressive than timed automata with εtransition. 9 To make deterministic a non-deterministic timed automaton It allows the system to control the action termination without forcing it to leave this state once action is executed (the system can stay there indenitely). It has shown in [START_REF] Kitouni | Article: Durational actions timed automata: Determinization and expressiveness[END_REF] that DATA is closed under all boolean operations.

Software tools

In order to support verication and analysis of the modeled systems using timed automata, several model checkers have been proposed. Among the best known, Kronos [START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF],

Hytech [START_REF] Wong-Toi | Hytech: The next generation[END_REF], and UPPAAL [START_REF] Behrmann | A tutorial on uppaal[END_REF]. We explain in what follows the general principle of model checking, and describe the model checker that we have chosen as a part of this work.

Model checking

Model checking consists in testing a model, i.e. if it satises or not some properties. reached or not; Safety properties which state that under some conditions, something bad will never happen in the system; And nally liveness properties which state that under some conditions, something Good will happen in the future [START_REF] Baier | Principles of Model Checking (Represe ntation and Mind Series)[END_REF].

There are several tools for model checking, among them, Kronos, Hytech and UP-PAAL. Kronos is a tool that allows to verify the timed automaton. Among works that use kronos [29][89]. Hytech is a tool that allows to verify an hybrid extension of the timed automata 10 and reachability and safety properties [57][112]. UPPAAL is a tool that allows to verify timed automata characterized by a set of clocks, set of channels for synchronisation automata, urgent actions, etc., and checks properties such as reachability, safety, liveness and deadlock [START_REF] Bouyer | Modéles et algorithmes pour la vérication des systémes temporisés[END_REF].

As a part of this thesis we will use the UPPAAL Model Checker that happens to be the most used in the timed system verication. Its main advantage over Kronos or Hytech is that it's easy to use thanks to its graphical user interface, in particular a simulation module that facilitates the testing phase and helps to faster detect eventual errors.

UPPAAL Model Checker

UPPAAL is a tool for modeling, simulating and verifying real time systems. UPPAAL uses an automaton extension. Among the elements of UPPAAL model:

(1) Start state: Each automaton is composed of a single start state represented by a double circle.

(2) Guards: Guards allow to express the conditions that must be satised on transitions. These conditions are timed conjunction constraints and constraints of integer variables.

(3) Reset operation: It corresponds to an initialization of the value of the clock. (4) Channels, synchronization and urgent : UPPAAL allows to verify a networks of timed automata, communication between automata is done through communication channels enabling a message exchange. Synchronization is the communication element between the automata. It enables the simultaneous crossing transitions between automata (e.g., (send) a! and (receive) a? corresponds to a normal synchronization between one transmitter and one receiver). UPPAAL allows to declare a channel as being urgent in order to prevent automata to linger in a state.

(5) Invariant : It corresponds to conditions associated with the states of the automaton, expressed as a constraint on the clock values.

UPPAAL tools

The UPPAAL graphical user interface (UPPAAL GUI) comprises three parts:

1. A modeling environment;

2. A simulation environment;

3. A verication environment.

Figure 2.4: UPPAAL: modeling environment

The UPPAAL editor as shown in Figure 2.4 allows to construct a set of automata, dene a tree automata, and congure and declare variables.

The UPPAAL simulator as shown in Figure 2.5 allows to simulate the execution of automata and to follow the execution evolution. Simulation with UPPAAL can be controlled by the user, in this case he may even choose by himself the transition to follow, or the simulation can be automatic. In this case the tool selects randomly transitions to follow.

The UPPAAL verier as shown in Figure 2.6 allows to perform the verication of some properties. For example, can the automata reach the state f from the initial state?

These properties must be written in a formal manner in order to be understood by the tool. The user can add or remove properties through this interface and at the end of the verication an answer is displayed to indicate whether or not the property is satised. UPPAAL uses a subset of (Timed Computational Tree Logic) TCTL logic [START_REF] Alur | Logics and models of real time: A survey[END_REF] to specify the properties to verify. Briey TCTL logic is a timed extension of the Computational Tree Logic (CTL) [START_REF] Clarke | Automatic verication of nitestate concurrent systems using temporal logic specications[END_REF]. TCTL was dened in [4], it corresponds to a logical tree which Chapter 2. State of the art is interpreted on timed transitions systems [31][108]. The TCTL formulas that are supported by UPPAAL [START_REF] Kim | A tutorial on uppaal[END_REF]:

• A[]ψ: For any execution, the property ψ is always veried;

• A <> ψ: For any execution, there is a state where ψ is veried;

• E[]ψ:

There exist an execution where ψ is always veried;

• E <> ψ: There exist an execution leading to a state where ψ is veried;

• ϕ ψ: Whenever ϕ is satised , then eventually ψ will be satised.

Timed automata in the medical eld

Several studies involving methods based on formal model exist in the literature. Up to our knowledge there are only few works which concern the medical domain. We review in what follows some of these works.

In the context of Ambient Assisted Living (AAL) [START_REF] Van Den | AALIANCE Ambient Assisted Living Roadmap[END_REF], [START_REF] Navarrete | Modeling a risk detection system for elderly's home-care with a network of timed automata[END_REF] proposes a model based on a network of timed automata (i.e., parallel composition of several timed automata) to tackle the problem of modeling a risk detection system for elderly's home care and allows to generate alarm if there is evidence of problem. The model enables to represent the patient's environment, characterized by a house equipped with a wireless sensor network in each room, each bed/armchair and a magnetic sensor at the entrance door, as well as patient's behavioral, and decides to generate an alarm if it detects some evidence of problem. The critical properties (e.g., reachability, safety and liveness) were veried using UPPAAL Model Checker.

[69] proposes a formal method based approach to the development of the Generic Patient Controlled Analgesic (GPCA) infusion pump. The objective was to develop methodologies that ease the safety property verication. Authors use the timed automata model to approach the problem of safety-assured development of the pump software.

Thus, they propose to transform manually the (GPCA) model expressed in Simulink 11and Stateow12 into a network of timed automata, which was then veried with respect to a set of generic safety properties.

[106] proposes a formal approach to model procedure of the medical treatment described in the Medical Guidelines (GLs) in the case of Imatinib (drog) dose adjustment protocol. Authors propose to formalize medical treatments described in GLs using extended timed automata with Task (TAT) [START_REF] Amnell | Code synthesis for timed automata[END_REF]. Briey TAT corresponds to timed automata where each state is associated with a piece of code. Semantic of TAT is the same as for TA extended with queue. The resulting formal model was veried using TIMES toolbox [START_REF] Mokrushin | Times: A tool for schedulability analysis and code generation of real-time systems[END_REF].

As part of Model Driving Design (MDD), [START_REF] Pajic | From verication to implementation: A model translation tool and a pacemaker case study[END_REF] proposes a model translation tool, which allows to convert automatically a verication model based on timed automata to a model which can be simulated and tested using Simulink/ Stateow. Knowing the strong needs of testing and verication of a medical device, authors propose to experiment their tool on an implementable cardiac pacemaker. They propose among others to model the pacemaker software using timed automata. Each timing cycle of the pacemaker was modeled using timed automata with a local clock. The model was then veried using UPPAAL and translated to be tested by Simulink. The experiment showed that the tool preserves the behavior of the pacemaker model from UPPAAL to Stateow.

Always using implementable cardiac medical devices, [START_REF] Mangharam | Cyber-physical modeling of implementable crdiac medical devices[END_REF] proposes a methodology for testing and verifying the proper functioning of a medical device within a closed loop of the patient 13 . To do so, they dene a real time Virtual Heart Model (VHM) to model the proper functioning and malfunctioning of the heart. The VHM was modeled using a network of timed automata which allows to capture the timing properties of the heart. As use case, a pacemaker device has also been modeled using a network of timed automata.

Tests and experimentation showed a clinically-relevant response.

Discussion with respect to timed automata

The study of some extension and subclasses of timed automata have allowed us to better understand what exists, in order to reuse or redene the model that is most suited to the constraints that we want to model in this thesis. In fact, as a part of this thesis, we opted for timed automata with εtransitions and invariants in the states. The dierent results of expressiveness [START_REF] Gastin | On the power of non observable actions in timed automata[END_REF][31] [START_REF] Gastin | Removing ε-transitions in timed automata[END_REF] have strengthened our choice.

Given a non-atomicity of activity that we will handle, it was necessary to make an overview of what is being done in the modeling of activity with duration using timed au-Chapter 2. State of the art tomata. The two works above, both enable to represent the activity with duration, nevertheless they fail to respond to our expectations as they are represented. Indeed, Timed Automata With non Instantaneous Action Transitions make heavier the constraints on transitions and modies the timed language acceptance by breaking this latter into initiation and completion language acceptance. Add to this the fact that it's less expressive than timed automata with εtransitions.

Regarding DATA, they can control the duration of an activity. However, if two activities (or more) follow each other, there is no way to control the time that elapses between these two activities. This feature is completely excluded in our case, since, we must not only control the duration of the executed activity, but also control the time interval between activities. Add to this, the two Timed automata models with non Instantaneous Action Transitions and DATA can not be used directly in the existing verication tools but they must be transformed rst.

From this nding, we propose in the next chapter a formal model which will allow us, among others, to control the execution time of activities to respect the time interval between activities, and which can be directly used by verication tools such as UPPAAL [START_REF] Behrmann | A tutorial on uppaal[END_REF].

Concerning the related work, all described works use the timed automata formalism in the medical eld. But while some of them simply reuse the timed automata as it is dened in Alur and Dill, others propose extension (e.g., TAT) to better adapt to their case studies. However any of these works have been interested in modeling semi-structured systems, none has taken into account the duration of the activity and also, except for the verication (e.g., reachability, safety), monitoring was not mentioned in these works.

Conclusion of Chapter 2

In this chapter we introduced the paradigms of domain specic languages. We have presented its various benets and the design steps necessary to its denition. Then we exposed the formalism of timed automata on which this thesis is based. In the last part of this chapter, we mentioned the few works that use timed automata in the medical eld. These works ignore several aspects of modeling such as the activity duration and the monitoring. In the next chapter, we will present the considered formal model which is based on timed automata formalism. We try through this formalism to take into account properties which we consider absent in other works.

Chapter 3

Modeling and analyzing home care plan using timed automata Contents 3.1 A DSL-based approach for specifying home care plans . . . . . . )RUPDO 0RGHO

( [ W U D F W W K H F D U H S O D Q L Q I R U P D W L R Q QJ 3 U R Y L G H W K H F D U H S O D Q D X W R P D W D
• Patient: it is important to have the main features of the patient involved in the home care plan elaboration, such as: personal information (last name, rst name, phone number. etc.), physical characteristics (weight to take into account eventual weight overload), comments (wish of the patient about the actor type, etc.). The input of this information is provided by the coordinator.

• Home health care: includes everything about medical prescription, the health care type, the therapeutic project, etc.

• Care plan activity: an activity denotes a medical or social service provided to Period species the time period during which the activity is dened; Days indicates the days within a period in which an activity must take place; Time ranges indicates the time slots in which the activity can occur; Duration species theoretical duration which corresponds to the average of already observed durations.

• Intervention: an intervention is a collection of activities that can be scheduled together. Interventions are dened by grouping together activities that can be performed by a same actor type and which occur in the same time range. Interventions may be specied manually by the coordinator or computed automatically from the specications of the activities and then proposed to the coordinator for validation.

Besides the aforementioned concepts, the proposed DSL is enriched with additional constraints derived from the domain knowledge (e.g., medical knowledge represented in ontologies, etc).

3.1.

A DSL-based approach for specifying home care plans 49

User centred specication of home care plan

Each activity of the care plan is associated with a set of elementary temporal specications. These specications provide the information about the time when the activity should be performed, expressed as a quadruplet (Days, Time ranges, Period, Duration), and allow us to provide a language that can express regular or irregular repetitions of an activity in some period under a condensed form, similar to that used by doctors (e.g.

Everyday morning and evening).

Thus, the elaboration of the home care plan is mainly based on the specication of the time which characterizes activities. In order to make the specication of the time much easier to the coordinator, we propose a temporal specication language which better capture the most often used temporal expressions.

Indeed, the conducted analysis in the home care area led us to suggest a temporal specication language with a high level of abstraction based on three forms of elementary specications [START_REF] Bouet | A general model for specifying near periodic recurrent activities -application to home care activities[END_REF]. Each instance of the quadruplet (Days, Time ranges, Period, Duration) corresponds to an elementary specication.

For the formal denition of the temporal expression, we use a BNF notation. Briey, an element inside embraces associated with one of the following symbols ? * + means respectively that the element may be present or absent, that it is present an indenite number of times and that it is present at least once.

Temporal expression

We dene below each element of the temporal specication, i.e., Period, Days, Time ranges. Knowing that Duration corresponds to the time duration of home care plan activity.

• Period 1. <period> ::= <starting-date> "-"<ending-date>? Combination of elementary specications allows to express specications of irregularities and exceptions. In fact, to avoid ambiguity, when a same day occurs in dierent elementary temporal specications, the coordinator must use exceptions. An exception is introduced via the keyword except.

Table 3.1 shows a simple example of a specication using this language. Each row of the table corresponds to an elementary temporal specication. The rst two for the activity Toilet and the last two for the activity Dress. The case of the activity Dress shows an example where an exception is needed. In fact, we have an exception on 04/20/13, since on 04/20/13 the activity takes place only in the morning. The general form of a Day3... are days to exclude from E1 (we call them "exception Days").

Roughly speaking, the notion of a legal schedule of a care plan activity is dened as a sequence of allowed instances of this activity which satises the set of temporal specications. An example of a legal schedule for the activity Toilet of Table 3.1 corresponds to the sequence: Toilet at 09h00 on 01/01/13; Toilet at 18h on 01/01/13; ...; Toilet at 10h00 on 03/31/13.

The proposal of temporality language has led to the development of a GUI to support a coordinator in designing a home care plan. We will present in the next chapter this GUI.

General modeling process with timed automata

From the graphical user interface, the coordinator can specify the home care plan which consists on dierent activities associated with their temporal specications. Recall that our main objective is to build the care plan timed automata. To achieve this objective, we propose a three steps approach (Figure 3.3): (Step 1) Pattern automata construction, which consists in mapping between elementary temporal specications and timed automata called Pattern automata, (Step 2) Activity automata construction, which consists in combining patterns automata to build the activity automata using our composition algorithm, and (Step 3) Home care plan automata construction, which consists in constructing the global care plan automata.

This modular approach allows an incremental denition of a home care plan (which may be complex or not) by progressively aggregating, at rst time, Pattern automata, and at the second time, Activities automata.

Among the advantages of this approach, is to facilitate the reuse of some components, in particularPatterns automata which makes the construction of the care plan more easier than if it is built directly from the specied temporal specications, as well as to facilitate

A formal model based on timed automata with duration

The formalism of timed automata is used to model home care plans. As already said, several variants of timed automata have been proposed in the literature. We consider in our work timed automata with ε-transitions (i.e., silent transitions) and invariants (i.e., guards on the states). The activities of care plan are not instantaneous but have a duration. This is why we need to capture the notion of duration of an activity in our timed automaton. This is achieved through the identication of the notion of execution states of an activity automaton. More precisely, we distinguish between three kinds of states in a given activity automaton: the start states where the automaton stays before the activity starts, the execution states where the activity is executed, and the waiting states where the automaton indicates that the activity has been terminated. Note that to achieve this goal, we slightly modied the denition of timed automata to introduce this set of states namely: waiting states (denoted W), execution states (denoted E) and start states (denoted St). It is worth noting that this set is used to construct "pattern automata" and by the composition operator to generate the activity automata and the care plan automata. The proposed modication doesn't impact the semantics of the generated automaton and hence standard tools, such as UPPAAL can still be used to handle the verication task. A formal denition of the extended timed automaton is given below: Denition 3.2.1 (timed automata (with an implicit duration))

Let A = (S, s 0 , Σ, X, Inv, T, F, W, E, St) be timed automaton where:

• S is a nite set of locations or states of the automaton with s 0 the initial state, F ⊆ S is the set of nal states, W ⊆ S is the set of waiting states, E ⊆ S is the set of execution states, and St ⊆ S is the set of start states;

• Σ is a nite set of transition labels including {ε};

• X is a nite set of clocks. W.l.o.g., we assume that the time unit is in minute, because there is no precision beyond the minutes in the home care plans;

• Inv: S → φ(X) associates an invariant to each state of the automaton;

• T ⊆ S × Σ × φ(X) × 2 X × S is a set of transitions. A transition (s, a, φ, λ, s )
represents an edge from location s to location s on symbol a. φ is a clock constraint, and the set λ ⊆ X gives the clocks to be reset after ring such a transition.

A A d s 0 ∈ St A s 1 ∈ E d A s 2 ∈ W {x d , x t } A x d x d <= 720 d Toilet x t x t == 0 A Σ t 0 ≤ ... ≤ t n

Relative days pattern

Relative days pattern is used to express a regular repetition of the activity of the care plan. For each row of temporality expressed as (Relative days, Time ranges, Period, Duration) dened for an activity a of the care plan, the corresponding timed automaton pattern A RD = (S, s 0 , Σ, X, Inv, T, F, W, E, St) is dened as follows :

• S is a nite set of states, with s 0 the initial state. The total number of states is:

N bStates = 3+(N bT imeRanges -1) * 2 * NbDays+ NbDays.
Where N bT imeRanges is the number of times ranges and NbDays is the number of specied Days;

• F is the set of nal states. We always have one nal state;

• Σ = {Activity name} ∪ {ε} is the set of transition labels, where ε denes the silent transition;

• X = {x d , x t , x p , x w } is the set of clocks, where x d is used to control the execution of the activity within a day, x t is used to control the activity duration, x w is used to control the execution of the activity in a day of the week and x p is used to control the execution of the activity in a day of the period. W.l.o.g., we assume that the time unit is the minute; another one is to reset x w in order to move to the next week in the period) and the transition to the nal state. φ is a clock constraint.

• Inv ={∀s ∈ S, Inv(s) = (x d ≤ EndT imerange -d) and s ∈ St, Inv(s) = (x d ≤ 24h) and s ∈ W, Inv(s) = (x t ≤ d) and s ∈ E}; • T ⊆ S × Σ ∪ {ε} × φ(X) × 2 X × S
The timed language accepted by the automaton A RD is the set of timed words asso- ciated with accepting runs. It is formulated as follows:

L(A RD ) = {w/w = ((end(P )-start(P ))/(7 * 24h))-1 k=0 ( m-1 i=0 ( n-1 j=0 (a, t j i,k ))), t j i,k ∈ [d i + k * 24h * 7 + start(P ) + start(I j ), d i + k * 24h * 7 + start(P ) + end(I j )]}. L(A RD ) t j i,k ∈ ∈ ∈ I j I j d i L(A RD )
• {s 0 , s 1 , s 2 , s 3 , s 4 } s 0 Toilet W = {s 3 } E = {s 1 , s 2 } 3.2.
General modeling process with timed automata 57

• F = {s 4 }; • Σ = {Toilet} ∪ {ε}; • X= {x d , x t , x p , x w };
• T is the set of transitions where:

Transitions

Absolute dates pattern

Absolute dates are used to dene precise dates for an activity of the care plan, e.g.

12/12/2013, 12/14/2013, etc. For each elementary temporal specication expressed as (Absolute dates, Time ranges, Period, Duration) dened for an activity a of the care plan, the corresponding timed automata A AD = (S, s 0 , Σ, X, Inv, T, F, W, E, St) is dened as follows :

• S is a nite set of states, with s 0 the initial state. The total number of states is:

N bStates = N bDates + 3+ (N bT imeRanges -1) * 2 * N bDates.
Where N bT imeRanges is the number of times ranges and N bDates is the number of specied dates;

• F is the set of nal states. We always have one nal state;

• Σ = {Activity name} ∪ {ε} is the set of transition labels; The timed language accepted by the automata A AD is the set of timed words associated with accepting runs. It can be formulated as follows: Transitions [START_REF] Alur | Model-checking for real-time systems[END_REF]4,[START_REF] Alur | A really temporal logic[END_REF] are triggered when x p is outside the specied dates. Tran- sition [START_REF] Alur | Model-checking for real-time systems[END_REF] represents the interval between the beginning of the period and the rst specic date. Transition (4) represents the interval between the two specic dates. Transition [START_REF] Alur | A really temporal logic[END_REF] represents the interval between the last specic date and the end date of the period. For those transitions the automata can move from s 0 to s 4 at any moment where (x d ≥ 0 && x d < 690), the guard is composed of a single condition on the clock x p , it ensures the validity of the interval where the activity should not be done.

• X ={ x d , x t , x p }
L(A AD ) = {w/w = m-1 i=0 ( n-1 j=0 (a, t j i )), t j i ∈ [D i + start(I j ), D i + end(I j )]}. L(A AD ) t j i ∈ ∈ I j I j D i L(A AD ) absolute dates pattern Toilet Toilet A AD (S, s 0 , Σ, X, Inv, T, F, W, E, St) Absolute dates • s 0 s 1 s 2 s 3 s 4 s 5 s 0 s 4 s 1 s 2 s 3 • F s 5 • Σ = {T oilet} ∪ {ε}
Transition [START_REF] Alur | Decision problems for timed automata: A survey[END_REF] enables the automaton to move back from s 4 to s 0 , without performing any activity, at the end of the day (i.e., when x d equals 1440) within the specied period (i.e., x p < 525600). Upon this transition, the variable x d is reset to record the beginning of a new day.

Transition [START_REF] Amnell | Code synthesis for timed automata[END_REF] is red at the end of the period (i.e., when x p equals 525600)

and enables the automaton to move to the nal state s 5 and terminate the execution.

For example the timed word = (Toilet, 1920).(Toilet, 4800).(Toilet, 6240) is an execution which is accepted by the automaton of Figure 3.6

Relative days

Toilet Transition ( 4) is red at the end of the period (i.e., when x p equals 525600)

Toilet A ED S s 0 Σ X Inv T F W E St Everyday • S s 0 N bStates N bT imeRanges * 2 + 2 NbT imeRanges s 2 s 1 • F s 3 • Σ = {T oilet} ∪ {ε} • X x d x t x p
and enables the automaton to move to the nal state s 3 and terminate the execution.

The timed language accepted by the automata A ED is the set of timed words associated with accepting runs. It can be formulated as follows:

L(A ED ) = {w/w = ((end(P )-start(P ))/24h)-1 i=0

( n-1 j=0 (a, t j i )), t j i ∈ [i * 24h + start(P ) + start(I j ), i * 24h + start(P ) + end(I j )]}.

This timed language L(A ED ) consists in concatenating successively the timed word (a, t j i ) according to two parameters: the existing time ranges in a day j ∈ [0,n-1] and the day i ∈ [0,((end(P)-start(P))/24h)-1]. Period is dened by start(P) and end(P), Time ranges by start(I j ) and end(I j ).

Hence, L(A ED ) corresponds to all the schedules of a given activity which satisfy the corresponding Everyday constraint.

Activities Automata

Now that we have seen how to build the "Elementary temporal specication timed automata" using temporal specication patterns, we will see here how to construct an activity automaton. As said previously, care plan activity is characterized by a set of temporal specications. In order to build activity automaton we have to combine its associated patterns automata. For this purpose, we dene a specic composition operator noted " ". This operator mixes the asynchronous product (or shue) on some states and a specic synchronisation product on other states (waiting states) in addition to blocking actions (in the execution states). Blocking is used to prevent the interleaving of activities. Indeed, since the activities are not instantaneous (i.e., they have duration), the composition operator must ensure that at a specic instant of time t, there is only one activity being executed (i.e., only one activity automaton is in an execution state).

Synchronous is needed when the activity automaton is at waiting states in order to synchronize the reset of the day and week clocks (respectively, the variables x d and x w ). A formal denition of the proposed composition operator is given below.

Denition 3.2.2 (Composition of timed automata) Let

A 1 = (S 1 , s 1 0 , Σ 1 , X 1 , Inv 1 , T 1 , F 1 , W 1 , E 1 , St 1 ) and A 2 = (S 2 , s 2 0 , Σ 2 , X 2 , Inv 2 , T 2 , F 2 , W 2 , E 2 , St 2 ) be two timed automata. The composition of A 1 and A 2 , denoted A 1 A 2 , is the timed automaton (S 1 × S 2 , s 0 1 × s 0 2 , Σ 1 ∪ Σ 2 , X 1 ∪ X 2 , Inv, T, F 1 × F 2 , W, E, St), where Inv (S 1 , S 2 ) = Inv (S 1 ) ∧ Inv (S 2
) and the set of transitions T is the union of the following sets:

1. {((s 1 , s 2 ), ε, φ, λ, (s 1 , s 2 )) : (s 1 , ε, φ 1 ,λ 1 ,s 1 )∈ T 1 and (s 2 ,ε,φ 2 , λ 2 ,s 2 ) ∈ T 2 , s 1 and s 2 are both waiting states and λ = λ 1 ∪ λ 2 , φ = φ 1 ∧ φ 2 }. The sets W, E and St are dened as follows:

{((s

• W={(s 1 , s 2 ) ∈ S 1 × S 2 : s 1 ∈ W 1 and s 2 ∈ W 2 }. • St={(s 1 , s 2 ) ∈ S 1 × S 2 : (s 1 ∈ St 1 and s 2 ∈ St 2 ) or (s 1 ∈ St 1 and s 2 ∈ W 2 ) or (s 1 ∈ W 1 and s 2 ∈ St 2 ) }. • E={(s 1 , s 2 ) ∈ S 1 ×S 2 : (s 1 ∈ W 1 ∪St 1 and s 2 ∈ E 2 ) or (s 1 ∈ E 1 and s 2 ∈ W 2 ∪St 2 )}. Σ i i = 1, ..n Σ 1 = Σ 2 = Σ 3 = ... Toilet A r1 A r2 A r1
Toilet Monday Thursday morning

A r1 A r2
Toilet Sunday evening We discuss below how to use the proposed framework to verify and monitor the home care plans using UPPAAL Model Checker.

A r2 A r1 A r2 Toilet Σ i i = 1, ..n Σ 1 = Σ 2 = Σ 3 = ...

Realizability of home care plans

It is important to check the realizability of a home care plan, i.e., to check whether or not the activities included in the home plan can be eectively scheduled and performed according to the constraints specied in the plan. In other words, a home care plan is realizable when each activity can be performed without interruption in the imposed time range in any specied period. Checking realizability of a home care plan can be reduced to the emptiness problem of the corresponding timed automaton. In fact, the emptiness problem for a timed automaton A consists in verifying whether or not L(A) is empty. A standard way to achieve such a test is to check reachability of the nal state from the initial state.

Consider again the timed automaton shown in Figure 3.12. We check in the following if the nal state (s 3 , s 3 ) is reachable from the initial state (s 0 , s 0 ). The emptiness checking is performed using the following query1 : E <>(Process.FinalStateName).

Figure 3.13 shows the emptiness checking of the home care plan timed automaton of Figure 3.12 using UPPAAL. The status box shows the query result (satised or not). In our example, the query is satised, which means that the home care plan is realizable.

Monitoring of home care plans

Note that most of the activities of a home care plan are manual, i.e., performed manually by professionals. In current state of aairs, the activities that have been performed are often recorded manually on paper. Our goal is to enable electronic recording of executed activities in order to keep track of the execution of home care plans. Such information can then be used to monitor home care plans. For example, compliance of execution traces w.r.t. a home care plan may be checked by reducing this problem to the membership problem in the timed automata framework. Also, the monitoring system may be used to detect executions that deviate from the specication. For example, if in the scheduled home care plan the activity Injection is provided at 09h00 and takes 30 minutes, and after execution we nd out that it was in fact done at 10h00, it is important to be able to detect this type of deviation. Below an example of query: This query checks that the activity Injection which was done on January 2 between 11h00 and 12Hh00 is well complying with a scheduled home care plan timed automaton of Figure 3.12. In other words, is there an execution which satises this activity ? The answer is property not satisfied since Injection was scheduled starting from 9h00. More generally, a monitoring system can be enhanced with rules that enable to trigger alerts when particular deviations are detected.

Grouping activities into interventions

Grouping together activities that can be performed by a same type of actor (nurse, nurse auxiliary, etc.) and which occur in the same time range is called Intervention. Interventions may be specied manually by the coordinator or computed automatically from the specications of activities and then proposed to the coordinator for validation. The concept of intervention is really important in the sense that it allows to reduce the waiting time between activities in order to avoid multiple movings at the patient's home. The analysis of activities to specify interventions is a complex task since it requires to ensure com- A Int = (S, s 0 , Σ, X, Inv, T, F, W, E, St, Int) is dened as follows:

• S = {s 0 , s 1 , s 2 , s 3 , s 4 } with s 0 the initial state; The graphical user interface that allows to assist the coordinator for editing home care plans, (ii) The temporality automata generator that enables to generate temporality automata of each activity from extracting information about the temporal specications in the database, (iii) The care plan timed automata generator which consists on constructing the home care plan timed automata using the result of (ii), this construction is an implementation of our composition algorithm, and (iv) The interventions generator which consists in grouping together activities that can be performed in a same time range and by a same type of actor. These four components have been implemented using JavaTM platform version 8, Netbeans 1 framework and Vaadin 2 framework. Here, we describe the technical details of the prototype implementation and present some tests on real home care plans.

• W = {s 3 }; • E = {s 1 } • St = {s 0 } • Int = {s 2 } • F = {s 4 } • Σ = {Toilet, Intervention} ∪ {ε} • X = {x d , x t , x p , x i } x i • T intervention state • {((s 1 , s 2 ), a, φ, λ, (s 1 , s 2 )) s 1 φ λ s 1 ∈ T 1 s 2 s 2 s 2 ∈ W ∪ E ∪ St s 1 ∈ Int s 2 φ λ s 2 ∈ T 2 s 1 s 1 s 1 ∈ W ∪ E ∪ St s 2 ∈ Int } Int • (s 1 , s 2 ) ∈ S 1 × S 2 s 1 ∈ Int s 2 ∈ Int s 1 ∈ Int s 2 ∈

Overview of the prototype

Before going into the details of the prototype architecture and implementation, it is necessary to have the intuition and the general view of the prototype functioning. of allowed labels. Actor type for each activity and duration are initialized by the system by default (we associate for each activity a nominal duration and an actor type), but the coordinator has the possibility to change their values. He may even impose a name of actor (when the coordinator wants to assign an actor with specic skills).

We see for example in The value of the period is by default the same as that of the home care plan. The main actor type is associated with each activity (this is the type of actor who is responsible for the activity). The activity ID in the rst column (A1, A2, ...) is attributed by the system. It is specic to each entry. Indeed, expressing activities temporalities is essential to specify their repetitiveness. We can see for example in Figure 4.6 several elds to be completed: Date (which refers to a calendar), Time ranges (which refer to times of the day, time slots or xed times), the Period and the Principal actor type. However, activities repetitiveness is not always fully regular but there may be exceptions. The button "except public holidays" allows to insert exceptions. We will see in more details in section 4.3 a real example of the care plan verication and how the answers are displayed to the coordinator through the graphical user interface.

Interventions generator

Interventions generator enables to provide to the coordinator a complete list of interventions to be performed by actors, day after day, during all the period of the home 4. Before building the interventions list to be provided to the coordinator, dierent requirements must be taken into account, which are:

• The idle time between the activities of the home care plan;

• The non-interleaving interventions;

• The selection of actor type who intervenes in each intervention;

• The time range of each intervention.

• actor type is designed to execute the corresponding activities.

Monitoring

Another important step supported by our prototype is the monitoring. Once the care plan validated and the activities performed at patient's home, the coordinator can check the consistency between scheduled activities and those executed. This verication is done with respect to certain criteria such as: Has the activity X been given? Has the activity time range been well respected? The developed prototype can answer such questions using UPPAAL Model Checker and following the two steps below:

1. Once the care plan executed, the system retrieves the log le. The log le contains the execution trace of the care plan by the actor (at patient's home). It describes each executed activity with its time range (start time and end time).

2. Using TCTL requests, the system queries the care plan timed automaton (elaborated home care plan) to report anomalies. As mentioned before, this procedure involves the membership question, which consists on taking the care plan timed automaton, and some information about the executed care plan from the log le, and determine if there is an execution of the care plan automaton which satises the tested information.

Test and experimentation

We now show how the prototype can be used to facilitate the analysis and interventions generation of home care plans. In fact, our prototype will assist the coordinator in checking the care plan by validating it, if there is non error, or by identifying the problem if it exists. It will also assist the coordinator for generating interventions which are an important step for the planning.

To better understand and see concretely the prototype functioning, we propose in what follows treating a real example of care plan of an anonymous patient (for condentiality reasons). We will test dierent analysis and verication steps (realizability, interventions generation and monitoring) that we have identied previously.

Realizability test

Testing realizability of the home care plan consists in testing whether or not each activity can be performed without interruption in the determined time ranges throughout the

Monitoring test

We dened monitoring as a way to detect executions that deviate from the specications.

We illustrate in this part the same example as the one we saw in 4. We described in this chapter the prototype which allows to generate the care plan timed automata from the input of temporal specications dened for a set of activities using the GUI. The resulting care plan automata were veried using the UPPAAL Model Checker through XML les and TCTL queries. We exposed the technical details of the prototype implementation which we exploited in order to conduct tests and experiments. In fact, we tested the prototype using real home care plans. These tests allowed us to assess eciency of the prototype regarding the realizability, interventions generation and monitoring. In our experiments, we have found out that the application works well for the tested home care plans.

Conclusion

We investigated in this thesis the issues related to the design and analysis of the home care plan. Home care plans are inherently unstructured processes. This is due to the specicity of each patient, i.e., a specic care plan is required for each specic patient, as well as to the irregularity of repetitive activities within a plan. Nevertheless, we showed that using appropriate temporal expressions, it is possible to specify the schedule of such activities. In fact, we describe in this thesis a detailed presentation of the approach to construct temporal specication of the home care plan using a DSL. The obtained specication plays the role of a process model that must be enacted by a business process management or a workow system. In order to formally describe the home care plans constructed using the proposed DSL, we rested on a formal framework based on timed automata. Our proposal includes an approach to generate a formal specication of the home care plan, expressed as timed automata. We propose a three steps approach which consists in (i) the identication of the elementary patterns that are useful to specify the home care plans,(ii) the proposition of a specic composition algorithm that enables to combine patterns automata to build the activity automata, and then (iii) the construction of the global care plan automaton. The resulting care plan automaton encompasses all the possible allowed schedules of activities for a given patient. Once the care plan automaton is constructed, we can benet from model checkers to make dierent analysis in a declarative way. We have illustrated realizability verication, monitoring of a care plan and grouping of activities into interventions using UPPAAL Model Checker.

Our specication language can easily be extended in order to increase its expressivity and its usability. Extensions are performed by introducing other patterns for dening elementary temporal expressions. For example, patterns such as "n times per day or per week" would be useful in a medical context. For preserving our modeling, it is necessary to ensure that each of these supplementary patterns can be transformed into timed automata.

The elaboration of a home care plan is an instance of the MTSPTW (Multiple Traveling Salesman Problem With Time Windows) with a time windows constraint for each activity and the optimization of interventions. In this type of problem, precedence constraints between tasks are very often considered. Introducing such constraints between activities into a care plan is sometimes necessary (for example, an injection of Lovenox 96 Conclusion must be followed by a blood control before 15 days). Since it is possible to model precedence constraints with automata, we envisage an extension of our specication language to express this kind of constraint and to adapt our modeling into timed automata.

The interest of timed automata to model and solve planning and scheduling problems has been addressed in previous works [START_REF] Male | Job-shop scheduling using timed automata?[END_REF] [START_REF] Panek | Scheduling and planning with timed automata[END_REF]. Planning determines the possible plans while scheduling assigns resources to activities in order to respect the various constraints.

Our approach deals only with planning preparation through the generation of interventions. An interesting issue will be to study how our care plan automata can be used to facilitate scheduling. For example, it has been shown [START_REF] Male | Job-shop scheduling using timed automata?[END_REF] that optimal schedules correspond to shortest paths in timed automata. In our context, such an approach can be bind to optimal rounds after introducing distances between patients' homes. Extension of timed automata into priced timed automata [START_REF] Subramani | Resource-optimal scheduling using priced timed automata[END_REF] can also be worthwhile to consider since it permits to assign costs to activities. It is important to note that, when assigning resources to interventions, availability of human actors can be expressed with our temporal expressions.

In all these works for modeling planning and scheduling problems by automata, the specication of the problem is generally made by experts directly with the automata formalism. It would be necessary that end users can specify directly the main constraints of the problem. We think that our specication language can be enriched to oer such a possibility.

1. 1

 1 Age group in France at January 1st 2013 and January 1st 2015. source: INSEE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 Use cases of the Plas'O'Soins platform . . . . . . . . . . . . . . . . . . . 1.3 Main processes of home care (adapted from [51]) . . . . . . . . . . . . . . 1.4 Processes managed by Plas'O'Soins platform . . . . . . . . . . . . . . . . 1.5 Example of home care plan . . . . . . . . . . . . . . . . . . . . . . . . . . 1.6 Process for the creation and the management of the home care plan . . . 2.1 Design process of a DSL (adapted from [72]) . . . . . . . . . . . . . . . 2.2 Timed automaton . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.3 Principle of model checking . . . . . . . . . . . . . . . . . . . . . . . . . 2.4 UPPAAL: modeling environment . . . . . . . . . . . . . . . . . . . . . . 2.5 UPPAAL: simulation environment . . . . . . . . . . . . . . . . . . . . . . 2.6 UPPAAL: verication environment . . . . . . . . . . . . . . . . . . . . .

3. 1

 1 Underlying processes to the elaboration of the home care plan . . . . . . 3.2 UML class diagram for a home care plan (partial) . . . . . . . . . . . . . 3.3 The three steps approach . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.4 Example of a part of timed automaton for a task A . . . . . . . . . . . . 3.5 Example of a timed automaton in case of relative days (here Thursday except(05/01/14)) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.6 Example of a timed automaton in case of Absolute dates . . . . . . . . . . 3.7 Example of a timed automaton in case of Everyday . . . . . . . . . . . . 3.8 Timed automaton A r1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.9 Timed automaton A r2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.10 Activity (Toilet) timed automaton. . . . . . . . . . . . . . . . . . . . . . 3.11 Toilet and Injection automata. . . . . . . . . . . . . . . . . . . . . . . . . . 3.12 Home care plan timed automaton . . . . . . . . . . . . . . . . . . . . . . 3.13 Emptiness checking timed automata with UPPAAL. . . . . . . . . . . . . 3.14 Toilet automaton with interventions. . . . . . . . . . . . . . . . . . . . . 3.15 Example of interventions automaton. . . . . . . . . . . . . . . . . . . . . List of Tables 3.1 Specication of activities Toilet and Dress . . . . . . . . . . . . . . . . . . 3.2 Specication of activity Toilet . . . . . . . . . . . . . . . . . . . . . . . . 3.3 Specication of activity Toilet: Absolute dates pattern . . . . . . . . . . . 3.4 Specication of activity Toilet: Everyday pattern . . . . . . . . . . . . . . 3.5 Elementary temporal specications . . . . . . . . . . . . . . . . . . . . . 3.6 Example of home care plan . . . . . . . . . . . . . . . . . . . . . . . . . . 3.7 Example of home care plan . . . . . . . . . . . . . . . . . . . . . . . . . .

Contents 1 . 1

 11 Home care area . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.1.1 Home care in France . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.1.2 Home care processes . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.1.3 Home care challenges . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.1.4 Overview on main software tools . . . . . . . . . . . . . . . . . . . . 1.2 Plas'O'Soins Project . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2.1 Our contribution within Plas'O'Soins project . . . . . . . . . . . . . 1.3 Requirement analysis . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3.1 Involved actors in home care plan . . . . . . . . . . . . . . . . . . . . 1.3.2 Home care plan activities . . . . . . . . . . . . . . . . . . . . . . . . 1.3.3 Example of a home care plan . . . . . . . . . . . . . . . . . . . . . . 1.3.4 Problems related to the design and monitoring of the home care plan 1.4 Objective of the thesis . . . . . . . . . . . . . . . . . . . . . . . . . 1.5 Conclusion of Chapter 1 . . . . . . . . . . . . . . . . . . . . . . . .

1. 1 .

 1 Home care area 11 1.1.1.3 Home care services

Figure 1 .

 1 Figure 1.2 illustrates the actors types (roles) involved in the Plas'O'Soins project with their dierent goals.

4 .

 4 Objective of the thesis 23 capturing in advance the home care plans of all the patients.

Contents 2 . 1

 21 Domain specic language . . . . . . . . . . . . . . . . . . . . . . . . 2.1.1 Denition of DSLs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1.2 Main features of a DSL . . . . . . . . . . . . . . . . . . . . . . . . . 2.1.3 DSL development . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1.4 Using DSL in medical eld . . . . . . . . . . . . . . . . . . . . . . . 2.1.5 Discussion with respect to DSL . . . . . . . . . . . . . . . . . . . . . 2.2 Timed automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Chapter 2 .

 2 State of the artDATA were introduced in[START_REF] Belala | Formalisation des systémes temps-réel avec durées d'actions[END_REF]. The major dierence of this model compared to the model of timed automata is found in the associated states invariants. Indeed each state of the automaton (except the start state) has a termination condition of the action potentially in execution. This condition is of the form {x ≥ t} , where x ∈ X and t ∈ R + .

Figure 2 .

 2 Figure 2.3 illustrates the principle of model checking. The model checker can be denedas the tool that allows to realize the model checking, since it receives as input the model and the property to verify, and provides as an output the answer regarding the property (if it's satised or not)[START_REF] Baier | Principles of Model Checking (Represe ntation and Mind Series)[END_REF].

Figure 2 . 3 :

 23 Figure 2.3: Principle of model checking

Figure 2 . 5 :Figure 2 . 6 :

 2526 Figure 2.5: UPPAAL: simulation environment

  persons in their own homes. The proposed DSL includes several predened activities identied by our analysis of the application domain. Examples of the predened activities are: (i) Health services: monitor medications, drug injection, aftercare, etc. (ii) Activities of daily living: bathing, assist with meal planning and preparation, dressing, maintain clean household, etc. Each activity is associated with description which provides additional information about the activity, in particular, a description of an activity includes the required qualication of the actors who are allowed to carry out the activity as well as the temporal constraint expressed as quadruplet (Period, Days, Time ranges, Duration), where:

2 .

 2 <starting-date>::=/a date with the format mm/dd/yy/ 3. <ending-date>::=/a date with the format mm/dd/yy/ • Days 1. <days-expression-form1>::= <date>+|"holiday" | <date>+"holiday" 2. <days-expression-form2>::=<day-of-week>+["except("<date>*["holiday"]")"] 3. <days-expression-form3>::="everyday"|"every(n)days("<date>")"["except(" <date >* <day-of-week>* ["holiday"]")"] where: 4. <date>::=/a date with the format mm/dd/yy/ 5. <day-of-week>::= "monday"| "tuesday" |"wednesday" | "thursday" |"friday"| "saturday" | "sunday" • Time ranges 1. <intervals>::= (<integer> "times") |<interval>+ where: 2. <integer>::= /number of occurrences of the activity in the day/ 3. <interval>::=<string-form>|<pair-form>|<hour-form> 4. <string-form>::="morning"|"midday"|"afternoon" |"evening"|"night" 5. <pair-form>::=<starting-hour>"-"<ending-hour> 6. <hour-form>::=<hour> /an hour with the format hh:mm Note that Days and Time ranges can take dierent forms (patterns). Patterns associated with Days can be: (a) Absolute dates, expressed as <days-expression-form1>, species the specic date in a time range (holidays is used to describe all the dates of public holidays); (b) Relative days, expressed as <days-expression-form2>, species days of a week; or (c) Everyday, expressed as <days-expression-form3>, species that the activity occurs repetitively everyday or every n days from a given date. Patterns associated with Time ranges are periods in the day (e.g. morning, afternoon, evening, night), time interval (e.g. 10h-11h), or a starting hour of the activity (e.g. 10h).

3 . 2 .

 32 General modeling process with timed automata 53

3+( 7 -

 7 is the set of transitions. Each transition corresponds to a day of the week. The number of transitions is: N bT ransitions = NbDays)+NbDays * 2 * N bT imeRanges. Where 3 corresponds to the two return transitions to the initial state (the rst one to reset x d in the same week,

( 1 , 2 , 3 , 4 ,

 1234 10 and 11) express the fact that the activity Toilet does not take place during the other days of the week except Thursday ie. (Sat- urday, Sunday, Monday, Tuesday, Wednesday and Friday). However, Thursday is represented by three transitions labeled dierently: the transition 5 expresses the fact that the activity Toilet is done every Thursday that are in the period before the 05/01/14, transition 6 is used to respect the xed duration of the activity. Same thing for the transitions 8 and 9 but this time the activity Toilet is done every Thursday that are in the period after 05/01/14. At the end, the transition 7 expresses the fact that on Thursday 05/01/14 the activity Toilet is not performed. Transitions 13 and 12 are respectively used to reset the clock of days in the same week of the period and to reset the clocks of days and weeks in the same period. Transition 14 is used to express the end of the period and terminates the execution of the automaton. For example a timed word = (Toilet, 6240 ).(Toilet, 16320).(Toilet, 26400).(Toilet, 36480).(Toilet, 46560).(Toilet, 56640).(Toilet, 66720).(Toilet, 76800).(Toilet, 86880).(Toilet, 96960).(Toilet, 107040).(Toilet, 117120).(Toilet, 127200).(Toilet, 137280).(Toilet,147360). (Toilet, 157440).(Toilet, 167520).(Toilet, 177600).(Toilet, 187680).(Toilet, 197760).(Toilet, 207840).(Toilet, 217920).(Toilet, 228000).(Toilet, 238080).(Toilet, 248160).(Toilet, 258240).(Toilet, 268320). (Toilet, 278400).(Toilet, 288480).(Toilet, 298560).(Toilet, 308640). (Toilet, 318720).(Toilet, 328800).(Toilet, 338880).(Toilet, 348960).(Toilet, 359040).(Toilet, 369120).(Toilet, 379200).(Toilet, 389280).(Toilet, 399360).(Toilet, 409440).(Toilet, 419520). (Toilet, 429600).(Toilet, 439680).(Toilet, 449760).(Toilet, 459840).(Toilet, 469920). (Toilet, 480000).(Toilet, 490080). (Toilet, 500160).(Toilet, 510240). is an execution which is accepted by the automaton of Figure 3.5

  is the set of clocks expressed in terms of minutes where x d is used to control the execution of the activity in a time of the day, x t is used to control the activity duration and x p is used to control the execution of the activity in a day of the period;• Inv ={∀s ∈ S, Inv(s) = (x d ≤ EndT imeRanged) and s ∈ St, Inv(s) = (x d ≤ 24h) and s ∈ W, Inv(s) = (x t ≤ d) and s ∈ E}; • T ⊆ S × Σ ∪{ε}×φ(X) × 2 X ×S is the set of transitions. The number of transitions between two states of time range depends of the number of the specied dates for an activity. The number of transitions N bT ransitions =2 + N bT imeRanges * 2 * N bDates + N bIntervals. Where N bDates is the the number of specic dates when the activity will be performed during the period, N bIntervals is the number of intervals [Start date, End date] where the activity will not be performed, and 2 corresponds to the return transition to the start state and the transition to the nal state.

3 . 67 3. 3

 3673 Formal analysis of home care plan using timed automata Formal analysis of home care plan using timed automata With a formal model describing the behavior of home care plans at hand, it becomes now possible to handle automatic verication and monitoring of home care plans. Here we focus on realizability verication, monitoring and interventions generation. These verication tasks are important in the sense that a planning error or a bad monitoring can have dramatic consequences.

Figure 3 . 13 :

 313 Figure 3.13: Emptiness checking timed automata with UPPAAL.

  patibility of time ranges by taking into account the duration of each activity (multiple congurations are possible). It is also necessary to ensure that the grouped activities can be made by a same type of actor. The composition operator can be modied in order to incorporate the interventions in the computed care plan automaton (the obtained automaton is called interventions automaton). This is achieved by modifying the activity automaton in order to take into account the Intervention state. More precisely, we modify Denition 3.2.1 to consider an automaton as a tuple A= (S, s 0 , Σ, X, Inv, T, F, W, E, St, Int) where Int denotes the set of intervention states. In addition, a specic time parameter, denoted Tmin, is added to control the idle time between the activities within the same intervention. Tmin can be dened as " the minimum waiting time between two activities before starting a new intervention". In fact, the value of Tmin can be used as a parameter that can be dened by the coordinator and given as input to the composition operator to compute the interventions automaton (i.e., care plan annotated with interventions).

Figure 3 .

 3 Figure 3.14 shows how the automaton of Figure 3.11 is modied to illustrate the Toilet automaton with interventions which will be used to generate interventions automaton. Indeed, let A Int be the automaton corresponding to Toilet automaton with interventions.

Figure 4 .

 4 Figure 4.1 illustrates through a BPMN 3 process, a structured overview of the general functioning of our prototype, since the elaboration of the home care plan by the coordinator, till its verication phase.

Figure 4 .

 4 5 four dierent planned activities. Temporal specications are edited into four main elds: Days, Ranges, Period and Duration. The values of these elds can be entered through a dialogue box (4.2.1.2) to allow an assisted entry.

Figure 4 . 5 :

 45 Figure 4.5: Editing home care plan activities

83 Figure 4 . 10 :

 83410 Figure 4.10: Part of an XML le generated by care plan automata generator

Figure 4 .

 4 [START_REF] Arango | Domain analysis: From art form to engineering discipline[END_REF] shows how UPPAAL Model Checker uses TCTL queries.

Figure 4 . 11 :Figure 4 . 12 :: 1 . 2 . 3 .

 411412123 Figure 4.11: UPPAAL uses XML le of Figure 4.10 to display the corresponding care plan timed automaton

  Dierent optimisation criteria such as minimize the global waiting time of interventions. Minimize the total number of interventions and dierent costs problems. Execute the home care plan automaton with interventions using UPPAAL. This enables to generate all possible schedules of interventions to perform at patient's home. Timed words of such automaton satisfy the rst two requirements. Time range of each intervention and dierent optimisation problems have not been considered in our current prototype. Implementation of the optimisation problems require a specic investigation. 5. Once the interventions are generated, the most qualied (having the highest skills)

  observe that the activity Parenteral nutrition is scheduled on 01/11/2015 at 10H00 and takes 40 minutes. If it starts execution and ends after 40 minutes, the following activity Dress which is also scheduled from 10H00 to 11H00 on 01/11/2015 and takes 45 minutes will not be performed and nished before 11H00. For this reason, a deadlock in the care plan automaton execution is detected. The coordinator must then re-edit the care plan.

Figure 4 . 16 :

 416 Figure 4.16: Dialog box showing the non realizability of a care plan

Figure 4 .

 4 Figure 4.17 shows the list of interventions through the GUI for the coordinator.

  [START_REF] Alur | Timed automata[END_REF].1 for which we test the monitoring.

  2.2.1 Clock valuations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2.2 Semantic of timed automata . . . . . . . . . . . . . . . . . . . . . . . 2.2.3 Properties of timed automata . . . . . . . . . . . . . . . . . . . . . . 2.2.4 Variants of Timed automata . . . . . . . . . . . . . . . . . . . . . . . 2.2.5 Software tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2.6 Timed automata in the medical eld . . . . . . . . . . . . . . . . . . 2.2.7 Discussion with respect to timed automata . . . . . . . . . . . . . . 2.3 Conclusion of Chapter 2 . . . . . . . . . . . . . . . . . . . . . . . .

	Chapter 2. State of the art

Table 3 .

 3 1: Specication of activities Toilet and Dress specication is therefore (E1) except (Day1 Day2 Day3 ...) where (E1) is a specication that can be expressed by the quadruplet (days, time range, period, duration) and Day1 Day2

	3.2. General modeling process with timed automata	51
	Activity Days Toilet Monday Wednesday Friday morning evening 01/01/13-03/31/13 30 Time ranges Period Duration Sunday morning 01/01/13-03/31/13 Dress Everyday except(04/20/13) morning evening 01/01/13-03/31/13 20 04/20/13 morning 01/01/13-03/31/13

•

  X= {x d , x t , x p }; • T is the set of the following transitions: Transition (2) species that when the automaton is at state s o , it can move to state s 1 to trigger the execution of the activity T oilet in the state s 1 on condition that the conjunction of state invariant (x d ≤ 690). Where 690 minutes = (12h*60minutes)-30 minutes of activity duration at s 0 and the transition guard (x d ≥ 480 && x p ≥ 1440 && x p < 2880) allow it. (x d ≥ 480) ensures that the activity T oilet can be performed only in the morning and (x p ≥ 1440 && x w < 2880) ensures that the activity T oilet takes place in the date 05/06/2013 of the period. The transition (3) is used to respect the xed duration of the activity. The state invariant ( x t ≤ 30) ensures that the automata stays at state s 1 during 30 minutes to perform the activity T oilet.

	Same principle for transition (5 and 6) for 05/08/2013, and transitions (7 and
	8) for 05/09/2013.

  • T is the set of transitions where N bT ransitions = N bT imeRanges * 2 + 2. We will see the meaning of each transition:Transition (1) species that when the automaton is at state s 0 , it can move to state s 1 to trigger the execution of the activity Toilet in the state s 1 . The conjunction of state invariant (x d ≤ 690) at s 0 and the transition guard (x d ≥ 480) ensure that the activity T oilet can be performed only in the morning (i.e., when the value of x d is between 480 and 690). Transition (2) is used to respect the xed duration of the activity. The state invariant ( x t ≤ 30) ensures that the automata stays at state s 1 during 30 minutes to perform the activity Toilet. (3) enables the automaton to move back from s 2 to s 0 , without performing any activity, at the end of the day (i.e., when x d equals 1440) within the specied period (i.e., x p < 525600). Upon this transition, the clock x d is reset to record the beginning of a new day.

	Transition

  1 , s 2 ), a, φ, λ, (s 1 , s 2 )): ((s 1 ,a,φ,λ,s 1 ) ∈ T 1 , s 2 =s 2 ) or ((s 2 , a, φ, λ, s 2 )∈ T 2 , s 1 =s 1 ), s 1 and s 2 are both start states, or, s 1 is start state and s 2 is waiting state, or, s 1 is waiting and s 2 is start state }.3. {((s1 , s 2 ), a, φ, λ, (s 1 , s 2 )): ((s 1 , a, φ, λ, s 1 )∈ T 1 , s 2 =s 2 ,s 2 is a waiting/start state, s 1 is an execution state) or ((s 2 , a, φ, λ, s 2 )∈ T 2 ,s 1 =s 1 ,s 1 is a waiting/start state, s 2 is an execution state) }.

  E<> (Process.S0S'1) && (Process.xp >= 1440 && Process.xp < 2880 && Process.xd >= 660 && Process.xd <= 720).

  IntIn order to test and validate our work, we have implemented the approach that we proposed in this thesis. We implemented our prototype as a part of the project Plas'O'Soins,

		Chapter 4. Prototype and experimentations
	which aims to provide a software platform for modeling, planning and monitoring home
	care plans. Pointing out that our work is in parallel with Plas'O'Soins project and
	we address identied problems with another vision. We have the same starting point,
	namely, temporal specications. But we bring other performance such as realizability
	check, monitoring and interventions generation using UPPAAL Model Checker. As part
	of this thesis, we developed four main components: (i)
	intervention
	Toilet	Dress	Toilet

  Upon admission of a new patient, the coordinator creates for him/her a personalized home care plan, taking into account his/her medical needs as well as his/her social and physical environments. This activity is represented by the collapsed subprocess Create Home care plan (see Figure4.1). An expended version of the decomposable activity CreateHome care plan is shown in Figure4.2.This latter presents the set of elementary human

1 https://netbeans.org 2 https://vaadin.com/home 3 http://www.omg.org/spec/BPMN/2.0/PDF/ Create Home care plan

http://plasosoins.univ-jfc.fr/

http://www.iminds.be/en/projects/2014/03/07/coplintho

hhttp://www.presenceverte.fr

http://www.diatelic.com

arcan.fr

http://www.medisys.fr/

www.med-link.org

http://hippocad.com/

http://www.agence-nationale-recherche.fr/

http://www.dsmforum.org/tools.html

, which provides development tools based on models. It consists on three frameworks (Eclipse Modeling Framework (EMF

), Graphical Editing Framework (GEF

), Graphi- cal Modeling Framework (GMF

5 )). (2)

MetaEdit+ 6 , which is an environment used for 2 http://www.eclipse.org/modeling/ 3 http://www.eclipse.org/modeling/emf/ 4 http://www.eclipse.org/gef/ 5 http://www.dsmforum.org/tools.html 6 http://www.metacase.com/products.html

Projection enables to map a timed automaton A to timed automaton B by replacing the alphabet which is not in B by ε.

An hybrid timed automata combines both continuous and discret behavioral[START_REF] Alur | Symbolic analysis of hybrid systems[END_REF]

http://fr.mathworks.com/products/simulink/

http://fr.mathworks.com/products/stateow/

Closed-loop context of the patient is " a function of both the environment and the input from the device controller and must be captured by the device evaluation process"[START_REF] Mangharam | Cyber-physical modeling of implementable crdiac medical devices[END_REF]

Note that UPPAAL model checker uses a subset of TCTL (Timed CTL) as query language to express properties.

Proceedings of the 13th International Conference, ICCSA, pages 475490. Springer Berlin Heidelberg, 2013.