病院のオーダリングシステムでは、医師、看護師、検査技師、薬剤師、栄養士などが、職種ごとの役割に応じて同じオーダーを参照または操作する。 ある時点のデータだけが正しくても、取得、変更、中止、開始、完了の順序によっては、業務規則に反する状態へ到達し得る。 時相論理を使えば、個々の状態に加えて、複数のアクターによる操作を並べた状態列も検査対象にできる。
ただし、すべての関心事を一つのオーダー状態へ押し込む必要はない。 FHIR の ServiceRequest では依頼の状態を主に依頼者が管理し、実施者側の活動状態は対応するイベントまたは Task で表す。 Task は実施する活動の取得、受諾、開始、一時停止、完了、失敗、中止などを追跡する。 この区別に沿えば、医療オーダーのモデルは「依頼が何を求めているか」と「実施側がどこまで進んだか」という二つの状態機械になる。
たとえば検査オーダーについて、次の状態列を考える。
状態0: オーダーは有効、実施タスクは未取得、版は1
状態1: 検査技師が実施タスクを取得、参照した版は1
状態2: 医師がオーダーを変更し、版は2
状態3: 検査技師が版1の内容に基づいて実施を開始状態3を許すかどうかは、一つの状態値からは決まらない。 実施者がどの版を確認したか、変更時に旧版を失効させたか、すでに実施を開始していたか、変更を誰へ通知するかという時間的な関係が要る。 Alloy ではオーダー状態、実施状態、担当者、確認済みの版を可変な関係として表し、各職種の操作を遷移として定義できる。 そのうえで「失効した版を新たに取得できない」「一人だけが取得できるタスクを二人が同時に所有しない」「完了の前には許可された開始がある」など、施設が採用する規則を安全性として検査できる。
Alloy で版の取り違えを探す
動作確認用の Alloy モデルは、上の状態列を最小限の要素で表している。 claim は検査技師が実施タスクを取得して現在の版を確認する遷移、revise は医師が版1を版2へ変更する遷移、start は検査技師が実施を開始する遷移である。 start には、確認済みの版と現在の版が一致するという前提を意図的に入れていない。
完全なモデルと再現手順は次の Gist に置いている。
Alloy Analyzer は NoStartFromStaleVersion を破る次の状態列を見つける。
状態0: currentVersion=V1, status=Ready, owner=none, acknowledgedVersion=none
状態1: currentVersion=V1, status=Claimed, owner=Technician, acknowledgedVersion=V1
状態2: currentVersion=V2, status=Claimed, owner=Technician, acknowledgedVersion=V1
状態3: currentVersion=V2, status=InProgress, owner=Technician, acknowledgedVersion=V1状態1から状態2でオーダーだけが更新され、状態2から状態3で古い版を確認した検査技師が実施を開始している。 start に次の前提を加えると、この反例は5ステップの範囲では見つからなくなる。
Fulfillment.acknowledgedVersion = LabOrder.currentVersion活性としては、「受諾されたタスクは、いつか完了、失敗、中止のいずれかへ進む」のような性質を候補にできる。 この性質に反して受諾状態へ留まり続ける状態列が見つかれば、処理の再開条件、再通知、引き継ぎ、エスカレーションのどれがモデルに欠けているかを検討できる。 ただし、現実の担当者が必ず行動することを時相論理だけで保証できるわけではないため、どの条件なら処理が進むと仮定するかもモデルに含める必要がある。
中止後の扱いは、とくに現場確認が要る。 FHIR の Task 仕様も、中止の意図が作業の停止であっても、現実の作業を止められず、後から実施結果が関連付けられる場合があるとしている。 したがって「中止後は結果が存在しない」と一律に制約するのではなく、作業開始前、作業中、結果登録後を区別し、各段階で許される遷移を業務規則から決める必要がある。
時相論理が検査するのは、診療内容そのものの正しさではない。 職種別の権限、代行入力、口頭指示、事後承認、変更通知、中止不能な作業を状態と遷移にしたとき、その規則がすべての操作順序で矛盾しないかを検査する。 Alloy Analyzer が示す反例は、複数のアクターが介入したときだけ現れる規則の抜けを、実装前に具体的な状態列として読む材料になる。
https://hl7.org/fhir/servicerequest-definitions.html
https://hl7.org/fhir/R5/task.html
https://hl7.org/fhir/R5/workflow-management.html
https://alloytools.org/alloy6.html
#healthcare #order-entry-system #temporal-logic #alloy #formal-methods #state-machine