Kerangka Kerja Verifikasi Formal Model Sistem Rekam Medis Elektronik Berwaktu ( RME⁺)

Taryana, Acep (2026) Kerangka Kerja Verifikasi Formal Model Sistem Rekam Medis Elektronik Berwaktu ( RME⁺). Doctoral thesis, Institut Teknologi Sepuluh Nopember.

Text 7002221003-Doctoral.pdf - Accepted Version Restricted to Repository staff only Download (10MB) | Request a copy

Abstract

Verifikasi formal sangat penting dalam memastikan kebenaran dan keandalan sistem nyata-waktu (real-time) yang kompleks. Penelitian ini mengembangkan kerangka kerja verifikasi formal yang digeneralisasi untuk Timed System Models, guna mengatasi risiko inheren dari kesalahan logika, bug, dan deadlock yang berdampak pada domain safety-critical. Meskipun metodologi ini dapat diterapkan pada berbagai sistem berwaktu, studi ini menggunakan sistem Rekam Medis Elektronik Berwaktu ( RME⁺) sebagai studi kasus representatif untuk memvalidasi pendekatan tersebut. Inti dari penelitian ini adalah pengembangan metode verifikasi terintegrasi yang menerapkan logika temporal untuk membangun model yang secara ketat mematuhi kebutuhan berwaktu (timed requirements). Dengan memformalkan perilaku sistem melalui timed automata dan spesifikasi melalui Timed Computational Tree Logic (TCTL), kerangka kerja ini mengatasi keterbatasan teknik tradisional dalam menangani struktur temporal yang kompleks. Kontribusi signifikan dari penelitian ini adalah usulan metode translasi yang mengonversi model berwaktu dan formula TCTL tersebut ke dalam sintaks Satisfiability Modulo Theories (SMT) untuk verifikasi otomatis. Efektivitas kerangka kerja ini dievaluasi melalui perbaikan iteratif (iterative refinement) pada tiga skenario dalam studi kasus RME⁺, yaitu: (1) logika reaktif untuk memverifikasi alur kerja administratif mendasar menggunakan Linear Temporal Logic (LTL); (2) sinkronisasi sumber daya guna mengelola konkurensi dalam layanan Home Care Plan (HCP) dengan ketersediaan staf medis dibatasi oleh waktu dan lokasi; serta (3) resolusi konflik untuk mencegah deadlock dan timelock dalam akses sumber daya kompetitif, contohnya alokasi kamar pasien. Hasil validasi membuktikan bahwa kerangka kerja ini secara efektif mendeteksi ketergantungan sirkular (circular dependencies) dan pseudo-deadlocks yang dipicu oleh latensi komputasi, yang diselesaikan melalui penerapan committed locations dan mekanisme timeout. Penelitian ini menawarkan kerangka kerja yang kokoh untuk memfasilitasi proses transisi dari model formal menjadi artefak perangkat lunak yang andal.
===================================================================================================================================
Formal verification is essential for ensuring the trustworthiness and reliability of complex real-time systems. This research develops a generalized formal verification framework for Timed System Models to address the inherent risks of logical errors, software bugs, and deadlocks that affect safety-critical domains. Although the proposed methodology is applicable to a wide range of timed systems, a Timed Electronic Medical Record (EMR+) system is employed as a representative case study to validate the framework. The core contribution of this research is the development of an integrated verification method that applies temporal logic to construct models that strictly satisfy timing requirements. By formalizing system behavior using timed automata and system specifications using Timed Computational Tree Logic (TCTL), the framework overcomes the limitations of conventional verification techniques in handling complex temporal behaviors. A key contribution of this study is the proposed translation method that converts timed automata models and TCTL specifications into Satisfiability Modulo Theories (SMT) syntax, enabling automated formal verification. The effectiveness of the framework is evaluated through iterative refinement across three scenarios in the EMR+ case study: (1) reactive logic for verifying fundamental administrative workflows using Linear Temporal Logic (LTL); (2) resource synchronization for managing concurrency in Home Care Plan (HCP) services, where medical staff availability is constrained by both time and location; and (3) conflict resolution for preventing deadlocks and timelocks during competitive resource access, such as patient room allocation. The validation results demonstrate that the proposed framework effectively detects circular dependencies and pseudo-deadlocks caused by computational latency, which are subsequently resolved through the implementation of committed locations and timeout mechanisms. Overall, this research provides a robust framework for bridging formal models and reliable software artifacts.

Item Type:	Thesis (Doctoral)
Uncontrolled Keywords:	deadlock, RME⁺, SMT solver, timed automata, verifikasi formal.
Subjects:	Q Science > QA Mathematics > QA76.758 Software engineering
Divisions:	Faculty of Science and Data Analytics (SCIENTICS) > Mathematics > 44002-(S3) PhD Thesis
Depositing User:	Acep Taryana
Date Deposited:	06 Aug 2026 06:13
Last Modified:	06 Aug 2026 06:13
URI:	http://repository.its.ac.id/id/eprint/144029

Actions (login required)

View Item