MODEL-DRIVEN DEVELOPMENT: FASE AWAL VERIFIKASI MODEL DESIGN REKAM MEDIS ELEKTRONIS MENGGUNAKAN PERUMUSAN GRAF LENGKAP
Abstrak. Pada makalah ini akan
ditunjukkan perumusan graf sebagai pendekatan formal dalam penelitian
Model-Driven Development (MDD) dengan studi kasus pengembangan Rekam Medis
Elektronis (RME) pada
ruang lingkup Puskesmas.
Model dirancang menggunakan notasi
grafis Unified Modelling
Langguage (UML) dan
dipilih diagram State Machine
sebagai representasi kebutuhan
prasyarat pengguna (requirements). Sebelum model
diturunkan (driven) ke
dalam kerangka program,
State Machine harus diverifikasi ketepatan modelnya
sehingga meyakinkan (certainty).
Agar State Machine dapat
diverifikasi dengan pendekatan
formal maka State
Machine harus ditransformasikan kedalam
formula proposisi dengan
bantuan perumusan graf lengkap, dan model
parsial. Tahap awal
verifikasi akan mengecek
kesesuaian model dengan kebutuhan prasyarat
dalam Propositional Normal
Form (PNF) menggunakan
SAT Solver, berturut-turut ditulis 𝛷�
dan 𝛷𝑝.
SAT Solver akan memberikan sebuah keputusan perancangan, apakah
sebuah requirement tertuang
dalam model atau
tidak. Jika requirement tersebut
tidak terwakili maka
requirement tersebut kurang
meyakinkan (uncertain) dan harus dilakukan perancangan ulang model.
Penulis: Acep Taryana, Bangun
Wijayanto, Naoyasu Ubayashi, Joko Setyono
Kode Jurnal: jpmatematikadd141041
