1 of 10

Making Model Checking Usable & Accessible for HIT Workflows

Bryce Pierson* and Eric Mercer

Brigham Young University

Provo UT, USA

Keith Butler*

University of Washington

Seattle WA, USA

2 of 10

Functional integration of human cognition and machine reasoning is challenging especially where failure risks health or safety

3 of 10

Knowledge Types

Scenario: Patient with COVID-19 diagnosis, mild/asymptomatic & no co-morbidities & treatment plan for home care with remote patient monitoring (RPM);

Requirement: The cognitive work problem (CWP) that RPM must solve:

Establish & maintain actionable risk awareness of the patient's condition- defined as a finite state machine;

Design: A BPMN workflow for an HIT design that solves the CWP by integrating the functionality of patients at home, AI in the cloud, and providers at their offices;

Automatic translations: The BPMN graphical workflow into Promela, a formal process modeling language, & the CWP into linear temporal logic;

Correctness analysis: Of the workflow's HIT design by the SPIN model-checker, and the meaning of its verification certificate;

Fault isolation: Any design flaws reported by SPIN are mapped back onto the graphical BPMN model.

4 of 10

The CWP of remote patient monitoring (RPM) is actionable risk awareness

RPM must solve the CWP

- its computational meaning is defined by this finite state diagram of allowed states & transition rules;

- it must handle care transitions per NIH 2019 COVID Guidelines.

Patient safety is defined by the cognitive work problem of actionable risk awareness.

It is computation independent, defined by a UML state diagram, and complies with NIH guidelines.

It starts with a positive exam. Based on the severity and the ability of the patient to be cared for at home, the doctor prescribes homecare (A) or other appropriate care (B).

Click

When the doctor prescribes homecare, the orders include an monitoring and exam schedule, and it is hoped that at some point an exam finds that the patient meets discharge criteria and no longer needs monitoring.

Click

It is also possible that the severity of the disease progresses in homecare to a point where the patient is at an elevated risk.

Here there is a possibility of the patient passing.

Click

That said, an exam may find that the patient is no longer safe at home.

Click

Or that the patient can still be safe at home with an appropriate change in monitoring or other prescriptions to manage the disease.

Click

The patient of course may pass while being cared for outside the home.

Click

Or recover and be discharged from care.

5 of 10

System Design in BPMN for Remote Patient Monitoring with PHware

Must satisfy the actionable risk awareness CWP

The top portion of the workflow represents the responsibilities of the clinicians.

The workflow begins with a patient testing positive for COVID-19 and then having a subsequent exam.

Depending on the exam, the patient is prescribed home care or other appropriate care.

The orders include an exam schedule, so at some future exam, discharge criteria maybe satisfied and the patient no longer needs monitoring.

Similarly, if the patient is not in home care, but other ambulatory or hospital care, then that patient may be discharged or expire.

The bottom portion represents the responsibilities of the patient or those caring for the patient at home.

A patient in home care must start the doctor prescribed interventions and setup the PHware system.

Once PHware in configured, the patient follows the prescribed schedule for exams and measuring vitals.

Click

Here’s an image of the patient’s user experience.

The patient may expire in homecare, and if not, is expected to meet with the doctor or clinician at the scheduled times.

Here, the patient process ends at each exam time, and that process is restarted after an exam if needed.

The middle portion of the workflow represents the responsibilities of the AI analytics in the cloud.

It starts when it receives vitals, and it ends after it assigns numerical values to vitals and analyses have been sent to the clinicians.

If any combination of trends in vital signs exceeds the risk threshold an alert is added to the sent package.

Click.

The vitals, and alerts, are reviewed by the appropriate clinicians depending on the alert status.

An alert re-orders that patient towards the top of the clinician’s patient panel.

Click

The data trend that is the basis of an alert can be viewed with one click.

In the presence of an alert, and based on the scheduled exam, the exam maybe rescheduled sooner.

Click

Similarly, in the absence of an alert, if the exam has yet to be scheduled, the normal routine exam is arranged.

Click

The person reviewing the vitals from the AI analytics may change the exam priority of the patient as appropriate.

Click

The workflow returns to the beginning if the scheduled exam is now.

Click

Or it returns to the monitoring state if it is not time for the exam.

6 of 10

�

How do we know if the HIT workflow design for PHware preserves actionable risk awareness as defined in the CWP?

7 of 10

Proposed Solution

Cognitive Work Problem (UML)

System Design (BPMN)

Model Checking (SPIN)

What

How

Does the BPMN solve the CWP?

To Linear Temporal Logic (LTL)

To Process Meta Language (Promela)

The solution proposed in this work is to separate WHAT a system must do from HOW it does it.

The meaning of ”patient safety” is first described as a cognitive work problem.

It is a declarative statement in the from of a UML state diagram that describes what a system must accomplish.

The state diagram defines allowable states of the problem and allowable ways that problem evolves overtime until it reaches some set of goal or end states.

The HOW is the system design. In this application, it is a workflow in the business process modeling notation.

Graphical standards are used so that doctors and other stake holders are able to participate in the design process.

The WHAT and HOW are related to one another through model checking.

In this application the model checker is SPIN. The WHAT is a set of linear temporal logic properties from the state diagram, and the HOW is a Promela version of the system design.

The model checker then proves whether or not the system design solves the cognitive work problem.

This work claims that without such analysis it is difficult to argue the absence of unwanted emergent behavior in the functional integration of human and machine reasoning.

8 of 10

LIVE DEMO

9 of 10

Expected Benefits

Thorough design flaw discovery before HIT gets too expensive to change will promote-

Increased patient safety;
Decreased provider burden of HIT use;
Increased HIT quality from

medical personnel reading and critiquing BPMN's graphical workflows,
and participating in design revisions;

Trustworthiness should increase by certification that all sequences of interactive HIT design are correct.

10 of 10

Relevant FAIR Principles

Findable- complex HIT designs can be indexed for discovery by the cognitive work problem they were certified to solve.
Accessible- automated translation from/to the languages of the design community will make model checking widely accessible and usable for HIT design.
Interoperable- the BPMN standard is widely adopted and available in dozens of commercial modeling products.
Reusable- the CWP’s finite state machine can be re-used for model checking & comparing multiple HIT design options.