Formal Modeling and Analysis of Home Care Plans

A home care plan defines all the services provided for a given patient at his/her own home and permits the coordination of the involved health care professionals. In this paper, we present a DSL (Domain specific language) based approach tailored to express home care plans using high level and user-oriented abstractions. Then we describe how home care plans, formalized as timed automata, can be automatically generated from these abstractions. We finally show how verification and monitoring of the resulting care plan can be handled using existing techniques and tools.