Using Timed Automata Framework for Modeling Home Care Plans

A home care plan defines the set of medical and/or social activities that are carried out day after day at a patient´s home. Such a care plan is usually constructed through a complex process involving a comprehensive assessment of patient´s needs as well as his/her social and physical environment. Specification of home care plans is challenging for several reasons: care plans are inherently non-structured processes which involve repetitive, but irregular, activities, whose specification requires complex temporal expressions. These features make home care plans difficult to model using traditional process modeling technologies. In this paper, we describe how home care plans, formalized as timed automata, can be generated from a set of high level and user-oriented abstractions. The resulting care plan encompasses all the possible allowed schedules of activities for a given patient. We discuss then how verification and monitoring of the resulting care plan can be handled using existing techniques and tools (e.g., UPPAAL model checker).