Generating Safety Guidance for Medical Injection with Three-Compartment Pharmacokinetics Model

Medical cyber-physical systems are a new trend of software controlled physical systems that are increasingly common in medical domains. With rapid developments in medical science and computer technology, safety verification and simulation becomes more challenging. This paper introduces a general model for medical injection systems, which can be used for formal verification, simulation/testing, and computing the Area Under the Curve (AUC) metrics, using Satisfiability Modulo Theories (SMT) over Reals. An algorithm of computing constrained AUC for measuring drug exposure with relative baseline, is presented based on the proof of unsatisfiability. We demonstrate that our model can efficiently solve these problems using the state-of-the-art SMT solver dReal.