Machine Learning (ML) technologies have been increasingly adopted in Medical Cyber-Physical Systems (MCPS) to enable smart healthcare. Assuring the safety and efectiveness of learning-enabled MCPS is challenging, as such systems must account for diverse patient profiles and physiological dynamics and handle operational uncertainties. In this paper, we develop a safety assurance case for ML controllers in learning-enabled MCPS, with an emphasis on establishing confidence in the ML-based predictions. We present the safety assurance case in detail for Artificial Pancreas Systems (APS) as a representative application of learning-enabled MCPS, and provide a detailed analysis by implementing a deep neural network for the prediction in APS. We check the suficiency of the ML data and analyze the correctness of the ML-based prediction using formal verification. Finally, we outline open research problems based on our experience in this paper.
ported by evidence, to justify claims for an application Medical Cyber-Physical Systems (MCPS) integrate con- in a given environment [3]. Recent eforts in safety analnected software and hardware components with sensors ysis and assurance have confirmed that AC are valuable and actuators to monitor and control patient physiology. for assessing and demonstrating trust [4]. For example, Machine Learning (ML) technologies have been increas- AC have been deployed for unmanned aircraft systems ingly used in MCPS, often deployed in the estimation [5] and medical devices [6]. The U.S. FDA has also isand prediction components, to make data-driven deci- sued a guideline [7] suggesting medical manufacturers sions based on sensor or patient input and guide control provide AC with pre-market submissions. Among the actions [1]. Ensuring the successful deployment of ML standards published by various organizations (e.g., ISO within MCPS can be challenging, as the ML components 26262 [8], ISO/PAS 21448 [9], ANSI/UL 4600 [10], and must be able to handle the intricacies of patient physiol- the FDA guideline for Artificial Pancreas Systems (APS) ogy, time lags between the impact of a control action and [11]), ANSI/UL 4600 is the only one ofering evaluations sensor measurements, uncertainties in the operational of ML technology for the safety of autonomous vehicles. environment that may afect the patient’s physiology, Among more AC-centric studies, Hawkins et al. [12] and variability in patient profiles which may result in provide a guideline on the assurance of ML in audifering impacts of the control actions. Moreover, due to tonomous systems, including a safety case pattern for physiological complexities and the limited availability of each stage of the ML life cycle. Kaur et al. [13] proposed realistic patient profiles or datasets, ML techniques may a modular assurance case pattern based on assume/guaruse synthetic data or virtual patient models for training. antee reasoning for ML-enabled CPS, where the safety of The mismatch between the training data and the real- the ML component and the rest of the system are assessed world data seen in deployment may result in erroneous, separately. However, the ML lifecycle is not dealt with in biased, or incomplete output predictions [2]. Failure of this pattern. A few studies have also developed AC for the ML component due to any of the challenges noted concrete learning-enabled use cases in the automotive above could result in irreparable harm to patients. As domain [14, 15, 16]. Within the healthcare domain, [17] such, the use of ML within MCPS should be assured by is the only work that presents an assurance case pattern evidence that these components are safe and reliable [2]. to justify the use of ML. Even so, none of [12]-[17] inAssurance cases (AC) are structured arguments, sup- stantiate the process activities and generate evidence for a concrete application in the medical domain. This paper SafeAI: The AAAI’s Workshop on Artificial Intelligence Safety, Feb tackles this gap by presenting detailed AC to assure the 13–14, 2023, Washington, D.C., US safety and efectiveness of a general framework of APS * Corresponding author. [18], suitable for all types of APS. We select APS as a 0000-0001-9576-2478 (M. Bagheri); 0000-0002-4982-7768 representative of learning-enabled MCPS as it contains (J. Lamp); 0000-0002-3663-7447 (X. Zhou); 0000-0002-4651-8441 a collection of typical components of many ML-enabled (L. Feng); 0000-0001-5279-842X (H. Alemzadeh)
Copyright © 2023 for this paper by its authors. Use permitted under Creative Commons License MCPS, including data-driven estimation algorithms and CPWrEooUrckReshdoinpgs IhStpN:/c1e6u1r3-w-0s.o7r3g ACttEribUutRion W4.0oInrtekrnsahtioonpal (PCCroBYce4.0e).dings (CEUR-WS.org) embedded controllers for insulin dosage calculation.
Expanding on the patterns proposed in [12, 13], we develop a safety assurance case for the ML-enabled controller of MCPS, consisting of a controller algorithm and an ML prediction algorithm, where our emphasis is greatly on the ML-based prediction. By proving trust in ML prediction, the safety of the controller algorithm can be assessed in isolation. Considering the patient as an essential element of the control loop, we discuss the AC elements that should be instantiated based on an individual patient profile or a population of patients. The instantiation is due to diferent physiologies of diferent Figure 1: The structure of APS (modified from [20]). The APS patients, which may afect control actions, the ML con- controller consists of a prediction algorithm to predict the BG troller’s expected behavior, and the claims satisfaction. values and a controller algorithm to adjust the insulin dosage. This is the first time that the patient profiles are included in AC for ML controllers and MCPS. In support of claims BG values, an APS controller that calculates the correct in AC for APS, we implement a deep neural network for insulin dosages based on the CGM and user input, and blood glucose prediction in APS. We then present an anal- an insulin pump that delivers insulin dosages. ysis characterizing the suficiency of the training data The APS controller consists of a data-driven glucose for the ML controller and the ML development process. prediction algorithm to predict future BG values and a We also utilize APS domain knowledge to specify a set control algorithm to adjust the insulin dosage based on of properties based on a patient’s metabolism (e.g., in- the predicted BG values. Recently, researchers have besulin senstivity, carbohydrate absorption profile) and use gun exploring the use of neural networks [21, 22] and formal verification to check them against the ML predic- reinforcement learning [23] for the design of the APS tion component. We are unaware of any work verifying controllers (e.g., use of machine learning for glucose prethe ML components in APS except [19], which unlike us, diction). The primary objective of the controller is to compares the output ranges of two identical networks provide safe and eficient glycemic control by infusing given a slight change in their input ranges. an appropriate amount of insulin to keep the patient’s Contributions. The major contributions of this paper BG within the proper range (between 70 and 180 mg/dL) are summarized as follows: and avoid hypoglycemias and hyperglcemias. To provide such safe control, the controller needs to account for the • We present preliminary results on developing a safety complexities of glucose metabolism and deal with unassurance case template for ML controllers in MCPS, predicted meal intake, exercise, stress, or illness, rapid which includes patient profiles in its element descrip- changes in BG concentration, and time lags between BG tions. measurement and insulin impact. • We present a detailed safety assurance case for APS As of the date of this writing, there are four commerthat is supported by a thorough analysis of ML-based cially available APS that have received FDA approval glucose prediction module. and/or the Conformité Européenne (CE) mark: Medtronic • We define properties based on the body’s metabolism MiniMed 670/770/780G [24], Tandem Control-IQ [25], and check them against the ML prediction component Omnipod 5 [26], and CamAPS FX [27]. These systems using formal verification. use some form of data-driven learning algorithm, i.e., Tandem Control-IQ uses a simple linear regression algorithm In the end, we discuss open research problems in devel- [28] to predict BG values 30 minutes in the future and oping safety assurance cases for learning-enabled MCPS. then a PID algorithm to adjust the insulin dosage based 2. Artificial Pancreas Systems on the predicted BG values. To ensure the adoption and use of such systems, patients need to be confident in the underlying ML technology embedded in the controllers.
patient’s pancreas produces little to no insulin. Patients with T1D must constantly monitor their blood glucose (BG) levels and inject insulin to regulate their concentrations of BG. Artificial Pancreas Systems (APS) are closedloop insulin delivery systems that relieve the burden of T1D on patients by regulating a patient’s BG level, using input from various sensors such as continuous glucose monitors (CGM). Figure 1 depicts the typical structure of APS, consisting of a CGM sensor to continuously monitor
Typical CPS consist of embedded software and hardware components controlling the plant through interconnected sensors and actuators. MCPS are a distinct class of CPS with the patient as the plant, aiming to monitor and control multiple aspects of the patient’s physiology. With the patient in the control loop, the MCPS should either be tailored for specific physiological parameters of the patient C0-1 Cdeosmcrpiopntieonnt P
A0-1 ML_abs as an abstraction of the ML component is safe
G0 {Learning-enabled controller c}, composed of ML, is safe and effective in treating the patient.
S0-1 Argument byAssume/Guarantee reasoning
C0-2 System safety requirements allocated to {Learningenabled controller c} G1-1 {Controller c}, composed with ML_abs, is sufficiently safe and effective in treating the patient
G1-2 The ML (prediction/perception) component is sufficiently safe and effective outputs of the ML component are safe, as presented in assumption A0-1, goal G1-1 claims that the controller component combined with _ is safe and efective.
or should cover a population of patients. This adaptation is even more critical as a part of the design process in learning-enabled MCPS that employ a learning-enabled controller, a controller relying on machine learning to perform perception or prediction tasks. So, in the regulatory process for checking the safety of MCPS, it would make sense to instantiate the safety assurance case for individual patient profiles or populations. To emphasize this, we mark the context elements in safety assurance cases with the uppercase letter P in a half circle to denote the decision points where the context needs to be initialized for an individual patient profile or the population.
The top-level goal in safety AC of learning-enabled MCPS is to ensure that "x as a case of learning-enabled MCPS is safe and efective". Confidence in this claim is obtained by ensuring the safety and efectiveness of all constituent components, including sensors, actuators, and their interactions. For this paper, we discuss only the safety and efectiveness of the learning-enabled controller, assuming that the safety and efectiveness of other components have been adequately examined. We first present a safety assurance case template for a learning-enabled controller in MCPS, shown in Figure 2. We then use APS as an instance of MCPS and explain how instantiating the template results in a general safety assurance case for APS. We use goal structuring notation (GSN) [29], with a slight of notation abuse, to show our AC.
lying the APS, the main components of APS remain the same, i.e., they all consist of a learning-enabled controller.
Additionally, APS should satisfy a set of safety and performance properties common and desirable to regulatory agencies. For instance, requirements specified by the FDA [11] include high accuracy of CGM readings, safe insulin dosages, usable design, and so on. The most significant requirement is that APS must not increase the incidence 3.1. Safety Assurance Case Template for and severity of hypoglycemic and hyperglycemic events.
learning-enabled controllers in MCPS These reasons induce a general safety assurance case to The root goal G0 in Figure 2 asserts that the learning- be developed for all APS, like [30] which presents AC enabled controller is safe and efective while the device for a generic infusion pump device. Thus, the proposed is used in treating the patient. The environment and the template in Figure 2 can be employed for APS, where system within which the learning-enabled controller is goals G1-1 and G1-2 are modified as follows. used are described in context C0-1, and the requirements • G1-1: Assuming that the BG predictions are accurate, assigned to the learning-enabled controller are explained the insulin dosage management component is suficiently in context C0-2. We use assume/guarantee reasoning safe and efective for treating patients. to justify goal G0. This is because the learning-enabled • G1-2: The ML glucose prediction component is suficontroller is a combination of two main algorithms that ciently safe and efective. perform in sequence: an algorithm that performs the ML Context Elements. Context C0-1 describes inputs to tasks and delivers its output to the control algorithm, and the APS controller (i.e., history of the CGM values and the control algorithm that selects the control action and insulin injected and prediction horizon), outputs of the initiates it in the system. Assuming that the results pro- controller (i.e., the amount of insulin to be injected), the vided by the ML tasks are correct, the control algorithm component’s role in the system, and the environmental should guarantee the safe and efective treatment of the phenomena (i.e., uncertain meal intake, daily activity). patient. Hereafter, we use the term controller to refer to Context C0-2 includes all requirements of the learningthe control algorithm of the learning-enabled controller. enabled controller. Table 1 shows a set of these requireWe consider a separate component for each algorithm. ments, which we have extracted from the diabetes treatAs reflected in goal G1-2, the safety and efectiveness of ment literature (e.g., [31]). The main requirement in the ML component are justified in isolation. The con- Table 1 is RQ.C.1, which is further refined into its followtroller’s input is an interface with the ML component, ing requirements. Although this is not an extensive list containing the results received from the ML component. of requirements, it represents some of the most imporThis interface shows an abstraction of the ML compo- tant requirements for such a system. A few examples of nent, denoted as _ in goal G1-1. Assuming the peripheral requirements are related to the controller’s platform, such as security, reliability, and usability. For example, the smartphone used in some of the APS is a platform. The goal G1-1 is also defined in the same context as C0-2 since it claims the safety and efectiveness of the APS controller when BG predictions are reliable. We assume that the controller requirements are adequately examined in consultation with domain experts and medical professionals and do not discuss them in this paper.
Patient or Population. The contexts C0-1 and C0-2 can be defined based on an individual patient profile or a population of patients. A clear example of this decision is that diferent patients have varying insulin sensitivity levels, and their physiologies may be afected diferently by meal volume or activity. In addition to the training datasets and the control algorithms themselves, other components such as thresholds and target values that afect the requirements, can be defined diferently based on individual patients or a population of patients.
In the next section, we develop a general argument for goal G1-2, claiming that the ML glucose prediction component is suficiently safe and efective.
C1-1 Description of the ML glucose prediction component P
G1-2 The ML glucose prediction component is sufficiently safe and effective S1-1 Argument over the development and deployment of the component C1-2 System safety requirements allocated to ML glucose prediction component P G2-1 The development of the ML glucose prediction model is sufficiently safe and effective G2-2 The deployment of the ML glucose prediction component intoAPS is sufficiently safe and effective
C2-1 ML safety requirements, developed from system safety requirements, allocated to the ML glucose perdition model P
S2-1 Argument over the ML safety and effectiveness requirements G3-1 ML glucose prediction model satisfies the ML requirements G3-2 ML requirements are a valid development of the APS requirements allocated to the glucose prediction component
This claim is supported by contexts C1-1 and C1-2. Context C1-1 describes the ML prediction component, its expected inputs and outputs (e.g., CGM, insulin, and meal values), along with their possible sources and targets (e.g., various CGM or pump devices). Besides, it is necessary to determine whether the component is specialized based on a patient profile or a population of patients.
We categorize the requirements allocated to the ML glucose prediction component into performance and roTabnuhdsetsanereersesdqeruefiniqeruedmiirneemncotesnnattersxeatinnCdd1e-e2pn.euMnmdLee-rnRatQtoe1ftiMhseLtmhteeinpchrTinmaoballoreyg2y. pCreM3d-i1Lctgioluncmosoedel aMrgLPulmeaernnting GsMa3tL-i1sgfileuscothsee MprLedriecqtiuoinremmoednetsl aMrgLudmaetant sMynLthCcel3itni-c2icdaalt/a P performance requirement refined into ML-RQ1.1 through ASr3g-u1ment over satisfaction of ML-RQ1.8 based on the patient’s physiology. Prediction ML safety requirements results are accurate when the learning component has G4-1 G4-2 learned the physiological dynamics of the patients, and aMreLspaetirsffoiremd.ance requirements sMatLisRfioedb.ustness requirements are hence ML-RQ1.1 to ML-RQ1.8 are satisfied. Although we have extracted these requirements from the APS literature, based on our knowledge, it is the first time that Figure 4: Argument to ensure the suficiency of the ML gluphysiologically-inspired requirements are assigned to an cose prediction model.
ML component. The thresholds and target values in these G3-1 is made in context C3-1 of the ML model created rperqoufileisr.eRmoebnutsstndeespsernedquoinremtheenptsatMieLn-tR’sQo2ranpdopMuLla-tRioQn3’s caGpT4arnhe-e1dndidcetvioecinlonmpomocdneenllttiuosefsdtuhxfefeilcteiaernCndt.t ga3lutc-oa2se forfotmGhsT4uh-efef2ioMciMeLnntc.lliLnyicald/asyannttheatiic,ndradtaeiissvpiedcutaivleplayt.iMenLt doartaa refer to variations in the input space of the component. population of patients, and the ML model and its hyperFor instance, ML-RQ2 ensures a variety of patient profiles parameters are tuned based on collected data. The goal are considered in a population-based setting. G3-1 is supported by goals G4-1 and G4-2 claiming that
To justify claim G1-2, the approach of [12] splits the ar- the ML model satisfies the performance and robustness gument based on the development and deployment of the requirements. Further assurance is also needed regarding ML component. Goal G2-1 claims that the development of the ML process and ML data used for development. The the ML model predicting the BG values is suficiently safe ML learning and ML data arguments provide arguments and efective, and goal G2-2 claims that the integration and evidence for the safety and efectiveness of the ML of the ML component into the system is suficiently safe process and ML data. We provide an assurance case for and efective. The G2-2 justification involves techniques the suficiency of ML data in Section 4.3 and concrete evisuch as runtime assessment that are beyond the scope of dence for both arguments in Section 5. The links with the this paper. We leave G2-2 undeveloped and emphasize ML learning and data arguments are established using G2-1. The first step to support claim G2-1 is to develop assurance claim points [12] (black squares), representing ML requirements using the concepts amenable to the ML the points at which further assurance is required. implementation. The performance requirement ML-RQ1 4.3. Suficiency of the ML Data in Table 2 can be measured by the accuracy or mean prediction error of the ML algorithm. Thus, ML-RQ1 is The argument to ensure the suficiency of the ML data defined as “ ML component should predict the glucose is shown in Figure 5. Claim G4-3 justifies that the data value with the mean prediction error of less than thres collected meet desiderata, including relevance, completemg/dL”, where thres is determined by human experts or ness, balance, and accuracy [12], thus, the assurance that compared to the most reliable existing method for BG the model trained on such data satisfies ML requirements prediction. ML-RQ1.1 to ML-RQ1.8 are meaningful to the increases. The first step to check the data against the ML model when defined over inputs and outputs of the desiderata is to provide a list of ML data requirements ML model. We specify these requirements in Section 5. for each desideratum. The sub-claim G5-1 assures that These ML requirements are expressed in context C2-1. the list has suficient ML data requirements, and the sub
The development of the ML component refers to the claim G5-2 checks whether the data meet the ML data reprocess of designing and training the ML model. So, quirements. We enumerate the ML data requirements in claim G2-1 is supported by sub-claims G3-1 and G3-2 Table 3. Section 5 provides concrete evidence to support through strategy S2-1. Goal G3-1 claims that the ML G5-2. In the following, we describe data requirements model satisfies the ML requirements. A complete argu- and their efects on the satisfaction of the performance mentation must demonstrate that the ML requirements and robustness requirements in support of G5-1. are a valid development of the APS requirements allo- The requirements DR.R1 and DR.R2 concern the pocated to the glucose prediction component, as expressed sition of the CGM sensor on the patient’s body and the in claim G3-2. In our case, there is an exact mapping be- format of the data captured by the sensor, respectively. A tween requirements of Table 2 and the ML requirements CGM sensor is worn on specific body areas. It should be (Section 5), so G3-2 is justified. The G3-1 justification is placed around a fattier area of the body, i.e., the upper arm described in the next section. or abdomen for the adult and the abdomen or buttocks for kids. DR.R1 also relates to the accuracy desideratum 4.2. Suficiency of the ML Model (DR.A1), as the sensor position afects the accuracy of the The argument to ensure the suficiency of the ML glu- sensor readings and, consequently, the accuracy of the cose prediction model is shown in Figure 4. The claim BG prediction. The requirement DR.R3 refers to the type G4-3 C4-1 120 pounds. The datasets should not only include sufsTuhfefiMcieLntc.linical /synthetic data is Devieolno/ptemsetndta/tvaesreitficat P ifcient samples with all allowed ages and weights, but also include samples with the combination of these fea
ASr4gM-u1mLesnafteotvyerresqautiirsefmacetinotns of ovMeCrL4thd-e2atcdalairnteaiqsceuatilsr/seymnethnetstic P tshuayrmpeesprl(geDslyRic.nCecm3l)ui.cdD,eRapn.Cadt4iekinsettssopaewcciiidtfiehodsftiroseqeenvuseeunnrttesh.tyhApastogtshlpyeecdceiamfietdaic, G5-1 G5-2 by DR.C5, the data samples shall include the profile of eMnLsudreatiat riseqpuoisrseimbleenttos adreevesuloffpicaiegnlutctoose ML data satisfies the ML patients during the day and night and even in sickness. rperqeduiircetimonenmtso.del that satisfies the ML data requirements. Nighttime sleep and sickness impact metabolic regulation and endocrine release by the pancreas. Considering all the requirements above is crucial to satisfying physioFigure 5: Argument to ensure the suficiency of the ML data. logical properties and ensuring robustness. From the accuracy perspective, the CGM readings and of insulin, i.e., rapid-acting, regular-acting, intermediate- the pump infusions not afected by a system failure must acting, or long-acting, and even the brand of insulin. The be correctly recorded, and the total amount of insulin deAPS controller may support a specific type of insulin, livered for each person be within the limit, as explained as diferent types have diferent absorption mechanisms. by DR.A2 and DR.A3, respectively. The only data reThe APS designed for adults may not be allowed to be quirement regarding the balance desideratum is that the used for kids or vice versa. As DR.R4 explains, a similar number of samples for features should be comparable argument can be expressed for other characteristics such (DR.B1). For instance, the number of samples representas gender, insulin type, etc., and relates to the relevance ing kids and adults should be comparable if the system is desideratum. Sex, age, and insulin type may afect the supposed to work for both categories of kids and adults. satisfaction of physiological and robustness properties. Notably, the dataset should include data from patients
The APS controller should be able to safely adjust the of diferent ages, sexes, weights, etc., if the context is deinsulin dosage in the face of uncertain events such as ifned for a population of patients. Hence, context C4-2 is intraday meal intakes, exercise, and diferent values of annotated with P. Similarly, the size of the development, meal carbohydrates. To support this, as explained by test, and verification datasets change according to the DR.C1, the datasets should include a suficient range of data collected and the model learned, which should be examples in which the appropriate features refer to the reflected in C4-1. So, C4-1 is also annotated with P. mentioned events. If the system is supposed to work for diferent positions of CGM sensor installments, as 5. Concrete Evidence explained by DR.C2, suficient examples regarding each position should be presented in the datasets. A similar In this section, we provide concrete evidence in support requirement can be specified for weight and age. For of ML learning argument, and claims G4-1, G4-2, and instance, consider that the system is designed to work G5-2. We used the Simglucose simulator [32, 33] to genfor people aged 14 to 60 who weigh between 20 and erate synthetic data for T1D patients and trained a FeedForward Neural Network (FFNN) to predict BG values. decreases over the increasing number of epochs but, like The model, contexts, and all properties in our experi- training loss, becomes nearly fixed after a few epochs. ments are based on a population of patients. We per- Evidence for G4-1 and G4-2. We need to ensure formed our experiments on Ubuntu 20.04 with Intel Core that the ML model meets each ML performance and roi7, CPU 3.60GHz × 8, and 15.6 GiB memory. bustness requirement. We used test-based verification
ML Data (Context C3-2). Simglucose is a Python imple- to check ML-RQ1. We split the data into training and mentation of the FDA-approved UVA-Padova Simulator test data with a proportion of 80% to 20%, respectively that employs a glucose-insulin meal model to simulate (context C4-1), and calculated RMSE. We consider ML30 virtual patients (ten adolescents, ten adults, and ten RQ1 is satisfied if RMSE is less than a threshold (i.e., 12 children). Using Simglucose, we emulated all patients mg/dL [21]). The RMSE in our experiments is 3.03 mg/dL. for 40 days and nights, where the BG and insulin values We also used formal verification to check ML-RQ1.1 to are provided every 5 minutes. Simglucose implements a ML-RQ1.8. We employed the DNNV framework [35], basic basal-bolus controller and generates random meals using which we compared the performance of diferent for each patient, where the amount and the time of each NN verifiers and selected Nnenum [ 36]. The properties meal are random numbers from pre-specified intervals. are specified using inputs and outputs of the network Each patient’s data includes 11,521 entries, and each en- by constraining their ranges of values. Table 4 shows try includes a set of features from which we use only BG, the mapping between the performance requirements alinsulin, and meal data. We removed data of 4 adolescents, located to the ML component (Table 2) and the require1 adult, and 5 children from the dataset, since their data ments amenable to the ML implementation. We describe included negative BG values. ML-RQ1.1 and ML-RQ1.2 as an example. In ML-RQ1.1,
ML Model (Context C3-1). Our FFNN has three dense the diference between two consecutive BG values in the layers with 8, 8, and 6 neurons in each layer, respectively. input and output is limited by ∆ . In ML-RQ1.2, we asIt has 36 inputs, including BG, insulin, and meal intake of sume that if meal intake is larger than a value ( 1), BG the patient for an hour (12 timesteps with 5 min intervals) will be greater than a value ( 1). We use an OR condition and predicts BG values 30 minutes into the future (6 to indicate the timestep in which the meal is consumed timesteps). We scale the inputs between 0 and 1. More is not relevant. The meal intake should be suficiently details on the model are available at [34]. large to assure us about its efect on the BG value.
Evidence for ML Learning Argument. This argu- To verify the properties, we first determined ranges ment grounds on the suficiency of the iterative process of values based on the minimum and maximum values to design and train the model. This process selects the of the corresponding variables in the dataset. We also model structure and appropriate values for the model chose the thresholds based on our knowledge of the litparameters. We used the same number of neurons pro- erature (e.g., we set ∆ , the constraint for max glucose posed in [21, 19]. We tested the network with diferent rise/drop over 5 min, to 40 based on [19]). As a result, neurons in each hidden layer and compared them using all properties were violated. This confirms that learning the root mean squared error (RMSE), which was very complex body physiology in the presence of uncertain similar for those networks. We chose eight neurons in meal intake is dificult, and having high precision does the first and second layers of the network, as network not necessarily show the algorithm’s correctness. Selectsize afects verification complexity. To make sure that the ing the thresholds also needs consulting with physicians model does not overfit on data, we plotted training loss and domain experts. So, we considered specific forms of versus validation loss. We observed that validation loss the properties and selected the thresholds with try and 6. Open Research Problems test. We tried to increase the likelihood of property satisfaction by tightening ranges and thresholds. A part of our Herein, based on our experience in developing safety experiments are shown in Table 5. Besides, we checked assurance cases for learning-enabled MCPS, we outline the properties on a network with 128 and 64 neurons in several interesting open research problems. layers one and two. We observed that a property satisfied • We observed that the network structure influences the on the first network is not necessarily satisfied on the satisfaction or violation of a property. Undoubtedly, the other, and vice versa. These experiments confirm the training data, using which the weights in the network need to instantiate AC according to the patient profiles are calculated, also has an impact. How we can trace the or the population. Because the network structure as well violation of a property back to its origin? as the thresholds and ranges of values may change based • The dificulty of learning the patient’s physiology on data available for a patient or a population of patients. solely from the training data may explain why several
The robustness can be checked by measuring RMSE, physiologically-based properties are violated. How can given data of a virtual patient as the test data. The data we enforce the ML model to satisfy the properties while does not include the exercise information (ML-RQ3). it develops over the data?
Evidence for G5-2. Since we use synthetic data, the • RNN is a very commonly used network for time series requirements DR.R1 (DR.A1), DR.R3, and DR.C2 in Ta- data. However, we are unaware of any RNN verifiers ble 3 are not applied to our dataset. Synthetic data gen- that can assess a broad range of properties (not just roeration was conducted via the Dexcom sensor, and this bustness) and are not specialized for specific applications. can serve as evidence to support DR.R2. Simglucose is a Also, the current FFNN verifiers do not support properties simulator to generate data of virtual patients with T1D, with complex structures like ours. How can we develop so DR.R4 is met. If the controller is used for all diabetic an RNN verifier functional for various properties? patients, DR.R5 and DR.C3 are violated since the data is In addition, addressing the following questions can generated for three subject groups of patients, exclud- improve the assurance case. ing the elderly group and patients weighing more than • How to develop adaptive safety AC for online learning 118 kg. We are also uncertain about sex and ethnicity. models, e.g., where the datasets and consequently the Simglucose generates random intraday meal intake. Thus, learned model change during the system operation? DR.C1 is partially met because the data does not include • How to develop quantitative measures to evaluate the exercise information. Over the whole data, 0.14% of the confidence in a dynamic assurance case, via aggregating data samples are hyperglycemic, 0.11% are hypoglycemic, the uncertainty introduced by diferent evidence (e.g., and 99.75% are in the glycemic range. Thus, DR.C4 is from model training, testing, and verification) and reamet, but the data balance, DR.B1, is violated. We are not soning about the suficiency for assurance? certain about DR.C5. This requirement is met if the data • How to build automated tool support for the developgeneration model considers illness. Although the data is ment and review of safety AC for ML-enabled MCPS? generated by the simulator, DR.A2 is satisfied because the simulator models both the sensor and pump. There 7. Conclusion are not equal numbers for three subject groups in the dataset, which is another reason for the DR.B1 violation.
plate for APS as a representative of learning-enabled MCPS. We focused on ensuring the safety and efectiveness of the ML-based APS controller. We first extracted the primary performance and robustness requirements allocated to the APS controller. Then we enumerated the learning for highly automated driving functions, in: Computer requirements on the dataset and provided concrete evi- Safety, Reliability, and Security, 2019. dence regarding ML and data requirements. In the future, [17] C. Picardi, R. Hawkins, C. Paterson, I. Habli, A pattern for arguing the assurance of machine learning in medical diagnosis we plan to continue this line of research and investigate systems, in: A. Romanovsky, E. Troubitsyna, F. Bitsch (Eds.), the open problems listed in Section 6. Computer Safety, Reliability, and Security, 2019, pp. 165–179. [18] S. Kapil, R. Saini, S. Wangnoo, S. Dhir, Artificial pancreas Acknowledgment system for type 1 diabetes—challenges and advancements, ExThis work was supported in part by the National Science ploratory Research and Hypothesis in Medicine 5 (2020). [19] M. Narasimhamurthy, T. Kushner, S. Dutta, S. SankaraFoundation (NSF) grants CCF-1942836, CCF-2131511, and narayanan, Verifying conformance of neural network models: CNS-2146295 and by the Commonwealth Cyber Initia- Invited paper, in: 2019 IEEE/ACM International Conference tive, an investment in the advancement of cyber R&D, on Computer-Aided Design (ICCAD), 2019. innovation, and workforce development. [20] mobihealthnews, 2021. URL: https: //www.mobihealthnews.com/news/ roche-inks-deal-diabeloop-integrate-automated-insulin-delivery.
References [21] S. Dutta, T. Kushner, S. Sankaranarayanan, Robust data-driven control of artificial pancreas systems using neural networks, [1] J. He, S. L. Baxter, J. Xu, J. Xu, X. Zhou, K. Zhang, The prac- in: M. Češka, D. Šafránek (Eds.), Computational Methods in tical implementation of artificial intelligence technologies in Systems Biology, 2018, pp. 183–202.
medicine, Nature Medicine 25 (2019) 30–36. [22] M. Zhang, K. B. Flores, H. T. Tran, Deep learning and regres[2] R. Ashmore, R. Calinescu, C. Paterson, Assuring the machine sion approaches to forecasting blood glucose levels for type 1 learning lifecycle: Desiderata, methods, and challenges, ACM diabetes, Biomedical Signal Processing and Control 69 (2021).
Comput. Surv. 54 (2021). [23] S. Lee, J. Kim, S. W. Park, S.-M. Jin, S.-M. Park, Toward a fully [3] R. Bloomfield, P. Bishop, Safety and assurance cases: Past, automated artificial pancreas system using a bioinspired reinpresent and possible future – an adelard perspective, in: Mak- forcement learning design: In silico validation, IEEE Journal ing Systems Safer, 2010, pp. 51–67. of Biomedical and Health Informatics 25 (2021). [4] E. Asaadi, E. Denney, J. Menzies, G. J. Pai, D. Petrof, Dynamic [24] FDA approval for Medtronic MiniMed, 2022. URL: https://www. assurance cases: A pathway to trusted autonomy, Computer accessdata.fda.gov/cdrh_docs/pdf16/P160017S076b.pdf. 53 (2020) 35–46. [25] B. Kovatchev, P. Cheng, S. M. Anderson, J. E. Pinsker, F. Boscari, [5] R. Clothier, E. Denney, G. J. Pai, Making a risk informed B. A. Buckingham, F. J. Doyle III, K. K. Hood, S. A. Brown, M. D. safety case for small unmanned aircraft system operations, in: Breton, et al., Feasibility of long-term closed-loop control: a 17th AIAA Aviation Technology, Integration, and Operations multicenter 6-month trial of 24/7 automated insulin delivery, Conference, 2017, p. 3275. Diabetes technology & therapeutics 19 (2017) 18–24. [6] L. Feng, A. L. King, S. Chen, A. Ayoub, J. Park, N. Bezzo, [26] J. L. Sherr, B. A. Buckingham, G. P. Forlenza, A. Galderisi, O. Sokolsky, I. Lee, A Safety Argument Strategy for PCA L. Ekhlaspour, R. P. Wadwa, L. Carria, L. Hsu, C. Berget, T. A. Closed-Loop Systems: A Preliminary Proposal, in: 5th Work- Peyser, et al., Safety and performance of the omnipod hyshop on Medical Cyber-Physical Systems, 2014. brid closed-loop system in adults, adolescents, and children [7] Infusion pumps total product life cycle, guidance for industry with type 1 diabetes over 5 days under free-living conditions, and FDA staf, 2014. Diabetes technology & therapeutics 22 (2020) 174–184. [8] ISO 26262: Road vehicles — functional safety, 2018. [27] N. S. Chen, C. K. Boughton, S. Hartnell, J. Fuchs, J. M. Allen, [9] ISO/PAS 21448: Road vehicles — safety of the intended func- M. E. Willinska, A. Thankamony, C. de Beaufort, F. M. Camptionality, 2019. bell, E. Fröhlich-Reiterer, et al., User engagement with the [10] ANSI/UL 4600: Standard for safety for the evaluation of au- CamAPS FX hybrid closed-loop app according to age and user tonomous products, 2022. characteristics, Diabetes care 44 (2021) e148–e150. [11] The content of Investigational Device Exemption (IDE) and [28] T. D. Care, Basal-IQ, 2022. URL: https://www.tandemdiabetes.
Premarket Approval (PMA) Applications for Artificial Pan- com/providers/products/basal-iq.
creas Device Systems, 2012. [29] Goal Structuring Notation Community Standard Version 2, [12] R. Hawkins, C. Paterson, C. Picardi, Y. Jia, R. Calinescu, I. Habli, 2018. URL: https://scsc.uk/r141B:1?t=1.
Guidance on the assurance of machine learning in autonomous [30] 2022. URL: https://rtg.cis.upenn.edu/gip/. systems (AMLAS), 2021. [31] F. Cameron, G. Fainekos, D. M. Maahs, S. Sankaranarayanan, [13] R. Kaur, R. Ivanov, M. Cleaveland, O. Sokolsky, I. Lee, Assur- Towards a verified artificial pancreas: Challenges and solutions ance case patterns for cyber-physical systems with deep neural for runtime verification, in: E. Bartocci, R. Majumdar (Eds.), networks, in: A. Casimiro, F. Ortmeier, E. Schoitsch, F. Bitsch, Runtime Verification, 2015, pp. 3–17.
P. Ferreira (Eds.), SAFECOMP Workshops, 2020, pp. 82–97. [32] X. Zhou, M. Kouzel, H. Ren, H. Alemzadeh, Design and val[14] S. Burton, I. Kurzidem, A. Schwaiger, P. Schleiss, M. Unter- idation of an open-source closed-loop testbed for artificial reiner, T. Graeber, P. Becker, Safety assurance of machine pancreas systems, in: the IEEE/ACM international conference learning for chassis control functions, in: Computer Safety, on Connected Health: Applications, Systems and Engineering Reliability, and Security, 2021. Technologies (CHASE), 2022. [15] L. Gauerhof, R. Hawkins, C. Picardi, C. Paterson, Y. Hagiwara, [33] J. Xie, Simglucose v0.2.1 (2018) [online], 2022. URL: https:// I. Habli, Assuring the safety of machine learning for pedestrian github.com/jxx123/simglucose. detection at crossings, in: A. Casimiro, F. Ortmeier, F. Bitsch, [34] 2022. URL: https://arxiv.org/abs/2211.15413. P. Ferreira (Eds.), Computer Safety, Reliability, and Security, [35] D. Shriver, S. Elbaum, M. B. Dwyer, Dnnv: A framework 2020, pp. 197–212. for deep neural network verification, in: Computer Aided [16] S. Burton, L. Gauerhof, B. B. Sethy, I. Habli, R. Hawkins, Con- Verification: 33rd International Conference, 2021, p. 137–150.
ifdence arguments for evidence of performance in machine [36] S. Bak, nnenum: Verification of relu neural networks with optimized abstraction refinement, in: NASA Formal Methods (NFM), 2021.