5 March 2018: Juliana Bowles Title: Combining Formal Methods in Healthcare Abstract: This talk shows different logic-based approaches to detect and resolve conflicts in the treatment of multiple chronic conditions, and model and compare treatment options for chronic conditions. We developed an automated approach focusing on the composition of (static or behavioural) design models via constraint solvers. This approach is directly applicable to many different domains, and can be used for the detection of conflicts in clinical pathways. Clinical pathways are care plans which detail essential steps in the care of patients with a specific clinical problem, usually a chronic disease. A pathway includes recommendations of medications prescribed at different stages of the care plan. For patients with three or more chronic diseases (known as multimorbidities) the multiple pathways have to be applied together. One common problem for such patients is the possible adverse interaction between medications given for different diseases. In this context, we have used an optimising SMT solver (Z3) to quickly find the set of medications with the minimal number and severity of conflicts which is assumed to be the safest. In our approach we can vary the measures of interest to obtain different outcomes and generate the best option, second best, etc. We use a combination of SMT solvers and theorem provers for checking correctness. Conversely, automata can be used to capture the stages and treatment options for a chronic disease, where traces in the model highlight different treatments plans that patients can follow. Adding further information to such models allow us to explore extensions and combinations of different variants of timed automata and associated tools in different ways. We can combine patient information and comorbidities with the disease automaton through composition. We have explored the use of model checking as an analysis technique to provide further insights into the effectiveness/completeness of treatment plans for a given patient. Bio: Juliana Bowles (née Küster-Filipe) is a senior lecturer at the School of Computer Science, University of St Andrews, Scotland. She has research interests in formal methods and dependability, logics and models for true-concurrency, and foundations of modelling languages. She is currently applying her foundational work to the healthcare domain, and has an EPSRC-funded project on "Automated Conflict Resolution in Clinical Pathways". Bowles received her PhD (Dr.rer.nat) from the Technical University of Braunschweig, Germany, in 2000. Website: https://www.cs.st-andrews.ac.uk/directory/person&id=juliana Mar 05 2018 14.00 - 15.00 5 March 2018: Juliana Bowles Combining Formal Methods in Healthcare IF 4.31/4.33
5 March 2018: Juliana Bowles Title: Combining Formal Methods in Healthcare Abstract: This talk shows different logic-based approaches to detect and resolve conflicts in the treatment of multiple chronic conditions, and model and compare treatment options for chronic conditions. We developed an automated approach focusing on the composition of (static or behavioural) design models via constraint solvers. This approach is directly applicable to many different domains, and can be used for the detection of conflicts in clinical pathways. Clinical pathways are care plans which detail essential steps in the care of patients with a specific clinical problem, usually a chronic disease. A pathway includes recommendations of medications prescribed at different stages of the care plan. For patients with three or more chronic diseases (known as multimorbidities) the multiple pathways have to be applied together. One common problem for such patients is the possible adverse interaction between medications given for different diseases. In this context, we have used an optimising SMT solver (Z3) to quickly find the set of medications with the minimal number and severity of conflicts which is assumed to be the safest. In our approach we can vary the measures of interest to obtain different outcomes and generate the best option, second best, etc. We use a combination of SMT solvers and theorem provers for checking correctness. Conversely, automata can be used to capture the stages and treatment options for a chronic disease, where traces in the model highlight different treatments plans that patients can follow. Adding further information to such models allow us to explore extensions and combinations of different variants of timed automata and associated tools in different ways. We can combine patient information and comorbidities with the disease automaton through composition. We have explored the use of model checking as an analysis technique to provide further insights into the effectiveness/completeness of treatment plans for a given patient. Bio: Juliana Bowles (née Küster-Filipe) is a senior lecturer at the School of Computer Science, University of St Andrews, Scotland. She has research interests in formal methods and dependability, logics and models for true-concurrency, and foundations of modelling languages. She is currently applying her foundational work to the healthcare domain, and has an EPSRC-funded project on "Automated Conflict Resolution in Clinical Pathways". Bowles received her PhD (Dr.rer.nat) from the Technical University of Braunschweig, Germany, in 2000. Website: https://www.cs.st-andrews.ac.uk/directory/person&id=juliana Mar 05 2018 14.00 - 15.00 5 March 2018: Juliana Bowles Combining Formal Methods in Healthcare IF 4.31/4.33
